Позначення
Щоб зберегти позначення лямбда-виразів в незагроможденном вигляді, зазвичай застосовуються наступні угоди:
- Зовнішні дужки опущені: MN замість (MN).
- Передбачається, що програми залишаються асоціативними: замість ((MN) P) можна написати MNP.
- Тіло абстракції простягається далі вправо: λx.MN означає λx. (MN), а не (λx.M) N.
- Скорочується послідовність абстракцій: λx.λy.λz.N можна λxyz.N.
Вільні і зв’язані змінні
Оператор λ з’єднує свою мінливу, де б він ні знаходився в тілі абстракції. Змінні, що потрапляють в область, називаються пов’язаними. У виразі λ x. М, частина λ х часто називають зв’язуючим. Як би натякаючи, що змінні стають групою з додаванням Х до М. Всі інші нестійкі називаються вільними.
Наприклад, у виразі λ y. х х у, у — пов’язана непостійна, а х – вільна. І також варто звернути увагу, що змінна згрупована своєї «найближчій» абстракцією. У наступному прикладі рішення лямбда-числення представлено єдиним входженням x, яке пов’язане другої складової:
λ x. y (λ x. z x)
Безліч вільних змінних M позначається як FV (M) і визначається рекурсією за структурою термінів наступним чином:
- FV (x) = {x}, де x – змінна.
- FV (λx.M) = FV (M) {x}.
- FV (MN) = FV (M) ∪ FV (N).
Формула, яка не містить вільних змінних, називається закритою. Замкнуті лямбда-вирази, також відомі як комбінатори і еквівалентні термінів у комбінаторної логіки.
