Лямбда-терміни
Синтаксис обчислення визначає деякі вирази як допустимі, а інші — як недійсні. Також, як різні рядки символів є допустимими програмами на Сі, а якісь-ні. Дійсне вираження лямбда-числення називається лямбда-терміном».
Наступні три правила дають індуктивне визначення, яке можна застосовувати для побудови всіх синтаксично допустимих понять:
Змінна x сама по собі є дійсним лямбда-терміном:
- якщо T це ЛТ, і x непостійна, то (lambda xt) називається абстракцією.
- якщо T, а також поняття s (TS) називається додатком.
Ніщо інше не є лямбда-терміном. Таким чином, поняття дійсно тоді і тільки тоді, коли воно може бути отримано повторним застосуванням цих трьох правил. Тим не менш, деякі дужки можуть бути опущені відповідно з іншими критеріями.
Визначення
Лямбда-вирази складаються з:
- змінних v 1, v 2,…, v n,…
- символів абстракції ‘λ’ і точки ‘.’
- дужки ().
Безліч Λ, може бути визначено індуктивно:
- Якщо змінна x, то x ∈ Λ;
- x непостійна і M ∈ Λ, (λx.M) ∈ Λ;
- M, N ∈ Λ, (MN) ∈ Λ.
