β-редукція
Бета-редукція відображає ідею застосування функції. Бета-відновлювальний визначається в термінах заміщення: ((X V. E) Е ‘) є Е [V: = Е’].
Наприклад, припускаючи деякий кодування 2, 7, ×, є наступне β-зменшення: ((λ n. N × 2) 7) → 7 × 2.
Бета-редукція може розглядатися як те ж саме, що і концепція локальної сводимости при природній дедукції через ізоморфізм Каррі – Ховарда.
η-перетворення
Ця-конверсія виражає ідею экстенсиональности, яка в цьому контексті полягає в тому, що дві функції дорівнюють тоді, коли вони дають однаковий результат для всіх аргументів. Ця конвертація обмінює між λ x. (F x) і f всякий раз, коли x не здається вільним f.
Дана дія може розглядатися як те ж саме, що і концепція локальної повноти в природному дедукції через ізоморфізм Каррі – Ховарда.
Нормальні форми і злиття
Для нетипізованого лямбда-числення β-редукція як правило переписування не є ні сильно нормалізує, ні слабо.
Тим не менше можна показати, що β-редукція зливається при роботі до α-перетворення (т. е. можна вважати дві нормальні форми рівними, якщо можливо α-перетворення однієї в іншу).
Тому і сильно нормалізують члени, і слабо налагоджують поняття мають єдину нормальну форму. Для перших термінів будь-яка стратегія скорочення гарантовано призведе до типової конфігурації. Тоді як для слабко нормалізують умов деякі стратегії скорочення можуть не знайти її.
