Перегляд вихідного коду сторінки Лямбда-числення

'''Ля́мбда-чи́слення''', або '''λ-числення'''&nbsp;— [[формальна система]], що використовується в теоретичній [[кібернетика|кібернетиці]] для дослідження визначення [[Функція (математика)|функції]], застосування функції, та [[Рекурсія|рекурсії]]. Це числення було запропоноване [[Черч Алонсо|Алонсо Черчем]] та [[Коул Кліні Стівен|Стівеном Кліні]] в [[1930-ті]] роки, як частина більшої спроби розробити базис [[математика|математики]] на основі функцій, а не [[Множина|множин]] (задля уникнення таких перешкод, як [[Парадокс Рассела]]). Однак {{Нп|Парадокс Кліні-Россера||en|Kleene–Rosser paradox}} демонструє, що лямбда-числення не здатне уникнути теоретико-множинних парадоксів. Незважаючи на це, лямбда-числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми [[функціональне програмування|функціонального програмування]]<ref>Henk Barendregt 1997</ref>.

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

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

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

Множину λ-виразів можна визначити індуктивно таким чином<ref> M.H. Sorensen and P. Urzyczyn «Lectures on the Curry-Howard Isomorphism» (2006) </ref>:

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

* <math> \lambda </math>-''абстракція'' <math> \lambda x.M </math>&nbsp;— це λ-вираз, якщо ''x''&nbsp;— це змінна, а <math> M </math>&nbsp;— λ-вираз;

* ''аплікація'' <math> MN </math>&nbsp;— це λ-вираз, якщо <math> M </math> та <math> N </math>&nbsp;— λ-вирази.

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

На цій множині ми визначаємо відношення <math> \rightarrow_\beta </math>, що називається ''бета-редукція'':

<math> (\lambda x M)N \rightarrow_\beta M[x:=N] </math>,

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

Тоді, у попередньому прикладі матимемо: <math> (\lambda x.x) M \rightarrow_\beta x [x:=M] = M </math>. Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.

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

λ-вирази не такі складні, як здаються на перший погляд. Просто треба звикнути до префіксної форми запису. Більше немає ні інфіксних (<math>+,\, -</math>), ні постфіксних (<math>x^2</math>) операцій. Крім того, аргументи функцій просто записуються в список після функції, розділені пропуском. Тому всюди, де математики пишуть <math>\sin(x)</math>, в лямбда-численні пишуть <math>\sin x</math>. Так само замість <math>x\ +\ y</math> пишуть <math>+\ x\ y</math>, а замість <math>x^2</math>&nbsp;— <math>*\ x\ x</math>.

Хоча дужки таки не пропадають. Вони використовуються для групування. Наприклад математичний вираз <math>\sin (x) + 4</math> в лямбда-численні записується як <math>+\ (\sin x)\ 4</math>.

Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад <math>f(x) = 3x</math>. Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для <math>f</math>). Для запису функції переводимо вираз в правій частині в префіксну форму (<math>*\ 3\ x</math>), і дописуємо спереду «<math>\lambda x .</math>». Отримуємо <math>\lambda x .\ *\ 3\ x</math>. Грецька літера <math>\lambda</math> має роль, подібну до тої що має слово «function» в деяких мовах програмування. Вона вказує читачу що змінна після неї&nbsp;— не частина виразу, а формальний параметр функції, що задається. Крапка після параметра позначає початок тіла функції.

{|class="wikitable"
|-
! Мова !! Приклад
|-
| Лямбда-числення || <math>\lambda x . *\ 3\ x</math>
|-
| [[Pascal]] || <syntaxhighlight lang="pascal">function f(x: integer): integer  begin f:= 3*x end;</syntaxhighlight> (не зовсім лямбда-вираз, оскільки є назва функції, але суть та ж)
|-
| [[Lisp]] || <syntaxhighlight lang="lisp">(lambda (x) (* 3 x))</syntaxhighlight>
|-
| [[Python]] || <syntaxhighlight lang="python">lambda x: x*3</syntaxhighlight>
|-
|[[C++11]]
|<syntaxhighlight lang="c++">
 [](int x) { return x * 3 }
</syntaxhighlight>
|-
|[[Swift (мова програмування)|Swift]]
|<syntaxhighlight lang="swift">
  { return $0 * 3 }
</syntaxhighlight>
|}

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

Для зручності ми можемо позначити нашу функцію якоюсь буквою:
: <math>F \equiv \lambda x . *\ 3\ x</math>
і потім просто писати <math>F 4</math>.

