Является ли эта функция хвостовой рекурсивной?
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)
В общем, есть способ формально проверить его?
Спасибо.
Эта функция является хвостовой рекурсивной; Я могу сказать, заметив это.
В общем, не всегда легко сказать. Возможно, самая надежная/прагматичная вещь - просто проверить ее на большом входе (и убедитесь, что вы компилируете в режиме "Release", так как режим "Отладка" отключает хвостовые вызовы для лучшей отладки).
Да, вы можете формально доказать, что функция является хвостовой рекурсивной. Каждое сокращение выражения имеет хвостовое положение, и если все рекурсии находятся в хвостовых позициях, тогда функция является хвостовой рекурсивной. Возможно, что функция является хвостовой рекурсивной в одном месте, но не в другой.
В выражении let pat = exprA in exprB только exprB находится в хвостовом положении. То есть, пока вы можете оценить exprA, вам все равно придется вернуться к оценке exprB с помощью exprA. Для каждого выражения на языке существует правило сокращения, указывающее, где находится позиция хвоста. В ExprA; ExprB он exprB снова. В if ExprA then ExprB else ExprC это как exprB, так и ExprC и т.д.
Компилятор, конечно, знает об этом. Однако многие выражения, доступные в F #, и множество внутренних оптимизаций, выполняемых компилятором по мере их использования, например, при компиляции совпадения с образцом выражения вычисления, такие как seq{} или async{}, могут знать, какие выражения в хвостовом положении неочевидны.
Практически говоря, с некоторой практикой для небольших функций легко определить хвостовой вызов, просто взглянув на ваши вложенные выражения и проверив слоты, которые НЕ находятся в хвостовых позициях для вызовов функций. (Помните, что вызов хвоста может быть другой функцией!)
Ты спросил, как мы можем официально проверить это, чтобы у меня был удар. Сначала мы должны определить, что означает, что функция является хвосторекурсивной. Рекурсивное определение функции вида
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
[]
И поскольку это хвостовой контекст, функция является хвостовой рекурсивной. Вот как это делают функциональные программисты - сканируйте тело определения для рекурсивных вызовов, а затем убедитесь, что каждый из них встречается в хвостовом контексте. Более интуитивное определение хвостового вызова - это когда ничего другого не делается с результатом вызова, кроме его возврата.