Лямбда-числення
Матеріал з Вікіпедії — вільної енциклопедії.
Ля́мбда-чи́слення, або λ-чи́слення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій, а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак Парадокс Кліні-Россера[en] демонструє, що лямбда-числення не здатне уникнути теоретико-множинних парадоксів. Незважаючи на це, лямбда-числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування[1].
Лямбда-числення можна розглядати як ідеалізовану, мінімалістичну мову програмування, у цьому сенсі лямбда-числення подібне до машини Тюрінга, іншої мінімалістичної абстракції, здатної визначати будь-який алгоритм. Відмінність між ними полягає в тому, що лямбда-числення відповідає функціональній парадигмі визначення алгоритмів, а машина Тюрінга, натомість — імперативній. Тобто, машина Тюрінга має певний «стан» — перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда-числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних (сталість).
Ядро λ-числення ґрунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови[2].
Множину λ-виразів можна визначити індуктивно таким чином[3]:
- будь-яка змінна — це λ-вираз;
- -абстракція — це λ-вираз, якщо x — це змінна, а — λ-вираз;
- аплікація — це λ-вираз, якщо та — λ-вирази.
Інтуїтивно, абстракції відповідають функціям, а аплікації їх застосуванню. Особливістю лямбда-числення є те, що аргументи «функцій», визначених таким чином, — це теж функції. Наприклад, — це λ-вираз, що відповідає функції ідентичності, а — це аплікація цієї функції до , у випадку коли — це теж λ-вираз.
На цій множині ми визначаємо відношення , що називається бета-редукція:
- ,
де означає, що вираз підставляється всюди замість змінної x у виразі .
Тоді, у попередньому прикладі матимемо: . Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.
Ремарка: Як і у випадку логіки першого порядку, важливо слідкувати за вільними змінними, коли йдеться про абстракцію та підстановки.
λ-вирази не такі складні, якими здаються на перший погляд. Просто треба звикнути до префіксної форми запису. Більше немає ні інфіксних (), ні постфіксних () операцій. Крім того, аргументи функцій просто записуються в список після функції, розділені пропуском. Тому всюди, де математики пишуть , в лямбда-численні пишуть . Так само замість пишуть , а замість — .
Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад, математичний вираз в лямбда-численні записується як .
Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад . Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для ). Для запису функції переводимо вираз в правій частині в префіксну форму (), і дописуємо спереду «». Отримуємо . Грецька літера має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї — не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.
Мова | Приклад |
---|---|
Лямбда-числення | |
Pascal | function f(x: integer): integer begin f:= 3*x end;
|
Lisp | (lambda (x) (* 3 x))
|
Python | lambda x: x*3
|
C++11 | [](int x) { return x * 3 }
|
Swift | { return $0 * 3 }
|
Щоб застосувати створену функцію до якихось аргументів, її просто підставляють в вираз, наприклад так: . Дужки навколо функції потрібні, щоб чітко знати де вона закінчується. Якби ми написали , то це могло б сприйматись як функція, що повертає , якщо * — тернарний оператор, або як синтаксична помилка, якщо * — завжди бінарне.
Для зручності ми можемо позначити нашу функцію якоюсь буквою:
і потім просто писати .
Залишилось розглянути ще один цікавий випадок:
якщо передати , то вона поверне нашу стару функцію . Тобто працює як , якій ми можемо передати наприклад 4, записавши це як . Або, ми можемо розглядати її як функцію від двох аргументів.
Можна записати це в скороченій формі, без дужок:
Чи ще коротше:
Наступний розділ цієї статті пояснює те ж саме, але трохи в іншому стилі.
Функція n змінних в λ-численні позначається так:
- .
Символ в лівій частині цього рівняння задає назву функції, (або ідентифікатор), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає абстракцію змінних від виразу , котрий називається тілом абстракції. Конструкція є абстрактором появи вільних змінних в тілі функції .
Застосування функції (або абстракції) з назвою до виразу з аргументами позначається:
- ,
Де не обов'язково має дорівнювати .
Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:
- .
Задля спрощення в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході Шейнфінкеля та Каррі, n-арні абстракції можна представляти у вигляді n-кратного вкладення унарних абстракцій, тобто:
- .
Використовуючи цю нотацію, застосування n-арної абстракції до r аргументів, наведене вище, матиме такий вигляд:
- .
Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:
- .
Тобто, λ-вираз це: або змінна, що позначається v, константа c, застосування λ-виразу до λ-виразу , або абстракція змінної v від λ-виразу відповідно.
λ-числення називається чистим, якщо множина констант порожня. В іншому випадку числення називається аплікативним.
- Типізоване лямбда-числення
- Система F
- Функційне програмування
- Пі-числення
- Машина Тюрінга
- Підстановка
- Лямбда-куб
- Achim Jung, A Short Introduction to the Lambda Calculus [Архівовано 23 квітня 2021 у Wayback Machine.]-(PDF)
- Henk Barendregt, The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997. The Impact of the Lambda Calculus in Logic and Computer Science
- W. Kluge (2005). Abstract Computing Machines, The Lambda Calculus perspective. Springer Verlag. ISBN 3-540-21146-2.
- Raúl Rojas, A Tutorial Introduction to the Lambda Calculus [Архівовано 1 листопада 2013 у Wayback Machine.](англ.) -(PDF)
- Wolfengagen, V.E. Combinatory logic in programming. Computations with objects through examples and exercises. — 2-nd ed. — M.: «Center JurInfoR» Ltd., 2003. — x+337 с. ISBN 5-89158-101-9.
![]() |
Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її. |
![]() |
Це незавершена стаття з математики. Ви можете допомогти проєкту, виправивши або дописавши її. |
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.