Залишилось розглянути ще один цікавий випадок:
: <math>N \equiv \lambda y . ( \lambda x . *\ y\ x) </math>
якщо передати <math>N\ 3</math>, то вона поверне нашу стару функцію <math>\lambda x . *\ 3\ x</math>. Тобто <math>N 3</math> працює як <math>F</math>, якій ми можемо передати наприклад 4, записавши це як <math>N\ 3\ 4</math>. Або, ми можемо розглядати її як функцію від двох аргументів.

Можна записати це в скороченій формі, без дужок:
: <math>\lambda y . \lambda x . *\ x\ y</math>

Чи ще коротше:
: <math>\lambda y\ x.*\ x\ y</math>

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

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

Функція ''n'' змінних <math>v_1, \dots, v_n</math> в λ-численні позначається так:
: <math>f = \lambda v_1\ldots v_n . e_0</math>.
Символ <math>f</math> в лівій частині цього рівняння задає ''назву'' функції, (або ''ідентифікатор''), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає ''абстракцію'' змінних <math>v_1, \ldots, v_n</math> від виразу <math>e_0</math>, котрий називається ''тілом абстракції''. Конструкція <math>\lambda v_1, \ldots, v_n</math> є ''абстрактором'' появи [[вільна змінна|вільних змінних]] <math>v_1, \dots, v_n</math> в тілі функції <math>e_0</math>.

''Застосування'' функції (або абстракції) з назвою <math>f</math> до виразу з <math>r</math> аргументами <math>e_1, \ldots, e_r</math> позначається:
: <math>(f e_1\ldots e_r) = (\lambda v_1\ldots v_n.e_0\; e_1\ldots e_r)</math>,
Де <math>r</math> не обов'язково має дорівнювати <math>n</math>.

Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:
: <math>(\lambda v_1\ldots v_n.e_0\; v_1\ldots v_n) = e_0</math>.

Задля спрощення в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході {{Не перекладено|Шейнфінкель Мойсей Ейлєвич|Шейнфінкеля|ru|Шейнфинкель, Моисей Эльевич}} та [[Гаскелл Каррі|Каррі]], ''n''-арні абстракції можна представляти у вигляді ''n''-кратного вкладення унарних абстракцій, тобто:
: <math>f = \lambda v_1\ldots v_n . e_0 \equiv \lambda v_1.\lambda v_2\ldots \lambda v_n . e_0</math>.
Використовуючи цю нотацію, застосування ''n''-арної абстракції до ''r'' аргументів, наведене вище, матиме такий вигляд:
: <math>(f\; e_1\ldots e_r) = (\dots ((f\; e_1)\; e_2)\; e_r)</math>.
Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:
: <math>e =_s v | c | (e_0\; e_1) | \lambda v.e_0</math>.
Тобто, λ-вираз це: або змінна, що позначається ''v'', константа ''c'', застосування λ-виразу <math>e_0</math> до λ-виразу <math>e_1</math>, або абстракція змінної ''v'' від λ-виразу <math>e_0</math> відповідно.

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

== Див. також ==
* [[Типізоване лямбда-числення]]
* [[Функційне програмування]]
* [[Пі-числення]]
* [[Машина Тюринга]]
* [[Підстановка]]
* [[Лямбда-куб]]

== Примітки ==
{{reflist}}

== Література ==
* Achim Jung, ''[http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf A Short Introduction to the Lambda Calculus] {{Webarchive|url=https://web.archive.org/web/20210423225252/https://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf |date=23 квітня 2021 }}''-([[Portable Document Format|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|назва=Abstract Computing Machines, The Lambda Calculus perspective|автор=W. Kluge|видавництво=Springer Verlag|рік=2005|isbn=3-540-21146-2}}
* [[Raúl Rojas]], ''[http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf A Tutorial Introduction to the Lambda Calculus] {{Webarchive|url=https://web.archive.org/web/20131101143623/http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf |date=1 листопада 2013 }}''{{ref-en}} -([[Portable Document Format|PDF]])
* Wolfengagen, V.E. '' Combinatory logic in programming. Computations with objects through examples and exercises''.&nbsp;— 2-nd ed.&nbsp;— M.: «Center JurInfoR» Ltd., 2003.&nbsp;— x+337 с. ISBN 5-89158-101-9.

{{comp-stub}}
{{Math-stub}}

[[Категорія:Лямбда-числення]]
[[Категорія:Теоретична інформатика]]
[[Категорія:Моделі обчислень]]
[[Категорія:Статті з прикладами коду мовою Python]]
[[Категорія:Статті з прикладами коду мовою Lisp]]
[[Категорія:Статті з прикладами коду мовою Pascal]]
[[Категорія:Статті з прикладами коду мовою Swift]]
[[Категорія:Статті з прикладами коду мовою C++]]