Відкрити головне меню

Ля́мбда-чи́слення, або λ-числення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 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
C++11
 [](int x) { return x * 3 }
Swift
  { return $0 * 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)

ЛітератураРедагувати

Див. такожРедагувати