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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Мова	Приклад
Лямбда-числення	${\displaystyle \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
	[](int x) { return x * 3 }
Swift	{ return $0 * 3 }

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

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

${\displaystyle F\equiv \lambda x.*\ 3\ x}$

і потім просто писати ${\displaystyle F4}$.

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

${\displaystyle N\equiv \lambda y.(\lambda x.*\ y\ x)}$

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

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

${\displaystyle \lambda y.\lambda x.*\ x\ y}$

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

${\displaystyle \lambda y\ x.*\ x\ y}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Див. також

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

Примітки

1. Henk Barendregt 1997
2. Kluge 2005, сторінка 51.
3. M.H. Sorensen and P. Urzyczyn «Lectures on the Curry-Howard Isomorphism» (2006)

Література

• 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 .
• 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 с. .