Term =
Atom | Abstraction | Application
Atom =
Variable | Constant | ( Term )
Abstraction =
λ Variable . Term
Application =
Application Atom | Atom Atom
Variable =
x | y ...
Constant =
1 | 2 ... + | - ...
термы вида λ x .( λ y . (...)) часто сокращают до λ x y . (...)
Редукция:
- α-преобразование - переименование параметра абстракции (применяется первой)
- β-редукция - подстановка значения параметра абстракции
- η-редукция - отбрасывание избыточной абстракции
Пример:
( ( λ a . ( λ b . + a b ) ( λ a x . * 2 a ) ) 3 ) 4
α=
( ( λ a . ( λ b . + a b ) ( λ c x . * 2 c ) ) 3 ) 4
η=
( ( λ a . ( λ b . + a b ) ( λ c . * 2 c ) ) 3 ) 4
β=
( λ b . + ( λ c . * 2 c ) b ) 3 ) 4
=
( ( λ b с . + * 2 c b ) 3 ) 4
β=
( λ c . + * 2 c 3 ) 4
β=
+ * 2 4 3 = 2*4 + 3 = 11
Теорема (о полноте λ-исчислений по Тьюрингу). Любую вычислимую ƒ : Z* → Z* можно записать как λ-терм и вычислить при помощи правил редукции, если в качестве констант использовать множество Z*∪{pred, succ, zero?}.
zero? 0 x y = x
zero? n x y = y ( n ≠ 0 )
succ 0 = 1
...
succ ( pred x ) = pred ( succ x ) = x
Можно обойтись и без Z*, если принять
0 = λ f x . x
1 = λ f x . f x
2 = λ f x . f ( f x )
...
Литература:
- A short introduction to the Lambda Calculus. Achim Jung. 2004
