Скорочення
Значення лямбда-виразів визначається тим, як вони можуть бути скорочені.
Існує три види обрізання:
- α-перетворення: зміна пов’язаних змінних (альфа).
- β-редукція: застосування функцій до своїх аргументів (бета).
- η-перетворення: охоплює поняття экстенсиональности.
Тут також йдеться про отримані эквивалентностях: два вирази є β-еквівалентними, якщо вони можуть бути β-перетворені в одне і те ж складова, а α / η-еквівалентність визначається аналогічно.
Термін redex, скорочення від приводиться обороту, відноситься до підтем, які можуть бути скорочені одним з правил. Лямбда числення для чайників, приклади:
(λ x.M) N є бета-редексом у вираженні заміни N x в M. Становить, до якого зводиться редекс, називається його редуктом. Редукція (λ x.M) N є M [x: = N].
Якщо x не є вільною в M, λ х. М х також ет-REDEX з регулятором М.
