Лямбда-числення: опис теореми, особливості, приклади

Лямбда-числення - це формальна система в математичній логіці для вираження підрахунків на основі Абстракції та застосування функцій за допомогою прив`язки та заміни змінних. Це універсальна модель, яку можна застосовувати для проектування будь-якої машини Тьюринга. Вперше введена лямбда-числення Черчем, відомим математиком, в 1930-х роках.

Система складається з побудови лямбда-членів і виконання над ними операцій скорочення.

Пояснення та Додатки

Грецька буква lambda (λ) використовується в лямбда-виразах і лямбда-термінах для позначення зв`язування змінної у функції.

Лямбда-числення може бути нетипізованим або набраним. У першому варіанті функції можуть бути застосовані тільки в тому випадку, якщо вони здатні приймати Дані цього типу. Типізовані лямбда-обчислення слабкіше, можуть виражати менше значення. Але, з іншого боку, вони дозволяють доводити більше речей.

Однією з причин того, що існує багато різних типів-це бажання вчених зробити більше, не відмовляючись від можливості доводити сильні теореми лямбда-обчислень.

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

Для чайників

Лямбда-числення була введена математиком Алонзо Черчем в 1930-х роках в рамках дослідження основ науки. Оригінальна система була показана як логічно несумісна в 1935 році, коли Стівен Клін і Дж. Б. Россер розробили парадокс Кліні-Россера.

Надалі, в 1936 році Черч виділив і опублікував тільки ту частину, яка має відношення до розрахунків, то, що зараз називається нетипізованим лямбда-обчисленням. У 1940 він також представив слабшу, але логічно послідовну теорію, відому як система простого типу. У своїй роботі він пояснює всю теорію простою мовою, тому, можна сказати, що Черч опублікував лямбду числення для чайників.

До 1960-х років, коли з`ясувалося його ставлення до мов програмування, λ стала лише формалізмом. Завдяки застосуванню Річарда Монтегю та інших лінгвістів у семантиці природної мови, числення стало почесним місцем як у лінгвістиці, так і в інформатиці.

Походження символу

Лямбда не позначає слово або абревіатуру, вона виникла, завдяки посилання в» принципової математики " Рассела, за якою слідують два друкарських зміни. Приклад позначення: для функції f з f (y) = 2Y + 1 дорівнює 2ŷ + 1. І тут використовується символ каретки (»капелюх") над y для позначення вхідної змінної.

Церква спочатку мала намір використовувати подібні символи, але набірники не змогли розмістити символ "капелюх" над літерами. Тому замість цього вони надрукували його спочатку як " /y.2y+1». У наступному епізоді редагування набірники замінили » /" на візуально подібний символ.

Введення в лямбда числення

Система складається з мови термінів, які вибираються певним формальним синтаксисом, і набору правил перетворення, які дозволяють маніпулювати ними. Останній пункт можна розглядати як екваціональну теорію або як операційне визначення.

Усі функції в лямбда-обчисленні є анонімними, тобто не мають Імен. Вони приймають лише одну вхідну змінну, при цьому каррування використовується для реалізації графіків з кількома непостійними.

Лямбда-терміни

Синтаксис обчислення визначає деякі вирази як дійсні, а інші як недійсні. Також, як різні рядки символів є допустимими програмами на Сі, а якісь-ні. Дійсний вираз лямбда-числення називається " лямбда-терміном».

Наступні три правила дають індуктивне визначення, яке можна застосовувати для побудови всіх синтаксично допустимих понять:

Змінна x сама по собі є дійсним лямбда-терміном:

• якщо T це ЛТ, і x непостійна, то (lambda xt) називається абстракцією.
• якщо T, а також S поняття, то (TS) називається додатком.

Ніщо інше не є лямбда-терміном. Таким чином, поняття дійсне тоді і тільки тоді, коли воно може бути отримано повторним застосуванням цих трьох правил. Проте деякі дужки можуть бути опущені відповідно до інших критеріїв.

Визначення

Лямбда-вирази складаються з:

• змінних v 1, v 2,..., v n,...
• символів Абстракції ` λ `і точки`.`
• дужка ().

Множина Λ, може бути визначена індуктивно:

• Якщо x змінна, то x Λ Λ;
• x непостійна і M ∈ Λ, то (λx.M) ∈ Λ;
• M, N ∈ Λ, то (MN) ∈ Λ.

Позначення

Щоб зберегти нотацію лямбда-виразів в незагромадженому вигляді, зазвичай застосовуються наступні угоди:

• Зовнішні дужки опущені: MN замість (MN).
• Передбачається, що додатки залишаються асоціативними: натомість ((MN) P) можна написати MNP.
• Тіло Абстракції простягається далі вправо: λx.MN означає λx. (MN), а не (λx.M) N.
• Скорочується послідовність абстракцій: λx.λy.λz.N можна λxyz.N.

Вільні та пов`язані змінні

