Является ли моя функция rec хвостовой рекурсивной? - PullRequest
Новая
       3

Является ли моя функция rec хвостовой рекурсивной?

3 голосов
/ 27 апреля 2011


Является ли эта функция хвостовой рекурсивной?

let rec rec_algo1 step J = 
    if step = dSs then J
    else
        let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J)
        let argmin = a|> Array.minBy snd |> fst
        rec_algo1 (step+1) (argmin::J)

В общем, есть ли способ формально проверить это?

Спасибо.

Ответы [ 3 ]

4 голосов
/ 28 апреля 2011

Да, вы можете формально доказать, что функция является хвостово-рекурсивной. Каждое сокращение выражения имеет хвостовую позицию, и если все рекурсии находятся в хвостовой позиции, то функция является хвостовой рекурсивной. Функция может быть хвостовой рекурсивной в одном месте, но не в другом.

В выражении let pat = exprA in exprB только exprB находится в хвостовой позиции. То есть, пока вы можете оценить exprA, вам все равно придется вернуться, чтобы оценить exprB с учетом exprA. Для каждого выражения в языке есть правило сокращения, которое говорит вам, где находится хвостовая позиция. В ExprA; ExprB это снова ExprB. В if ExprA then ExprB else ExprC это и ExprB, и ExprC, и т. Д.

Компилятор, конечно, знает это по ходу дела. Однако множество выражений, доступных в F #, и множество внутренних оптимизаций, выполняемых компилятором, например, например. во время компиляции сопоставления с образцом вычислительные выражения, такие как seq{} или async{}, могут не знать, какие выражения находятся в хвостовой позиции.

Практически говоря, с некоторой практикой для небольших функций легко определить хвостовой вызов, просто взглянув на ваши вложенные выражения и проверив слоты, которые НЕ находятся в конечных положениях для вызовов функций. (Помните, что хвостовой вызов может относиться к другой функции!)

4 голосов
/ 28 апреля 2011

Вы спросили, как мы можем официально проверить это, чтобы я получил удар. Сначала мы должны определить, что означает, что функция должна быть рекурсивной. Определение рекурсивной функции вида 

let rec f x_1 ... x_n = e

является хвостовой рекурсией, если все вызовы f внутри e являются хвостовыми вызовами - т.е. происходят в хвостовом контексте. хвостовой контекст C определяется индуктивно как термин с отверстием []: 

C ::= []
    | e
    | let p = e in C
    | e; C
    | match e with p_1 -> C | ... | p_n -> C
    | if e then C else C

, где e - это выражение F #, x - это переменная, а p - это шаблон. Мы должны расширить это до взаимно рекурсивных определений функций, но я оставлю это как упражнение.

Давайте теперь применим это к вашему примеру. В этом контексте единственный вызов rec_algo1 в теле функции: 

if step = dSs then J
else
    let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J)
    let argmin = a|> Array.minBy snd |> fst
    []

А поскольку это хвостовой контекст, функция является хвостовой рекурсивной. Вот как это делают функциональные программисты: просмотрите тело определения на предмет рекурсивных вызовов, а затем убедитесь, что каждое из них происходит в хвостовом контексте. Более интуитивное определение хвостового вызова - это когда ничего не делается с результатом вызова, кроме его возврата.

4 голосов
/ 27 апреля 2011

Эта функция хвостовая рекурсия; Я могу сказать это, взглянув на это.

В общем, это не всегда легко сказать. Возможно, самая надежная / прагматичная вещь - это просто проверить его на большом входе (и убедиться, что вы компилируете в режиме «Release», поскольку режим «Debug» отключает хвостовые вызовы для лучшей отладки).

...