Комбінаторна логіка — це нотація для усунення необхідності кількісних змінних в математичній логіці. Вона була введена Мойсеєм Шейнфінкелем Translated by Stefan Bauer-Mengelberg as «On the building blocks of mathematical logic» in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press: 355–66. і Гаскеллем Каррі, та використовується в інформатиці як теоретична модель обчислень, а також як основа для розробки функціональних мов програмування. Вона заснована на комбінаторах, які були введені Шейнфінкелем у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів. Комбінатор — це функція вищого порядку, яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах.
У математиці Комбінаторна логіка спочатку створювалася як «пре-логіка», яка б пояснювала роль кількісних змінних в логіці шляхом їх усунення. Іншим способом усунення кількісних змінних є логіка предикативного функтора Квайна. Хоча виразність комбінаторної логіки зазвичай перевищує за цим параметром логіку першого порядку, виразність логіки предикативного функтора ідентична логіці першого порядку (Квайн 1960, 1966, 1976).
Оригінальний винахідник комбінаторної логіки, Мойсеєм Шенфінкелем, не опублікував нічого про комбінаторну логіку після своєї оригінальної статті 1924 року. Гаскелл Каррі знову відкрив комбінатори, працюючи викладачем в Принстонському університеті наприкінці 1927 року. У 1930-х роках Алонзо Черч і його учні в Принстоні винайшли конкурентний формалізм для функціональної абстракції — лямбда-числення, що виявилося більш популярним, ніж комбінаторна логіка. Підсумком цих історичних обставин було те, що до тих пір, поки теоретична інформатика не почала цікавитися комбінаторною логікою в 1960-х і 1970-х роках, майже вся робота з цього питання була зроблена Гаскеллем Каррі та його учнями, i в Бельгії. У статтях написаних Каррі та Фейсом (1958) і Каррі та інші (1972) можна знайти огляд ранньої історії комбінаторної логіки. Для більш сучасного трактування комбінаторної логіки та лямбда-числення див. книгу Барендрегта, яка розглядає моделі Дана Скотта, розроблені для комбінаторної логіки в 1960-х і 1970-х роках.
В обчислювальній техніці У інформатиці комбінаторна логіка використовується як спрощена модель обчислень, що використовується в теорії обчислюваності та теорії доведення. Незважаючи на свою простоту, комбінаторна логіка охоплює багато суттєвих особливостей обчислення.
Комбінаторну логіку можна розглядати як варіант лямбда-числення, в якому лямбда-вирази (що представляють функціональну абстракцію) замінюються обмеженим набором комбінаторів, примітивних функцій, в яких відсутні зв'язані змінні. Лямбда-вирази легко трансформувати в комбінаторні вирази, а редукція комбінатора набагато простіше, ніж редукція лямбди. Тому комбінаторна логіка була використана для моделювання деяких нетривких функціональних мов програмування та . Найчистішою формою цього погляду є мова програмування , єдиним примітивом якого є комбінатори S і K, доповнені символом вводу/виводу. Не будучи практичною мовою програмування, Unlambda представляє певний теоретичний інтерес.
Комбінаторній логіці можна надати різні інтерпретації. Багато ранніх робіт Каррі показали, як перевести набори аксіом для звичайної логіки в комбінаторні логічні рівняння (Хіндлі і Мередіт 1990). Дана Скотт в 1960-х і 1970-х роках показав, як поєднати теорію моделей та комбінаторну логіку.
Огляд лямбда-числення
Лямбда-числення стосується об'єктів, які називаються лямбда-виразами, які можна представити такими трьома формами рядків:
де v — ім'я змінної, що складається з попередньо визначеного нескінченного набору імен змінних, і та є лямбда-термінами.
Вирази типу називаються абстракціями. Змінна v називається формальним параметром абстракції, і є тілом абстракції. Вираз представляє функцію, яка, будучи застосована до аргументу, зв'язує формальний параметр v з цим аргументом, а потім обчислює отримане значення — тобто повертає , у якому кожне входження v замінено на аргумент.
Вирази типу називаються аплікаціями. Аплікації моделюють виклик або виконання: функція, представлена , повинна бути викликана із як аргумент, і результат обчислюється. Якщо (іноді його називають аплікацією) є абстракцією, термін може бути редукований: , що є аргументом, може бути заміщений в тіло замість формального параметра з , і результат — новий лямбда-вираз, еквівалентний попередньому. Якщо лямбда-вираз не містить підвиразів типу , тоді він не може бути редукованим, та вважається, що він перебуває у .
Вираз являє собою результат обрання терміна і заміщення в ньому всіх вільних входжень на . Таким чином, ми записуємо:
За домовленістю, ми вважаємо скороченням (тобто, застосування є асоціативним зліва).
Мотивацією для визначення цього скорочення є те, що воно фіксує істотну поведінку всіх математичних функцій. Наприклад, розглянемо функцію, яка обчислює квадрат числа. Ми можемо написати: Квадратом x є
(Використовується «» для вказівки множення) x тут є формальним параметром функції. Щоб оцінити квадрат для конкретного аргументу, скажімо 3, вставляємо його в визначення замість формального параметра:
Квадратом 3 є
Для оцінки отриманого виразу , нам доведеться вдатися до наших знань про множення і число 3. Оскільки будь-яке обчислення є просто композицією оцінки відповідних функцій на відповідних примітивних аргументах, цього простого принципу заміщення достатньо, щоб захопити істотний механізм обчислення. Більш того, у лямбда-численні такі поняття, як '3' та '' можуть бути представлені без будь-якої потреби у визначених ззовні примітивних операторах або константах. Можливо ідентифікувати терміни в лямбда-численні, які, якщо їх правильно інтерпретувати, ведуть себе як число 3 і подібно оператору множення, як у .
Як відомо, лямбда-числення є обчислювально еквівалентним за потужністю для багатьох інших відомих моделей для обчислення (включаючи машини Тьюринга); тобто будь-який розрахунок, який можна виконати в будь-якій з цих інших моделей, може бути виражений в лямбда-численні і навпаки. Згідно з тезою Черча-Тюрінга, обидві моделі можуть виражати будь-які можливі обчислення.
Можливо, дивно, що лямбда-числення спроможне являти собою будь-яке можливе обчислення, використовуючи лише прості поняття абстракції та аплікації функції, засновані на простому текстовому заміщенні виразів на змінні. Але ще більш примітним є те, що абстракція навіть не потрібна. Комбінаторна логіка є моделлю обчислення, еквівалентною лямбда-численням, але без абстракції. Перевага цього полягає в тому, що оцінювання виразів у лямбда-численні є досить складним, оскільки семантика заміщення повинна бути задана з великою обережністю, щоб уникнути проблем із захопленням змінних. Навпаки, оцінювання виразів у комбінаторній логіці набагато простіше, оскільки не існує поняття заміщення.
Комбінаторне числення Оскільки абстракція є єдиним способом виробництва функцій у лямбда-численні, щось має замінити його в комбінаторному численні. Замість абстракції комбінаторне числення забезпечує обмежений набір примітивних функцій, з яких можуть бути побудовані інші функції.
Комбінаторні вирази Комбінаторний вираз має одну з таких форм:
де — змінна, — одна з примітивних функцій, і є застосування комбінаторних термінів і . Самі примітивні функції є комбінаторами, або функціями, які, якщо розглядати їх як лямбда-вирази, не містять вільних змінних. Щоб скоротити позначення, застосовується загальна домовленість , або навіть , позначає термін . Це та ж сама загальна домовленість (ліва асоціативність) що й для кількох аплікації в лямбда-численні.
Редукція в комбінаторній логіці У комбінаторній логіці кожен примітивний комбінатор має правило редукції форми
де Е — термін, що позначає лише змінні з множини x1 ... xn. Саме таким чином примітивні комбінатори ведуть себе подібно функціям.
Приклади комбінаторів Найпростішим прикладом комбінатора є I , комбінатор ідентичності, який визначається таким чином: (I x) = x для всіх термінів x.
Іншим простим комбінатором є K , який виробляє постійні функції: (K x) — це функція, яка, для будь-якого аргументу, повертає x , так що ми говоримо: ((K x) y) = x для всіх виразів x і y.
Або, відповідно до домовленості щодо кількох аплікацій,
(K x y) = x
Третім комбінатором є S , що є узагальненою версією аплікації:
(S xyz) = (xz (yz))
S застосовує x до y після першої підстановки z в кожен з них. Або по-іншому, x застосовується до y всередині середовища z.
Враховуючи S і K, I не потрібен, оскільки цей комбінатор може бути побудово з двох інших:
((SKK) x) = (SKK x) = (K x (K x)) = x
для будь-якого виразу х. Зауважимо, що хоча ((SKK) x) = (I x) для будь-якого x, (SKK) сама по собі не дорівнює I. Ми говоримо, що терміни . Рівень екстенсивності відображає математичне поняття рівності функцій: дві функції рівні, якщо вони завжди дають однакові результати для тих самих аргументів. Навпаки, самі вирази, разом із редукцією примітивних комбінаторів, фіксують поняття інтенсіональної рівності функцій: дві функції рівні, тільки якщо вони мають ідентичні реалізації до розширення примітивних комбінаторів, коли вони застосовані до достатньої кількості аргументів. Існує багато способів реалізації функції ідентичності; (SKK) і I є серед цих шляхів, а також (SKS). Ми будемо використовувати слово еквівалентність для позначення екстенсійної рівності, залишаючи рівність для ідентичних комбінаторних виразів.
Більш цікавим комбінатором є або комбінатор Y , який можна використовувати для реалізації рекурсії.
Повнота базису S-K S і K можуть бути складені так, щоб виробляти комбінатори, які є екстенсивно рівними будь-якому лямбда-виразу, а отже, за тезою Черча, до будь-якої обчислювальної функції. Доказом є перетворення, T[ ], який перетворює довільний лямбда-член в еквівалентний комбінатор.
T[ ] може бути визначено таким чином:
T[x] => x T[(E₁ E₂)] => (T[E₁] T[E₂]) T[λx.E] => (K T[E]) (якщо x не виявляється вільним в E) T[λx.x] => I T[λx.λy.E] => Tλx.Tλy.E (якщо x виявляється вільним в E) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (якщо x виявляється вільним в E₁ або E₂)
Цей процес також відомий як усунення абстракції. Це визначення є вичерпним: будь-який лямбда-вираз буде підпорядковуватися рівно одному з цих правил (див. Підсумок лямбда-числення вище).
Це пов'язано з процесом абстракції в дужках, який приймає вираз E, побудований зі змінних, і аплікацію, та повертає комбінаторний вираз [x]E, в якому змінна x не є вільною, так що [x]Ex = E виконується. Дуже простий алгоритм абстракції в дужках визначається індукцією за структурою виразів таким чином:
[x]y := K y [x]x := I [x](E₁ E₂) := S([x]E₁)([x]E₂)
Абстракція в дужках індукує переклад з лямбда-термінів на комбінаторні вирази, інтерпретуючи лямбда-абстракції за допомогою алгоритму абстракції в дужках.
Перетворення лямбда-вираза в еквівалентний комбінаторний термін Наприклад, ми перетворимо лямбда-термін λx.λy.(y x) до комбінаторного терміна:
T[λx.λy.(у x)] = Tλx.Tλy.(y x) (за 5-м правилом) = T[λx.(S T[λy.y] T[λy.x])] (за 6-м) = T[λx.(S I T[λy.x])] (за 4-м) = T[λx.(S I (K T[x]))] (за 3-м) = T[λx.(S I (K x))] (за 1-м) = (S T[λx.(S I)] T[λx.(K x)]) (за 6-м) = (S (K (S I)) T[λx.(K x)]) (за 3-м) = (S (K (S I)) (S T[λx.K] T[λx.x])) (за 6-м) = (S (K (S I)) (S (K K) T[λx.x])) (за 3-м) = (S (K (S I)) (S (K K) I)) (за 4-м)
Якщо застосувати цей комбінаторний термін до будь-яких двох термінів x і y, він зменшується таким чином:
(S (K (S I)) (S (K K) I) x y) = (K (S I) x (S (K K) I x) y) = (S I (S (K K) I x) y) = (I y (S (K K) I x y)) = (y (S (K K) I x y)) = (y (K K x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (y x)
Комбінаторний вираз (S (K (SI)) (S (KK) I)) набагато довше за лямбда-вираз, λx.λy.(ух), що є типовим. Загалом, T[ ] конструкція може розширити лямбда-вираз довжини n до комбінаторного виразу довжини Θ(n3).