Оператор λ з`єднує свою непостійну, де б він не знаходився в тілі Абстракції. Змінні, що потрапляють в область, називаються пов`язаними. У виразі λ x. М, частина λ х часто називають сполучною. Як би натякаючи, що змінні стають групою з додаванням Х х до М. Всі інші нестійкі називаються вільними.

Наприклад, у виразі λ y. х х у, у-пов`язана непостійна, а х-вільна. І також варто звернути увагу, що змінна згрупована своєю» найближчою " абстракцією. У наступному прикладі рішення лямбда-числення представлено єдиним входженням x, яке пов`язане другою складовою:

λ x. y (λ x. z x)

Множина вільних змінних M позначається як FV (M) і визначається рекурсією за структурою термінів наступним чином:

• FV (x) = {x}, де X-змінна.
• FV (λx.M) = FV (M){x}.
• FV (MN) = FV (M) ∪ FV (N).

Формула, яка не містить вільних змінних, називається закритою. Закриті лямбда-вирази також відомі як комбінатори і еквівалентні термінам у комбінаторній логіці.

Скорочення

Значення лямбда-виразів визначається тим, як вони можуть бути скорочені.

Існує три види урізання:

• α-перетворення: зміна пов`язаних змінних (альфа).
• β-редукція: застосування функцій до своїх аргументів (бета).
• η-перетворення: охоплює поняття екстенсіональності.

Тут мова також йде про отримані еквівалентності: два вирази є β-еквівалентними, якщо вони можуть бути β-перетворені в один і той же компонент, а α / η-еквівалентність визначається аналогічно.

Термін redex, скорочення від приводиться обороту, відноситься до підтем, які можуть бути скорочені одним з правил. Лямбда обчислення для чайників, приклади:

(λ x.M) N є бета-редексом у виразі заміни N на x в M. Складова, до якого зводиться редекс, називається його редуктом. Редукція (λ x.M) N є M [x: = N].

Якщо x не є вільною В M, λ х. М Х також ет-REDEX з регулятором М.

α-перетворення

Альфа-перейменування дозволяють змінювати імена пов`язаних змінних. Наприклад, λ x. х може дати λ у. у. Терміни, які відрізняються лише альфа-перетворенням, називаються α-еквівалентними. Часто при використанні лямбда-числення α-еквівалентні вважаються взаємними.

Точний правила для альфа-перетворення не зовсім тривіальні. По-перше, при даній Абстракції перейменовуються тільки ті змінні, які пов`язані з однією і тією ж системою. Наприклад, альфа-перетворення λ x.λ x. x може призвести до λ y.λ x. X, але це може не впасти до λy.λx.y останній має інший сенс, ніж оригінал. Це аналогічно поняттю програмування затінення змінних.

По-друге, альфа-перетворення неможливе, якщо воно призведе до захоплення непостійною іншою абстракцією. Наприклад, якщо замінити x на y у λ x.λ y. x, то можна отримати λ y.λ y. у, що зовсім не те ж саме.

У мовах програмування зі статичним обсягом альфа-перетворення можна використовувати для спрощення роздільної здатності імен. При цьому стежачи за тим, щоб поняття змінної не маскувало позначення В містить області.

У позначенні індексу де Брюйна будь-які два альфа-еквівалентні терміни синтаксично ідентичні.

Заміна

Зміни, написані Е [V: = R], являють собою процес заміщення всіх вільних входжень змінної V у виразі Е з оборотом R. Заміна з точки зору λ визначається лямбдою обчислення рекурсії за структурою понять наступним чином (Примітка: x і y - лише змінні, а M і N - будь-який λ-вираз).

x [x: = N] ≡ N

y [x: = N] ≡ y, якщо x ≠ y

(M 1 M 2) [x: = N] ≡ (M 1 [x: = N]) (M 2 [x: = N])

(λ x.M) [x: = N] ≡ λ x.M

(λ y.M) [x: = N] y λ y. (M [x: = N]), якщо x ≠ y, припускаючи, що y ∉ FV (N).

Для підстановки в лямбда-абстракцію іноді необхідно α-перетворити вираз. Наприклад, неправильно, щоб (λ x. Y) [y: = x] призвело до (λ x. X), оскільки заміщений x повинен був бути вільним, але врешті-решт був зв`язаний. Правильна заміна в цьому випадку (λ z. X) з точністю до α-еквівалентності. Варто звернути увагу, що заміщення визначається однозначно з вірністю до лямбди.

