Лямбда-числення

Ля́мбда-чи́слення, або λ-числення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій, а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак, Парадокс Кліні-Россера демонструє, що лямбда числення не здатне уникнути теоретико-множинних парадоксів. Не зважаючи на це, лямбда числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування.

Лямбда числення може розглядатись як ідеалізована, мінімалістича мова програмування, в цьому сенсі лямбда числення подібне до машини Тюринга, іншої мінімалістичної абстракції, здатної визначати будь-який алгоритм. Відмінність між ними полягає в тому, що лямбда числення відповідає функціональній парадигмі визначення алгоритмів, а машина Тюринга, натомість — імперативній. Тобто, машина Тюринга має певний «стан» — перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних (сталість).

Ядро λ-числення грунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.

Нотація λ-числення

Функція n змінних $v_{1},\dots ,v_{n}$ в λ-численні позначається наступним чином:

$f=\lambda v_{1}\ldots v_{n}.e_{0}$.

Символ $f$ в лівій частині цього рівняння задає назву функції, (або ідентифікатор), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає абстракцію змінних $v_{1},\ldots ,v_{n}$ від виразу $e_{0}$, котрий називається тілом абстракції. Конструкція $\lambda v_{1},\ldots ,v_{n}$ є абстрактором появи вільних змінних $v_{1},\dots ,v_{n}$ в тілі функції $e_{0}$.

Застосування функції (або абстракції) з назвою $f$ до виразу з $r$ аргументами $e_{1},\ldots ,e_{r}$ позначається:

$(fe_{1}\ldots e_{r})=(\lambda v_{1}\ldots v_{n}.e_{0}\;e_{1}\ldots e_{r})$,

Де $r$ не обов'язково має дорівнювати $n$.

Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:

$(\lambda v_{1}\ldots v_{n}.e_{0}\;v_{1}\ldots v_{n})=e_{0}$.

Задля спрощення, в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході Шонфінкеля та Каррі, n-арні абстракції можна представляти у вигляді n-кратного вкладення унарних абстракцій, тобто:

$f=\lambda v_{1}\ldots v_{n}.e_{0}\equiv \lambda v_{1}.\lambda v_{2}\ldots \lambda v_{n}.e_{0}$.

Використовуючи цю нотацію, застосування n-арної абстракції до r аргументів, наведене вище, матиме наступний вигляд:

$(f\;e_{1}\ldots e_{r})=(\dots ((f\;e_{1})\;e_{2})\;e_{r})$.

Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:

$e=_{s}v|c|(e_{0}\;e_{1})|\lambda v.e_{0}$.

Тобто, λ-вираз це: або змінна, що позначається v, константа c, застосування λ-виразу $e_{0}$ до λ-виразу $e_{1}$, або абстракція змінної v від λ-виразу $e_{0}$ відповідно.

λ-числення називається чистим, якщо множина констант порожня. В іншому випадку, числення називається аплікативним.

Джерела інформації

• 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). Abstarct Computing Machines, The Lambda Calculus perspective. Springer Verlag. ISBN 3-540-21146-2.

Дивіться також

• Функціональне програмування
• Пі числення
• Машина Тюринга
• Підстановка

Ресурси інтернету

• Raúl Rojas, A Tutorial Introduction to the Lambda Calculus(англ.) -(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.