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

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


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


Ядро λ-числення грунтується трохи більше ніж на визначені [[змінна|змінних]], області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, [[семантика]] мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.<ref>Kluge 2005, сторінка 51.</ref>
Ядро λ-числення грунтується трохи більше ніж на визначені [[змінна|змінних]], області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, [[семантика]] мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.<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> - <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" в деяких мовах програмування. Вона вказує читачу що змінна після неї - не частина виразу, а формальний параметр функції що задається. Крапка після параметра позначає початок тіла функції.

{|class="wikitable"
|-
! Мова !! Приклад
|-
| Лямбда-числення || <math>\lambda x . *\ 3\ x</math>
|-
| [[Pascal]] || <source lang="pascal">function f(x: integer): integer begin f:= 3*x end;</source> (не зовсім лямбда-вираз, але суть та ж)
|-
| [[Lisp]] || <source lang="lisp">(lambda (x) (* 3 x))</source>
|-
| [[Python]] || <source lang="python">lambda x: x*3</source>
|}

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

Для зручності, ми можемо позначити нашу функцію якоюсь буквою:
:<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>

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


Рядок 32: Рядок 69:


== Джерела інформації ==
== Джерела інформації ==
*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
* 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}}
* {{cite book|назва=Abstract Computing Machines, The Lambda Calculus perspective|автор=W. Kluge|видавництво=Springer Verlag|рік=2005|isbn=3-540-21146-2}}


== Дивіться також ==
== Дивіться також ==

* [[Функціональне програмування]]
* [[Функціональне програмування]]
* [[Пі числення]]
* [[Пі числення]]
Рядок 44: Рядок 80:


=== Ресурси інтернету ===
=== Ресурси інтернету ===

* 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]])
* 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''. -- 2-nd ed. -- M.: "Center JurInfoR" Ltd., 2003. -- x+337 с. ISBN 5-89158-101-9.
* 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.
Рядок 50: Рядок 85:


{{Math-stub}}
{{Math-stub}}
{{Compu-stub}}
{{без джерел}}


[[Категорія:Числення]]
[[Категорія:Числення]]

Версія за 14:18, 7 квітня 2011

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

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

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

Запис лямбда-виразів

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

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

Якщо вираз містить змінну, то він може описувати функцію, як залежність свого значення від значення змінної, наприклад . Лямбда-числення має спеціальний синтаксис, який не зобов'язує задавати ім'я функції (як для ). Для запису функції переводимо вираз в правій частині в префіксну форму (), і дописуємо спереду "". Отримуємо . Грецька літера має роль подібну до тої що має слово "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.

Джерела інформації

  • 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. 

Дивіться також

Ресурси інтернету