Лямбда-числення — це формальна система в математичній логіці для вираження підрахунків на основі абстракції і застосування функцій з використанням прив’язки і заміни змінних. Це універсальна модель, яку можна застосовувати для проектування будь-якої машини Тюрінга. Вперше введена лямбда-числення Черчем, відомим математиком, у 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. х, але це може не призвести до λ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) Е ‘) є Е [V: = Е’].
Наприклад, припускаючи деякий кодування 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. І, більш опосередковано, імперативних стилів створення. Типізовані лямбда-числення відіграють важливу роль у розробці систем типів мов програмування. Тут типизируемость зазвичай захоплює бажані властивості програми, наприклад, вона не викличе порушення доступу до пам’яті.
Типізовані лямбда-числення тісно пов’язані з математичною логікою і теорією доказів через ізоморфізм Каррі – Говарда, і їх можна розглядати як внутрішній мова класів категорій, наприклад, який просто є стилем декартових замкнутих.
