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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

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

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

Визначення лямбда-виразів[ред.ред. код]

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

  • будь-яка змінна — це λ-вираз;
  • -абстракція  — це λ-вираз, якщо x — це змінна, а  — λ-вираз;
  • аплікація  — це λ-вираз, якщо та  — λ-вирази.

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

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

,

де означає, що вираз підставляється всюди замість змінної x у виразі .

Тоді, у попередньому прикладі матимемо: . Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.

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

λ-вирази не такі складні, як здаються на перший погляд. Просто треба звикнути до префіксної форми запису. Більше немає ні інфіксних (), ні постфіксних () операцій. Крім того, аргументи функцій просто записуються в список після функції, розділені пропуском. Тому всюди, де математики пишуть , в лямбда-численні пишуть . Так само замість пишуть , а замість  — .

Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад математичний вираз в лямбда-численні записується як .

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

Мова Приклад
Лямбда-числення
Pascal
function f(x: integer): integer  begin f:= 3*x end;
(не зовсім лямбда-вираз, але суть та ж)
Lisp
(lambda (x) (* 3 x))
Python
lambda x: x*3

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

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

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

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

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

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

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

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

Нотація λ-числення[ред.ред. код]

Функція n змінних в λ-численні позначається так:

.

Символ в лівій частині цього рівняння задає назву функції, (або ідентифікатор), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає абстракцію змінних від виразу , котрий називається тілом абстракції. Конструкція є абстрактором появи вільних змінних в тілі функції .

Застосування функції (або абстракції) з назвою до виразу з аргументами позначається:

,

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

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

.

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

.

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

.

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

.

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

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

Примітки[ред.ред. код]

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

Література[ред.ред. код]

Див. також[ред.ред. код]


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