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

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

Література

  • 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.