Определение. λ-терм - слово, выводимое в грамматике:

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 )
...

Литература:

1. A short introduction to the Lambda Calculus. Achim Jung. 2004