Ля́мбда-чи́слення, або λ-чи́слення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій, а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак [en] демонструє, що лямбда-числення не здатне уникнути теоретико-множинних парадоксів. Незважаючи на це, лямбда-числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування.
Лямбда-числення можна розглядати як ідеалізовану, мінімалістичну мову програмування, у цьому сенсі лямбда-числення подібне до машини Тюрінга, іншої мінімалістичної абстракції, здатної визначати будь-який алгоритм. Відмінність між ними полягає в тому, що лямбда-числення відповідає функціональній парадигмі визначення алгоритмів, а машина Тюрінга, натомість — імперативній. Тобто, машина Тюрінга має певний «стан» — перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда-числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних (сталість).
Ядро λ-числення ґрунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.
Визначення лямбда-виразів
Множину λ-виразів можна визначити індуктивно таким чином:
- будь-яка змінна — це λ-вираз;
-абстракція
— це λ-вираз, якщо x — це змінна, а
— λ-вираз;
- аплікація
— це λ-вираз, якщо
та
— λ-вирази.
Інтуїтивно, абстракції відповідають функціям, а аплікації їх застосуванню. Особливістю лямбда-числення є те, що аргументи «функцій», визначених таким чином, — це теж функції. Наприклад, — це λ-вираз, що відповідає функції ідентичності, а
— це аплікація цієї функції до
, у випадку коли
— це теж λ-вираз.
На цій множині ми визначаємо відношення , що називається бета-редукція:
,
де означає, що вираз
підставляється всюди замість змінної x у виразі
.
Тоді, у попередньому прикладі матимемо: . Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.
Ремарка: Як і у випадку логіки першого порядку, важливо слідкувати за вільними змінними, коли йдеться про абстракцію та підстановки.
λ-вирази не такі складні, якими здаються на перший погляд. Просто треба звикнути до префіксної форми запису. Більше немає ні інфіксних (), ні постфіксних (
) операцій. Крім того, аргументи функцій просто записуються в список після функції, розділені пропуском. Тому всюди, де математики пишуть
, в лямбда-численні пишуть
. Так само замість
пишуть
, а замість
—
.
Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад, математичний вираз в лямбда-численні записується як
.
Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад . Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для
). Для запису функції переводимо вираз в правій частині в префіксну форму (
), і дописуємо спереду «
». Отримуємо
. Грецька літера
має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї — не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.
Мова | Приклад |
---|---|
Лямбда-числення | |
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 } |
Щоб застосувати створену функцію до якихось аргументів, її просто підставляють в вираз, наприклад так: . Дужки навколо функції потрібні, щоб чітко знати де вона закінчується. Якби ми написали
, то це могло б сприйматись як функція, що повертає
, якщо * — тернарний оператор, або як синтаксична помилка, якщо * — завжди бінарне.
Для зручності ми можемо позначити нашу функцію якоюсь буквою:
і потім просто писати .
Залишилось розглянути ще один цікавий випадок:
якщо передати , то вона поверне нашу стару функцію
. Тобто
працює як
, якій ми можемо передати наприклад 4, записавши це як
. Або, ми можемо розглядати її як функцію від двох аргументів.
Можна записати це в скороченій формі, без дужок:
Чи ще коротше:
Наступний розділ цієї статті пояснює те ж саме, але трохи в іншому стилі.
Нотація λ-числення
Функція n змінних в λ-численні позначається так:
.
Символ в лівій частині цього рівняння задає назву функції, (або ідентифікатор), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає абстракцію змінних
від виразу
, котрий називається тілом абстракції. Конструкція
є абстрактором появи вільних змінних
в тілі функції
.
Застосування функції (або абстракції) з назвою до виразу з
аргументами
позначається:
,
Де не обов'язково має дорівнювати
.
Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:
.
Задля спрощення в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході Шейнфінкеля та Каррі, n-арні абстракції можна представляти у вигляді n-кратного вкладення унарних абстракцій, тобто:
.
Використовуючи цю нотацію, застосування n-арної абстракції до r аргументів, наведене вище, матиме такий вигляд:
.
Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:
.
Тобто, λ-вираз це: або змінна, що позначається v, константа c, застосування λ-виразу до λ-виразу
, або абстракція змінної v від λ-виразу
відповідно.
λ-числення називається чистим, якщо множина констант порожня. В іншому випадку числення називається аплікативним.
Див. також
Примітки
- Henk Barendregt 1997
- Kluge 2005, сторінка 51.
- 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 с. .
![]() | Це незавершена стаття про інформаційні технології. Ви можете проєкту, виправивши або дописавши її. |
![]() | Це незавершена стаття з математики. Ви можете проєкту, виправивши або дописавши її. |