Редукция и равенство

Бинарное отношение ρ на множестве лямбда-термов называется совместимым (с операциями λ-исчисления), если для любых термов u, v, w: (u, v) ∈ ρ влечёт

(wu, wv) ∈ ρ,
(uw, vw) ∈ ρ,
(λx.u, λx.v) ∈ ρ.

Редукция — это совместимое рефлексивно-транзитивное замыкание отношения на множестве лямбда-термов, задаваемого β-конверсией.

Пусть u →_β v. Тогда

• u называется β-редексом,
• v — β-свёрткой, или β-редуктом,
• процесс преобразования — сворачиванием.

Мы хотим трактовать редукцию как

• равенство в одну сторону,
• преобразование, отражающее вычисление терма,
• преобразование, применимое к любым подтермам (благодаря условию совместимости).

Терм находится в нормальной форме (нф), если он не содержит β-редексов.

Терм v называется нормальной формой терма u, если v находится в нф и u редуцируется к v:

u → v.

Редукция за несколько шагов называется редукционной цепочкой.