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

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

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

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

Визначення лямбда-виразів

Множину λ-виразів можна визначити індуктивно таким чином:

• будь-яка змінна — це λ-вираз;

• $\lambda$-абстракція $\lambda x.M$ — це λ-вираз, якщо x — це змінна, а $M$ — λ-вираз;

• аплікація $MN$ — це λ-вираз, якщо $M$ та $N$ — λ-вирази.

Інтуїтивно, абстракції відповідають функціям, а аплікації їх застосуванню. Особливістю лямбда-числення є те, що аргументи «функцій», визначених таким чином, — це теж функції. Наприклад, $\lambda x.x$ — це λ-вираз, що відповідає функції ідентичності, а $\lambda x.xM$ — це аплікація цієї функції до $M$, у випадку коли $M$ — це теж λ-вираз.

На цій множині ми визначаємо відношення $\rightarrow _{\beta }$, що називається бета-редукція:

$(\lambda xM)N\rightarrow _{\beta }M[x:=N]$,

де $M[x:=N]$ означає, що вираз $N$ підставляється всюди замість змінної x у виразі $M$.

Тоді, у попередньому прикладі матимемо: $(\lambda x.x)M\rightarrow _{\beta }x[x:=M]=M$. Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.

Ремарка: Як і у випадку логіки першого порядку, важливо слідкувати за вільними змінними, коли йдеться про абстракцію та підстановки.

λ-вирази не такі складні, як здаються на перший погляд. Просто треба звикнути до префіксної форми запису. Більше немає ні інфіксних ($+,\,-$), ні постфіксних ($x^{2}$) операцій. Крім того, аргументи функцій просто записуються в список після функції, розділені пропуском. Тому всюди, де математики пишуть $\sin(x)$, в лямбда-численні пишуть $\sin x$. Так само замість $x\ +\ y$ пишуть $+\ x\ y$, а замість $x^{2}$ — $*\ x\ x$.

Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад математичний вираз $\sin(x)+4$ в лямбда-численні записується як $+\ (\sin x)\ 4$.

Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад $f(x)=3x$. Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для $f$). Для запису функції переводимо вираз в правій частині в префіксну форму ($*\ 3\ x$), і дописуємо спереду «$\lambda x.$». Отримуємо $\lambda x.\ *\ 3\ x$. Грецька літера $\lambda$ має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї — не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.

Мова	Приклад
Лямбда-числення	$\lambda x.*\ 3\ x$
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 }

Щоб застосувати створену функцію до якихось аргументів, її просто підставляють в вираз, наприклад так: $(\lambda x.*\ 3\ x)4$. Дужки навколо функції потрібні, щоб чітко знати де вона закінчується. Якщо б ми написали $\lambda x.*\ 3\ x4$ то це могло б сприйматись як функція, що повертає $3*x*4==12x$, якщо * — тернарний оператор, або як синтаксична помилка, якщо * — завжди бінарне.

Для зручності ми можемо позначити нашу функцію якоюсь буквою:

$F\equiv \lambda x.*\ 3\ x$

і потім просто писати $F4$.

Залишилось розглянути ще один цікавий випадок:

$N\equiv \lambda y.(\lambda x.*\ y\ x)$

якщо передати $N\ 3$, то вона поверне нашу стару функцію $\lambda x.*\ 3\ x$. Тобто $N3$ працює як $F$, якій ми можемо передати наприклад 4, записавши це як $N\ 3\ 4$. Або, ми можемо розглядати її як функцію від двох аргументів.

Можна записати це в скороченій формі, без дужок:

$\lambda y.\lambda x.*\ x\ y$

Чи ще коротше:

$\lambda y\ x.*\ x\ y$

Наступний розділ цієї статті пояснює те ж саме, але трохи в іншому стилі.

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

Функція 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}$ відповідно.

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

Див. також

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

Література

• Achim Jung, A Short Introduction to the Lambda Calculus-(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(англ.) -(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.