Відмінності між версіями «Лямбда-числення»

м
Розтлумачено Функція як Функція (математика), додано шаблон "Не перекладено" для Парадокс Кліні-Россера, вікіфікатор
м (Вилучення 30 інтервікі, відтепер доступних на Вікіданих: d:q242028)
м (Розтлумачено Функція як Функція (математика), додано шаблон "Не перекладено" для Парадокс Кліні-Россера, вікіфікатор)
'''Ля́мбда-чи́слення''', або '''λ-числення'''&nbsp;— [[формальна система]], що використовується в теоретичній [[кібернетика|кібернетиці]] для дослідження визначення [[Функція (математика)|функції]], застосування функції, та [[Рекурсія|рекурсії]]. Це числення було запропоноване [[Черч Алонсо|Алонсо Черчем]] та [[Коул Кліні Стівен|Стівеном Кліні]] в [[1930-ті]] роки, як частина більшої спроби розробити базис [[математика|математики]] на основі функцій, а не [[Множина|множин]] (задля уникнення таких перешкод, як [[Парадокс Рассела]]). Однак, [[{{Не перекладено|треба=Парадокс Кліні-Россера]]|є=:en:Kleene–Rosser paradox}} демонструє, що лямбда числення не здатне уникнути теоретико-множинних парадоксів. Не зважаючи на це, лямбда числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми [[функціональне програмування|функціонального програмування]]<ref>Henk Barendregt 1997</ref>.
 
Лямбда числення може розглядатись як ідеалізована, мінімалістича [[мова програмування]], в цьому сенсі лямбда числення подібне до [[Машина Тюринга|машини Тюринга]], іншої мінімалістичної абстракції, здатної визначати будь-який [[алгоритм]]. Відмінність між ними полягає в тому, що лямбда числення відповідає [[функціональне програмування|функціональній парадигмі]] визначення алгоритмів, а машина Тюринга, натомість &nbsp;— [[Імперативне програмування|імперативній]]. Тобто, машина Тюринга має певний «стан» &nbsp;— перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних ([[Незмінний об'єкт|сталість]]).
 
Ядро λ-числення ґрунтується трохи більше ніж на визначені [[змінна|змінних]], області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, [[семантика]] мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.<ref>Kluge 2005, сторінка 51.</ref>
 
== Запис лямбда-виразів ==
Вони не такі складні, як здаються на перший погляд. Просто треба трохи звикнути до префіксної форми запису. Більше немає ні інфіксних (<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>
|}
 
Щоб застосувати створену функцію до якихось аргументів, її просто підставляють в вираз, наприклад так: <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>.
 
Задля спрощення, в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході Шонфінкеля та Каррі, ''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> відповідно.
 
 
== Джерела інформації ==
* Achim Jung, ''[http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf A Short Introduction to the Lambda Calculus]''-([[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]''{{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}}