В качестве основного примера, выполнение которого иллюстрирует
основные эффекты вычислений с неподвижной точкой воспользуем-
ся функцией факториала F AC. Запишем функцию F AC сокращен-
но:
F AC = λn.(. . . F AC . . .). (9.1)
Применяя λ-абстракцию, получим:
λf ac.F AC f ac = (λf ac.(λn.(. . . f ac . . .)))F AC. (9.2)
9.2. ИСПОЛЬЗОВАНИЕ КОМБИНАТОРА Y
По правилу (η) получаем:
λf ac.F AC f ac = F AC,
и определение (9.2) запишется в виде:
F AC = (λf ac.(λn.(. . . f ac . . .)))F AC. (9.3)
Полагая H = λf ac.(λn.(. . . f ac . . .)), получим:
F AC = H F AC. (9.4)
Определение H представляет собой обычную λ -абстракцию, не ис-
пользующую рекурсию. Рекурсия выражена только лишь в форме
равенства (9.4). Определение (9.4) похоже на математическое урав-
нение. Например, решить уравнение (x2 −2) = x - это значит найти
значения x, которому удовлетворяют (x = −1, x = 2). Аналогич-
но, для того, чтобы решить (9.4), необходимо найти λ -абстракцию
для F AC, которая удовлетворяет (9.4). Уравнение F AC = H F AC
выражает тот факт, что когда функция H применяется к аргументу
F AC, в результате снова получаетсяF AC. ПоэтомуF AC называет-
ся неподвижной точкой функции H.
Пример 1. Числа 0 и 1 являются неподвижными точками функции
f = λx.×x x, то есть f0 = 0 и f1 = 1. Действительно,
f0 = (λx.×x x)0 = (β)
= × 0 0 = 0,
f1 = (λx.×x x)1 = (β)
= × 1 1 = 1.
Итак, нужно найти неподвижную точку функции H. Ясно, что эта
точка зависит только от H. Введем функцию Y , которая работает по
схеме: получив на входе в качестве аргумента функцию, на выходе
Y формирует неподвижную точку этой функции. То есть, получа-
ем Y H = H(Y H), где Y -- комбинатор неподвижной точки. Если
найдем такой Y , то получим решение уравнения (9.4):
F AC = Y H.
В ходе получения этого решения использован довольно общий ме-
тод. Он опирается на основную в теории рекурсивных вычислений
теорему о неподвижной точке. Фактически, пришлось дать ее част-
ное “доказательство” для функции F AC. Полученное решение дает
нерекурсивное определение F AC. Существо теоремы о неподвиж-
ной точке как раз и состоит в том, чтобы гарантировать переход от ре-
курсивных по форме записи определений к нерекурсивным по фор-
ме записи определениям. В последнем случае эффект цикличности
определения (и соответствующего вычисления) оказывается завуа-
лированным посредством комбинатора Y . Для того, чтобы убедится,
что определенная таким образом функцияF AC работает правильно,
приложим ее к некоторому аргументу, например, к 1:
F AC 1 = Y H 1 (F AC)
= H(Y H)1 (Y )
= (λf ac.(λn.(IF(= n 0)1)(×n(f ac(− n 1))))(Y H)1 (H)
= (λn.IF(− n ))1(×n(Y H(− n 1))))1 (β)
= IF(= 1 0)1(×1(Y H(− 1 1)))) (β)
= ×1(Y H)0 = ×1(H(Y H))0 (Y )
= ×1((λf ac.λn.IF(= n 0)1(×n(f ac(− n 1))))(Y H)0 (H)
= ×1((λn.IF(= n 0)1(×n(Y H(− n 1))))0) (beta)
= ×1(IF(= 0 0)1(×0(Y H(− 0 1)))) (β)
= ×11
= 1.
|
Главная
Каталог файлов
