Рекурсивные объявления функций

Все языковые элементы, введенные до сих пор, в совокупности допускают исключительно описание выражений, которые ведут всегда к терминированным ("конечно ограниченным") вычислениям, если только все вычисления для применяемых базисных функций терминированы. Тем самым длительность последовательностей вычисления всегда статически ограничена. Чтобы можно было допустить вычислительные предписания с неограниченно долгими вычислениями, применяется концепция рекурсивного объявления функций.

Объявление функции fct f = (m x) n: E называется рекурсивным,

если в абстракцию в правой части объявления (вернее, в тело E) снова свободно входит объявляемый идентификатор f. Рекурсивные объявления функций в общем случае ведут к вычислительным предписаниям с неограниченной длительностью вычислений и тем самым представляют собой мощный инструмент программирования. Соответственно этому понимание семантической интерпретации рекурсивных объявлений является особенно важным, но в то же время более трудным, чем при нерекурсивных объявлениях

В рекурсивном объявлении fct f = (m x) n: E символ функции f снова входит в Е в правой части. Поэтому абстракцию (m x) n: E

нельзя понимать как определение. Если попытаться абстракцию наивно представить как определение для f, то это приводит к "цикличности" определения. Так что сначала полностью не ясно, какая функция должна быть связана с идентификатором f.

Соответственно для рекурсивного объявления нельзя, как для нерекурсивного вычислительного предписания, вывести значение просто с помощью установления I[fct f = (m x) n:E](

) =

[f1/f], где f1 = I[(m x) n: E](

), так как в Е снова встречается символ f и тем самым функция f1 не может быть определена без того, чтобы в

было задано значение для f. Это определение во всяком случае является циклическим: значение для f может быть установлено, если имеется налицо значение f. Поэтому из рекурсивного объявления можно сначала вывести лишь предписание, которое каждой заданной функции f ставит в соответствие функцию f1.

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

·

индуктивное толкование;

· толкование через равенство фиксированной (неподвижной) точки.

В обоих толкованиях однозначно устанавливается, какое отображение предписывается идентификатору с помощью рекурсивного объявления.

До того как последует точное описание смысла рекурсивного объявления, сначала необходимо дать краткое разъяснение способа того, как можно обращаться операционально с рекурсивным объявлением

Подстановку правой части объявления функции вместо функции называют расширением

или развертыванием (англ. unfold) вызова рекурсивной функции. Через повторное применение правила расширения можно при известных обстоятельствах редуцировать рекурсивный вызов к значению. Идея вычисления через расширение является ведущей линией для операционального смысла рекурсивных объявлений функций.

При толковании с помощью функционала мы соединяем с рекурсивным объявлением функцию, которую связываем с объявляемым идентификатором.

Содержание раздела