Вычисление выражений при помощи комбинаторной логики

Приписывание типа комбинатору неподвижной точки.

Ya = a(Ya)

a^α(Ya)^β Y^{α→ β}

a ^β→γ

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

Замечание:

Y в типизированном исчислении не существует.

Выражение вида:

let x=plus in x(4(x where x=3))

можно переписать так: (λx.x 4((λx.x)3))+

Здесь λx.x = I

λx.C = KC, xFV(C)

λx.PQ = S(λx.P)(λx.Q)

λx.x4((λx.x)3) = λx.((x4)(I3)) = S(λx.x4)(λx.(I3)) = S(S(λx.x)(λx.4))(K(I3)) =

S(SI(K4))(K(I3)) =>

S(SI(K4))(K(I#))+ = SI(K4)+(K(I3)+) = I+((K4)+)(K(I3)+) = I+(K4+)(K(I3)+) = +4(I3) = +43

Контрольные вопросы

1. В чем Вы видите преимущества типизированных систем перед бестиповыми?
2. Задайте типы основных комбинаторов.
3. Какое правило вывода позволяет приписывать тип аппликации типизированных объектов?
4. Приведите примеры комбинаторов, которым невозможно приписать тип.
5. Вычислите выражение let x = 12 in *((x where x=7)(y where y=x))

Дата добавления: 2014-01-11