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

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

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

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

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

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

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

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

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

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

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

(λ x M) N \to_{β} M [x : = N]

,

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

Тоді, у попередньому прикладі матимемо: $(λ x . x) M \to_{β} 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) = 3 x$ . Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для $f$ ). Для запису функції переводимо вираз в правій частині в префіксну форму ( $* 3 x$ ), і дописуємо спереду « $λ x .$ ». Отримуємо $λ x . * 3 x$ . Грецька літера $λ$ має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї — не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.

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

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

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

F \equiv λ x . * 3 x

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

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

N \equiv λ y . (λ x . * y x)

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

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

λ y . λ x . * x y

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

λ y x . * x y

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

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

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

f = λ v_{1} \dots v_{n} . e_{0}

.

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

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

(f e_{1} \dots e_{r}) = (λ v_{1} \dots v_{n} . e_{0} e_{1} \dots e_{r})

,

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

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

(λ v_{1} \dots v_{n} . e_{0} v_{1} \dots v_{n}) = e_{0}

.

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

f = λ v_{1} \dots v_{n} . e_{0} \equiv λ v_{1} . λ v_{2} \dots λ v_{n} . e_{0}

.

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

(f e_{1} \dots e_{r}) = (\dots ((f e_{1}) e_{2}) e_{r})

.

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

e =_{s} v | c | (e_{0} e_{1}) | λ v . e_{0}

.

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

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

Див. також

Примітки

Шаблон:Reflist

Література

Achim Jung, A Short Introduction to the Lambda Calculus Шаблон:Webarchive-(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
Шаблон:Cite book
Raúl Rojas, A Tutorial Introduction to the Lambda Calculus Шаблон:WebarchiveШаблон:Ref-en -(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.

Шаблон:Comp-stub Шаблон:Math-stub

Шаблон:Математична логіка

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

[1] Henk Barendregt 1997

[2] Kluge 2005, сторінка 51.

[3] M.H. Sorensen and P. Urzyczyn «Lectures on the Curry-Howard Isomorphism» (2006)

[1]

[2]

[3]

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

Зміст

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

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

Див. також

Примітки

Література

Навігаційне меню

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

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

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

Див. також

Примітки

Література

Навігаційне меню

Пошук