Теоретические сведения. Приводимые в настоящем разделе задачи носят
характер небольшого самостоятельного исследования. Целью является
установление связи конструкций языков программирования с понятиями
исчисления λ-конверсии.
Характеристическое равенство функции Y имеет вид Y f = f(Y f). Ссы-
лающиеся на себя определение функции f можно искать в виде f = Ef,
где f не имеет свободного вхождения в E.
9.1 Элементы рекурсивных вычислений
Функция считается рекурсивной, если в определяющем ее выраже-
нии содержится хотя бы одно обращение к ней самой. Рассмотрим
рекурсивное определение функции вычисления факториала:
F AC = (λn.IF(= n 0)1(×n F AC(− n 1)))
При прямом применении этого определения происходят следующие
преобразования:
F AC = (λn.IF(= n 0)1
(×n F AC(− n 1))) =
F AC = (λn.IF(= n 0)1
(×n (λn.IF(= n 0)1
(×n F AC(− n 1)))(− n 1))) =
F AC = (λn.IF(= n 0)1
(×n (λn.IF(= n 0)1
(×n(λn.IF(= n 0)1
(×n F AC(− n 1)))(− n 1)))(− n 1))) =
. . . . . . .
Нетрудно заметить, что цепочка таких преобразований не заверша-
ется никогда. В предлагаемой записи λ-терму присвоено имя F AC.
Эта запись естественна и удобна, однако не согласуется с синтак-
сисом исчисления, так как в λ-исчислении именование функций не
предусмотрено. В связи с этим данное выражение следует перевести
на язык λ-исчисления, то есть выразить рекурсию в чистом виде (без
самоссылки). Как оказывается, такой перевод возможен, причем без
выхода за рамки комбинаторной логики. |
Главная
Каталог файлов
