Комбинатор y

Если есть функция Ф и комбинатор Y, то можем построить фиксированную точку:

Y F = F (Y F)

Раскрывая каждый раз Y F по равенству получим

F ( F ( …F(Y F)…)), т.е. мы получаем бесконечный терм, который нам позволит задать рекурсивный процесс. Свойства комбинатора – он позволяет любую функцию применить сколько угодно раз.

Комбинатор:

Y = h f . (h x . f (x x)) (h x . f (x x))

Докажем свойство фиксированной точки(применим комбинатор функции F):

Y F = ( h f . (h x . f (x x)) (h x . f (x x))) F

->_B (h x . F(x x)) (h x . F (x x))

->_B F((h x . F(x x)) (h x . F (x x))) =

F (Y F)

(на самом деле комбинаторов в фиксированной точке много)

Рассмотрим как Y комбинатор можно использовать для определения рекурсивного неравенства.

fact = h n . if (iszero n) 1

(mult n (fact (pred n))) [1]

Остается нереализованным вызов функции fact. Применим комбинатор фиксированной точки.

Абстрагируем рекурсивный вызов, мы получим F…, она будет иметь два аргумента..

F = h g n . if (iszero n) 1

(mult n (g(pred n))) [2]

Через Y-комбинатор эту функцию можно представить так

fact = Y F [3]

Т.е. (3) – это решение уравнения (1). Докажем это

Сделаем n-расширение (этта) с (3)

fact n = Y F n [4]

По свойству Y комбинатора получим

fact n = F (Y F) n [5]

свернув 5 по 3 получим

fact n = F fact n

Выполнив B редукцию дял F мы получим

fact n = if (iszero n) 1

(mult n (fact (pred n)))

А это определение (1)

Через Y комбинатор мы можем представить любую рекурсивную функцию. Циклы можно тоже через У комбинатор описать. Поэтому есть важная теория – теория фиксированной точки. Это основа теоретиеской информатики

Вычислим fact 3

Y F 3 = F (Y F) 3 Ξ

(h g n . if (iszero n) 1

(mult n (g (pred n)))) (Y F) 3 ->_B

(h n . if (iszero n) 1

(mult n ((Y F) (pred n))) 3 ->_B

if (iszero 3) 1 (mult 3 ((Y F) (pred 3))) ->>

(mult 3 ((Y F) 2)) =

(mult 3 (F(Y F) 2)) ->>

(mult 3 (mult 2 ((Y F) 1))) ->>

(mult 3 (mult 2 (mult 1 ((Y F) 0)))) ->>

(mult 3 (mult 2 (mult 1 1))) ->> 6

Вычислим fact 0

Y F 0 = F (Y F) 0 Ξ (свойство комбинатора У)

(h g n . if (iszero n) 1

(mult n (g (pred n)))) (Y F) 0 ->_B

(h n . if (iszero n) 1

(mult n (Y F (pred n))) 0 ->_B

If (iszero 0) 1 (mult 0 (Y F (pred 0)))->>1

(Рассказ про y комбинатор – сразу зачёт)