β-редукція

Бета-редукція відображає ідею застосування функції. Бета-відновний визначається в термінах заміщення: ((X V. E) E` ) є E [V: = E`].

Наприклад, припускаючи деяке кодування 2, 7,×, є таке β-зменшення: ((λ n. N × 2) 7) → 7 × 2.

Бета-редукція може розглядатися як така ж, як і концепція локальної зводимості при природній дедукції через ізоморфізм Каррі-Говарда.

η-перетворення

ЕТА-конверсія виражає ідею екстенсіональності, яка в цьому контексті полягає в тому, що дві функції рівні тоді, коли вони дають однаковий результат для всіх аргументів. Ця конвертація обмінюється між λ x. (F x) і f, коли x не здається вільним у f.

Дана дія може розглядатися як те ж саме, що і концепція локальної повноти в природній дедукції через ізоморфізм Каррі-Ховарда.

Нормальні форми та злиття

Для нетипізованого лямбда-числення β-редукція як правило Переписування не є ні сильно нормалізуючою, ні слабо.

Проте можна показати, що β-редукція зливається при роботі до α-перетворення (т. е. можна вважати дві нормальні форми рівними, якщо можливо α-перетворення однієї в іншу).

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

Додаткові методи програмування

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

Іменована константа

У лямбда-обчисленні бібліотека приймає форму набору раніше визначених функцій, де терміни є лише конкретними константами. Чисте числення не має поняття іменованих незмінних, оскільки всі атомні лямбда-терміни є змінними. Але їх також можна імітувати, виділивши непостійну як назву константи, використовуючи лямбда-абстракцію для зв`язування цієї мінливої в основній частині, і застосувати цю абстракцію до наміченого визначення. Таким чином, якщо використовувати f для позначення M в N, можна сказати,

(λ ф. Н) М.

Автори часто вводять синтаксичне поняття, таке як let, щоб дозволити писати все в більш інтуїтивному порядку.

f = M в N

Поєднуючи такі визначення, можна написати «програму» лямбда-числення як нуль або більше дефініцій функцій, за якими слідує один лямбда-член, використовуючи ті визначення, які складають основну частину програми.

Помітним обмеженням цього let є те, що ім`я f не визначено в M, оскільки M знаходиться поза межами області прив`язки лямбда-Абстракції f. Це означає, що атрибут рекурсивної функції не може використовуватися як M з let. Більш вдосконалена синтаксична конструкція letrec, яка дозволяє писати рекурсивні визначення функцій у цьому стилі, замість цього додатково використовує комбінатори з фіксованою точкою.

Друковані аналоги

Даний тип є типізованим формалізмом, який використовує символ для позначення анонімної функції Абстракція. У цьому контексті типи, як правило, є об`єктами синтаксичної природи, які присвоюються лямбда-термінам. Точна натура залежить від розглянутого обчислення. З певної точки зору, типізовані чи можна розглядати як уточнення нетипізованого чи. Але з іншого боку, їх також можна вважати більш фундаментальною теорією, а нетипізоване лямбда-числення-особливим випадком лише з одним типом.

Набрані Лі є основними мовами програмування та основою функціональних, таких як ML та Haskell. І, більш побічно, імперативних стилів створення. Набрані лямбда-числення відіграють важливу роль у розробці систем типів для мов програмування. Тут типізація зазвичай фіксує бажані властивості програми, наприклад, вона не спричинить порушення доступу до пам`яті.

Набрані лямбда-числення тісно пов`язані з математичною логікою та теорією доказів через ізоморфізм Каррі-Говарда, і їх можна розглядати як внутрішню мову КЛАСІВ категорій, наприклад, яка є просто стилем декартових замкнутих.