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

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

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

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

Запис лямбда-виразів

Вони не такі складні, як здаються на перший погляд. Просто треба трохи звикнути до префіксної форми запису. Більше немає ні інфіксних ($+,\, -$), ні постфіксних ($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

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

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

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

і потім просто писати $F 4$.

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

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

якщо передати $N\ 3$, то вона поверне нашу стару функцію $\lambda x . *\ 3\ x$. Тобто $N 3$ працює як $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$ позначається:

$(f e_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.

Це незавершена стаття про комп'ютери. Ви можете допомогти проекту, виправивши або дописавши її.