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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

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

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

Запис лямбда-виразів[ред.ред. код]

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

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

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

Мова Приклад
Лямбда-числення \lambda x . *\ 3\ x
Pascal
function f(x: integer): integer  begin f:= 3*x end;
(не зовсім лямбда-вираз, але суть та ж)
Lisp
(lambda (x) (* 3 x))
Python
lambda x: x*3

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

Для зручності, ми можемо позначити нашу функцію якоюсь буквою:

F \equiv \lambda x . *\ 3\ x

і потім просто писати F 4.

Залишилось розглянути ще один цікавий випадок:

N \equiv \lambda y . ( \lambda x . *\ y\ x)

якщо передати N\ 3, то вона поверне нашу стару функцію \lambda x . *\ 3\ x. Тобто N 3 працює як F, якій ми можемо передати наприклад 4, записавши це як N\ 3\ 4. Або, ми можемо розглядати її як функцію від двох аргументів.

Можна записати це в скороченій формі, без дужок:

\lambda y . \lambda x . *\ x\ y

Чи ще коротше:

\lambda y\ x.*\ x\ y

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

Нотація λ-числення[ред.ред. код]

Функція n змінних v_1, \dots, v_n в λ-численні позначається так:

f = \lambda v_1\ldots v_n . e_0.

Символ f в лівій частині цього рівняння задає назву функції, (або ідентифікатор), за яким можна посилатись на цю функцію в інших виразах. Вираз у правій частині рівняння визначає абстракцію змінних v_1, \ldots, v_n від виразу e_0, котрий називається тілом абстракції. Конструкція \lambda v_1, \ldots, v_n є абстрактором появи вільних змінних v_1, \dots, v_n в тілі функції e_0.

Застосування функції (або абстракції) з назвою f до виразу з r аргументами e_1, \ldots, e_r позначається:

(f e_1\ldots e_r) = (\lambda v_1\ldots v_n.e_0\; e_1\ldots e_r),

Де r не обов'язково має дорівнювати n.

Особливим випадком є застосування абстракції до абстрагованих змінних, що повертає тіло абстракції:

(\lambda v_1\ldots v_n.e_0\; v_1\ldots v_n) = e_0.

Задля спрощення, в λ-численні розглядаються функції від однієї змінної. Як було показано у винаході Шонфінкеля та Каррі, n-арні абстракції можна представляти у вигляді n-кратного вкладення унарних абстракцій, тобто:

f = \lambda v_1\ldots v_n . e_0 \equiv \lambda v_1.\lambda v_2\ldots \lambda v_n . e_0.

Використовуючи цю нотацію, застосування n-арної абстракції до r аргументів, наведене вище, матиме такий вигляд:

(f\; e_1\ldots e_r) = (\dots ((f\; e_1)\; e_2)\; e_r).

Такий підхід скорочує побудову виразів λ-числення до наступних синтаксичних правил:

e =_s v | c | (e_0\; e_1) | \lambda v.e_0.

Тобто, λ-вираз це: або змінна, що позначається v, константа c, застосування λ-виразу e_0 до λ-виразу e_1, або абстракція змінної v від λ-виразу e_0 відповідно.

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

Примітки[ред.ред. код]

  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. 

Див. також[ред.ред. код]

Посилання[ред.ред. код]


Комп'ютер Це незавершена стаття про комп'ютери.
Ви можете допомогти проекту, виправивши або дописавши її.