Комбінаторна логіка — це нотація для усунення необхідності кількісних змінних в математичній логіці. Вона була введена Мойсейем Шейнфінкелем і Гаскеллем Каррі, та використовується в інформатиці як теоретична модель обчислень, а також як основа для розробки функціональних мов програмування. Вона заснована на комбінаторах, які були введені Шейнфінкелем у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів. Комбінатор — це функція вищого порядку, яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах.
У математиці
Комбінаторна логіка спочатку створювалася як «пре-логіка», яка б пояснювала роль кількісних змінних в логіці шляхом їх усунення. Іншим способом усунення кількісних змінних є логіка предикативного функтора Квайна. Хоча виразність комбінаторної логіки зазвичай перевищує за цим параметром логіку першого порядку, виразність логіки предикативного функтора ідентична логіці першого порядку (Квайн 1960, 1966, 1976).
Оригінальний винахідник комбінаторної логіки, Мойсейем Шенфінкелем, не опублікував нічого про комбінаторну логіку після своєї оригінальної статті 1924 року. Гаскелл Каррі знову відкрив комбінатори, працюючи викладачем в Принстонському університеті наприкінці 1927 року. У 1930-х роках Алонзо Черч і його учні в Принстоні винайшли конкурентний формалізм для функціональної абстракції — лямбда-числення, що виявилося більш популярним, ніж комбінаторна логіка. Підсумком цих історичних обставин було те, що до тих пір, поки теоретична інформатика не почала цікавитися комбінаторною логікою в 1960-х і 1970-х роках, майже вся робота з цього питання була зроблена Гаскеллем Каррі та його учнями, i [en] в Бельгії. У статтях написаних Каррі та Фейсом (1958) і Каррі та інші (1972) можна знайти огляд ранньої історії комбінаторної логіки. Для більш сучасного трактування комбінаторної логіки та лямбда-числення див. книгу Барендрегта, яка розглядає моделі Дана Скотта, розроблені для комбінаторної логіки в 1960-х і 1970-х роках.
В обчислювальній техніці
У інформатиці комбінаторна логіка використовується як спрощена модель обчислень, що використовується в теорії обчислюваності та теорії доведення. Незважаючи на свою простоту, комбінаторна логіка охоплює багато суттєвих особливостей обчислення.
Комбінаторну логіку можна розглядати як варіант лямбда-числення, в якому лямбда-вирази (що представляють функціональну абстракцію) замінюються обмеженим набором комбінаторів, примітивних функцій, в яких відсутні зв'язані змінні. Лямбда-вирази легко трансформувати в комбінаторні вирази, а редукція комбінатора набагато простіше, ніж редукція лямбди. Тому комбінаторна логіка була використана для моделювання деяких нетривких функціональних мов програмування та [en]. Найчистішою формою цього погляду є мова програмування [en], єдиним примітивом якого є комбінатори S і K, доповнені символом вводу/виводу. Не будучи практичною мовою програмування, Unlambda представляє певний теоретичний інтерес.
Комбінаторній логіці можна надати різні інтерпретації. Багато ранніх робіт Каррі показали, як перевести набори аксіом для звичайної логіки в комбінаторні логічні рівняння (Хіндлі і Мередіт 1990). Дана Скотт в 1960-х і 1970-х роках показав, як поєднати теорію моделей та комбінаторну логіку.
Огляд лямбда-числення
Лямбда-числення стосується об'єктів, які називаються лямбда-виразами, які можна представити наступними трьома формами рядків:
- v
де v — ім'я змінної, що складається з попередньо визначеного нескінченного набору імен змінних, і та
є лямбда-термінами.
Вирази типу називаються абстракціями. Змінна v називається формальним параметром абстракції, і
є тілом абстракції. Вираз
представляє функцію, яка, будучи застосована до аргументу, зв'язує формальний параметр v з цим аргументом, а потім обчислює отримане значення
— тобто повертає
, у якому кожне входження v замінено на аргумент.
Вирази типу називаються аплікаціями. Аплікації моделюють виклик або виконання: функція, представлена
, повинна бути викликана із
у якості аргументу, і результат обчислюється. Якщо
(іноді його називають аплікацією) є абстракцією, термін може бути редукований:
, що є аргументом, може бути заміщений в тіло
замість формального параметра з
, і результат — новий лямбда-вираз, еквівалентний попередньому. Якщо лямбда-вираз не містить підвиразів типу
, тоді він не може бути редукованим, та вважається, що він перебуває у [en].
Вираз являє собою результат обрання терміна E і заміщення в ньому всіх вільних входжень v на a. Таким чином, ми записуємо:
За домовленістю, ми вважаємо скороченням
(тобто, застосування є асоціативним зліва).
Мотивацією для визначення цього скорочення є те, що воно фіксує істотну поведінку всіх математичних функцій. Наприклад, розглянемо функцію, яка обчислює квадрат числа. Ми можемо написати: Квадратом x є
(Використовується «» для вказівки множення) x тут є формальним параметром функції. Щоб оцінити квадрат для конкретного аргументу, скажімо 3, вставляємо його в визначення замість формального параметра:
- Квадратом 3 є
Для оцінки отриманого виразу , нам доведеться вдатися до наших знань про множення і число 3. Оскільки будь-яке обчислення є просто композицією оцінки відповідних функцій на відповідних примітивних аргументах, цього простого принципу заміщення достатньо, щоб захопити істотний механізм обчислення. Більш того, у лямбда-численні такі поняття, як '3' та '
' можуть бути представлені без будь-якої потреби у визначених ззовні примітивних операторах або константах. Можливо ідентифікувати терміни в лямбда-численні, які, якщо їх правильно інтерпретувати, ведуть себе як число 3 і подібно оператору множення, як у [en].
Як відомо, лямбда-числення є обчислювально еквівалентним за потужністю для багатьох інших відомих моделей для обчислення (включаючи машини Тьюринга); тобто будь-який розрахунок, який можна виконати в будь-якій з цих інших моделей, може бути виражений в лямбда-численні і навпаки. Згідно з тезою Черча-Тюрінга, обидві моделі можуть виражати будь-які можливі обчислення.
Можливо, дивно, що лямбда-числення спроможне являти собою будь-яке можливе обчислення, використовуючи лише прості поняття абстракції та аплікації функції, засновані на простому текстовому заміщенні виразів на змінні. Але ще більш примітним є те, що абстракція навіть не потрібна. Комбінаторна логіка є моделлю обчислення, еквівалентною лямбда-численням, але без абстракції. Перевага цього полягає в тому, що оцінювання виразів у лямбда-численні є досить складним, оскільки семантика заміщення повинна бути задана з великою обережністю, щоб уникнути проблем із захопленням змінних. Навпаки, оцінювання виразів у комбінаторній логіці набагато простіше, оскільки не існує поняття заміщення.
Комбінаторне числення
Оскільки абстракція є єдиним способом виробництва функцій у лямбда-численні, щось має замінити його в комбінаторному численні. Замість абстракції комбінаторне числення забезпечує обмежений набір примітивних функцій, з яких можуть бути побудовані інші функції.
Комбінаторні вирази
Комбінаторний вираз має одну з наступних форм:
- x
- P
де x — змінна, P — одна з примітивних функцій, і є застосування комбінаторних термінів
і
. Самі примітивні функції є комбінаторами, або функціями, які, якщо розглядати їх як лямбда-вирази, не містять вільних змінних. Щоб скоротити позначення, застосовується загальна домовленість
, або навіть
, позначає термін
. Це та ж сама загальна домовленість (ліва асоціативність) що й для кількох аплікації в лямбда-численні.
Редукція в комбінаторній логіці
У комбінаторній логіці кожен примітивний комбінатор має правило редукції форми
- (P x1 ... xn) = E
де Е — термін, що позначає лише змінні з множини 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. Ми говоримо, що терміни [en]. Рівень екстенсивності відображає математичне поняття рівності функцій: дві функції рівні, якщо вони завжди дають однакові результати для тих самих аргументів. Навпаки, самі вирази, разом із редукцією примітивних комбінаторів, фіксують поняття інтенсіональної рівності функцій: дві функції рівні, тільки якщо вони мають ідентичні реалізації до розширення примітивних комбінаторів, коли вони застосовані до достатньої кількості аргументів. Існує багато способів реалізації функції ідентичності; (SKK) і I є серед цих шляхів, а також (SKS). Ми будемо використовувати слово еквівалентність для позначення екстенсійної рівності, залишаючи рівність для ідентичних комбінаторних виразів.
Більш цікавим комбінатором є [en] або комбінатор 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).
Пояснення Т[ ] перетворення
T[ ] перетворення мотивується прагненням усунути абстракцію. Два особливих випадки, правила 3 та 4, тривіальні: λx.х явно еквівалентно I, а λx.Е явно еквівалентно (K T[E]), якщо x не з'являється вільно в E.
Перші два правила також є простими: змінні перетворюються самі на себе, а аплікації, дозволені в комбінаторних термінах, перетворюються на комбінатори просто шляхом перетворення апліканту та аргументу на комбінатори.
Інтерес представляють правила 5 та 6. Правило 5 просто говорить, що для перетворення складної абстракції на комбінатор, ми повинні спочатку перетворити його тіло на комбінатор, а потім видалити абстракцію. Правило 6 фактично видаляє абстракцію.
λx.(Е₁ Е₂) являє собою функцію, яка приймає аргумент, скажімо, a, і замінює його на лямбда-вираз (Е₁ Е₂) замість х, отримуючи (Е₁ Е₂)[х := a]. Але підставляючи a в (E₁ E₂) замість x, це те ж саме, що й підстановка його на обидва E₁ і E₂, таким чином: (E₂ E₂)[x := a] = (E₁[x := a]E₂[x := a]): (λx . (E ₂ E ₂) a) = ((λx . E) a) (λx . E) a))
- = (S λx . E λ λx . E) a)
- = ((S λx . E₁ λx . E a) a)
За екстенсійної рівності,
- λx.(E₁ E₂) = (S λx.E₁ λx.E₂)
Тому для знаходження комбінатору, що еквівалентний λx.(E₁ E₂), достатньо знайти комбінатор, що еквівалентний (S λx.E₁ λx.E₂), та: (S T[λx.E₁] T[λx.E₂])
очевидно відповідає умовам. Кожен з E₁ та E₂ має строго меншу кількість аплікацій, ніж (E₁ E₂), тому рекурсія повинна закінчуватися в лямбда-виразі без жодних аплікацій — або змінні, або вирази виду λx.E.
Спрощення перетворення
η-редукція
Комбінатори, що генеруються T[ ] перетворенням можуть бути зменшені, якщо взяти до уваги правило η-редукції :
- T[λx.(E x)] = T[E] (якщо x не вільна в E)
λx.(E x) — функція, яка приймає аргумент x, і застосовує до нього функцію E; це екстенсійно дорівнює самій функції E. Тому достатньо перетворити E у комбінаторну форму.
Враховуючи це спрощення, виникає цей приклад:
- T[λx.λy.(y x)]
- = …
- = (S (K (S I)) T[λx.(K x)])
- = (S (K (S I)) K) (за η-редукцією)
Цей комбінатор еквівалентний більш ранньому, довшому:
- (S (K (S I)) K x y)
- = (K (S I) x (K x) y)
- = (S I (K x) y)
- = (I y (K x y))
- = (y (K x y))
- = (y x)
Аналогічно, оригінальна версія T[ ] перетворення трансформувала функцію тотожності λf.λx.(f x) до (S (S (K S) (S (K K) I)) (K I)). За правилом η-редукції λf.λx.(f x) перетворюється в I.
Одноточковий базис
Існують одноточкові базиси, з яких кожен комбінатор може бути складений екстенсійно рівним будь-якому лямбда-члену. Найпростішим прикладом такого базису є {X}, де:
- X ≡ λx.((xS)K)
Не важко переконатися, що:
- X (X (X X)) =ηβ K та
- X (X (X (X X))) = ηβ S.
Оскільки {K, S} є базисом, то {X} також є базисом. Мова програмування [en] використовує X в якості свого єдиного комбінатора.
Іншим простим прикладом одноточкового базису є:
- X' ≡ λx.(x K S K) з: (X' X') X' =β K та
- X' (X' X') = β S
X' не потребує η контракції для отримання K і S. Фактично існує безліч таких базисів.
Комбінатори B, C
На додаток до S і K, стаття Шейнфінкеля включала в себе два комбінатори, які зараз називаються B і C, з наступними скороченнями:
- (C f g x) = ((f x) g): (B f g x) = (f (g x))
Він також пояснює, як вони в свою чергу можуть бути виражені, використовуючи тільки S і K:
- B = (S (K S) K)
- C = (S (S (K (S (K S) K)) S) (K K))
Ці комбінатори надзвичайно корисні при перекладі логіки предикатів або лямбда-числення в комбінаторні вирази. Їх також використовували Каррі, і набагато пізніше [en], чиє ім'я було пов'язане з їх обчислювальним використанням. Використовуючи їх, ми можемо розширити правила перетворення таким чином:
- 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₂)
- T[λx.(E₁ E₂)] ⇒ (C T[λx.E₁] T[E₂]) (якщо x вільний в E₁, але не E₂)
- T[λx.(E₁ E₂)] ⇒ (B T[E₁] T[λx.E₂]) (якщо x вільний в E₂, але не E₁)
Використовуючи комбінатори B і C , перетворення λx.λy.(y x) виглядає так:
- T[λx.λy.(y x)]
- = T[λx.T[λy.(y x)]]
- =T[λx.(C T[λy.y] x)] (за правилом 7)
- = T[λx.(C I x)]
- = (C I) (η-редукція)
- =
(традиційне канонічне позначення:
)
- =
(традиційне канонічне позначення:
)
І дійсно, (C I x y) зменшується до (y x):
- (C I x y)
- = (I y x)
- = (y x)
Мотивація тут полягає в тому, що B і C є обмеженими версіями S. У той час як S приймає значення і замінює його на обидва додатки і його аргумент перед виконанням програми, C виконує заміну тільки в застосуванні, а B - тільки в аргументі.
Сучасні назви для комбінаторів випливають з докторської дисертації Хаскелла Каррі 1930 року (див. [en]). У оригінальній роботі Шейнфінкеля те, що ми називаємо S, K, I, B і C, називали S , C , I , Z і T відповідно.
Зменшення розміру комбінатора, що випливає з нових правил перетворення, також може бути досягнуто без введення B і C, як показано в розділі 3.2.
CLK проти CLI числення
Необхідно розрізняти CLK, як описано в цій статті, і обчислення CLI. Відмінність полягає в тому ж, що й між λK і λI численням.
На відміну від обчислення λK, обчислення λI обмежує абстракцію до λx.E де x має принаймні одне вільне входження в E.
Як наслідок, комбінатор K не присутній у λI обчисленнях, а також у численні CLI. Константами CLI є: I, B, C і S, які є основою для складання всіх термінів CLI (рівність по модулю). Кожен термін λI може бути перетворений в рівний комбінатор CLI згідно з правилами, подібними до описаних вище для перетворення термінів λ K в комбінатори CLK. Див. розділ 9 у Барендрегта (1984).
Зворотне перетворення
Перетворення L[ ] від комбінаторних виразів до лямбда-виразів тривіальне:
- L[I] = λx.x
- L[K] = λx.λy.x
- L[C] = λx.λy.λz.(x z y)
- L[B] = λx.λy.λz.(x (y z))
- L [ S ] = λx . λy . λz. (х г (у г))
- L[(E₁ E₂)] = (L[E₁] L[E₂])
Зазначимо, однак, що це перетворення не є зворотним перетворенням будь-якої з версій T[ ] що ми бачили.
Нерозв'язність комбінаторного числення
[en] є будь-який комбінаторний термін, в якому примітивні комбінатори, які виникають, якщо такі є, не застосовуються до достатньої кількості спрощених аргументів. Не можна вирішити, чи має загальний комбінаторний термін нормальну форму; чи еквівалентні два комбінаторні терміни, і т. д. Це еквівалентно нерозв'язності відповідних задач для лямбда-виразів. Однак прямий доказ полягає в наступному: По-перше, зауважте, що цей вираз
- Ω = (S 'I I' (S 'I I))'
не має нормальної форми, оскільки вона зводиться до себе після трьох кроків, а саме:
- (S I I (S I I))
- = (I (S I I) (I (S I I)))
- = (S I I (I (S I I)))
- = (S I I (S I I))
і, очевидно, жоден інший порядок зменшення не може зробити вираз більш коротким.
Тепер припустимо, що N було комбінатором для виявлення нормальних форм, таких що
- (Де T і F представляють звичайні [en] для істинного і помилкового, λx.λy.x та λx.λy.y, перетворені до комбінаторної логіки. Комбінаторні версії: T = K і F = (K I) .)
Тепер нехай
- Z = (C (C (B N (S I I)) Ω) I)
Тепер розглянемо термін (S I I Z). Чи має (S I I Z) нормальну форму? Так, але тоді і тільки тоді, коли:
- (S I I Z)
- = (I Z (I Z))
- = (Z (I Z))
- = (Z Z)
- = (C (C (B N (S I I)) Ω) I Z) (визначення Z)
- = (C (B N (S I I)) Ω Z I)
- = (B N (S I I) Z Ω I)
- = (N (S I I Z) Ω I)
Тепер нам потрібно застосувати N до (S I I Z). Або (S I I Z) має нормальну форму, або ні. Якщо він має нормальну форму, то вищенаведене зменшується наступним чином :
- (N (S I I Z) Ω I)
- = (K Ω I) (визначення N)
- = Ω
але Ω не має нормальної форми, тому ми маємо протиріччя. Але якщо (S I I Z) не має нормальної форми, вищезгадане зменшується наступним чином:
- (N (S 'I I' Z) Ω I)
- = (K I Ω I) (визначення N)
- = (I I)
- = I
це означає, що нормальна форма (S I I Z) просто I, інше протиріччя. Тому гіпотетичний комбінатор N нормальної форми не може існувати.
Аналог теореми Райса для комбінаторної логіки говорить, що немає повного нетривіального предиката. Предикат є комбінатором, який, коли застосовується, повертає або T, або F. Предикат N нетривіальний, якщо існують два аргументи A і B такі, що N A = T і N B = F. Комбінатор N повний тоді і тільки тоді, коли N M має нормальну форму для кожного аргументу M. Тоді аналог теореми Райса говорить, що кожен повний предикат тривіальний. Доведення цієї теореми досить просте.
Доказ: За допомогою reductio ad absurdum. Припустимо, що є повний нетривіальний предикат, скажімо N. Оскільки N вважається нетривіальним, існують комбінатори A і B такі, що
- (N A) = T а: (N B) = F.
- Визначимо NEGATION λx . (Якщо (N x), то B, A)) λx . ((N x) B A): Визначити ABSURDUM ≡ (Y NEGATION)
Теорема з фіксованою точкою дає: ABSURDUM = (NEGATION ABSURDUM), для
- АБСУРДУМ ATION (Y НЕГАЦІЯ) = (НЕГАЦІЯ (Y НЕГАЦІЯ)) ≡ (НЕГАЦІЯ ABSURDUM).
Оскільки N має бути повним:
- (N ABSURDUM) = F або
- (N ABSURDUM) = T
- Випадок 1: F = (N ABSURDUM) = N (НЕГАЦІЯ АБСУРДУМ) = (N A) = T , протиріччя.
- Випадок 2: T = (N ABSURDUM) = N (НЕГАЦІЯ АБСУРДУМА) = (N B) = F , знову протиріччя.
Отже ( N ABSURDUM) не є ні T, ні F , що суперечить припущенню, що N буде повним нетривіальним предикатом. QED
З цієї теореми нерозв'язності відразу випливає, що немає повного предиката, який може розрізняти терміни, які мають нормальну форму, і терміни, які не мають нормальної форми. Також випливає, що немає повного предиката, наприклад EQUAL, так що:
- (EQUAL A B) = T, якщо A = B і: (EQUAL A B) = F, якщо A ≠ B.
Використання
Компіляція функціональних мов
Девід Тернер використовував свої комбінатори для реалізації [en].
Кеннет Е. Іверсон використовував примітиви на основі комбінаторів Каррі в його мові програмування J, наступнику APL . Це дозволило Іверсону застосувати так зване [en], тобто програмування у функціональних виразах, що не містять змінних, а також потужні інструменти для роботи з такими програмами. Виявляється, мовчазне програмування можливе в будь-якій APL-подібній мові з визначеними користувачем операторами.
Логіка
Ізоморфізм Каррі-Говарда передбачає зв'язок між логікою і програмуванням: кожне доведення теореми інтуїціоністської логіки відповідає скороченню типового лямбда-терміна і навпаки. Крім того, теореми можна ідентифікувати за допомогою сигнатур типу функцій. Зокрема, типізована комбінаторна логіка відповідає системі Гільберта в теорії доказів.
Комбінатори K і S відповідають аксіомам
- AK : A → (B → A),
- AS : (A → (B → C)) → ((A → B) → (A → C)), і застосування функції відповідає правилу відшарування (modus ponens)
- MP : від A і A → B вивести B.
Обчислення, що складається з AK, AS і MP, є повним для імплікаційного фрагмента інтуїціоністської логіки, що можна побачити наступним чином. Розглянемо множину W всіх дедуктивно замкнутих множин формул, упорядкованих за включенням. Тоді є інтуїціоністичним кадром Крипке, і ми визначаємо модель
в цьому кадрі таким чином:
.
Це визначення підпорядковується умовам задоволення →: з одного боку, якщо , і
таке, що
і
, то
за modus ponens. З іншого боку, якщо
, то
за теоремою про дедукцію, таким чином, дедуктивне змикання
є елементом
таким, що
,
, і
. Нехай A будь-яка формула, яка не є доказовою в численні. Тоді A не належить до дедуктивного замикання X порожньої множини, таким чином
і А не є інтуїтивно дійсним.
Див. також
Примітки
- Schönfinkel, Moses (1924). (PDF). Mathematische Annalen. 92: 305—316. doi:10.1007/bf01448013. Архів оригіналу (PDF) за 8 Квітня 2018. Процитовано 5 Березня 2019. 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.
- Curry, Haskell Brooks (1930). Grundlagen der Kombinatorischen Logik [Foundations of combinatorial logic]. American Journal of Mathematics (German) . The Johns Hopkins University Press. 52 (3): 509—536. doi:10.2307/2370619. JSTOR 2370619.
- Wolfram, Stephen (2002). A New Kind of Science. Wolfram Media, Inc. с. 1121. ISBN .
- Seldin, Jonathan (2008). (PDF). Архів оригіналу (PDF) за 16 Травня 2017. Процитовано 23 Квітня 2019.
- Barendregt, 1984.
- (1979). Another Algorithm for Bracket Abstraction. The Journal of Symbolic Logic. 44: 267—270. doi:10.2307/2273733. JSTOR 2273733.
- Lachowski, Łukasz (2018). . Reports on Mathematical Logic (53): 19—42. doi:10.4467/20842589RM.18.002.8835. Архів оригіналу за 23 Квітня 2019. Процитовано 9 вересня 2018.
- Goldberg, Mayer (2004). . Information Processing Letters. 89: 281—286. doi:10.1016/j.ipl.2003.12.005. Архів оригіналу за 23 Квітня 2019. Процитовано 23 Квітня 2019.
- Tromp, John (2008). Binary Lambda Calculus and Combinatory Logic. У Calude, Cristian S. (ред.). Randomness And Complexity, from Leibniz To Chaitin. World Scientific Publishing Company.
- Cherlin, Edward (1991). Pure Functions in APL and J. Proceedings of the international conference on APL '91: 88—93. doi:10.1145/114054.114065.
Подальше читання
- Barendregt, Hendrik Pieter (1984). The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Т. Volume 103. North Holland. ISBN .
- Curry, Haskell B.; (1958). Combinatory Logic. Т. Vol. I. Amsterdam: North Holland. ISBN .
- Curry, Haskell B.; ; Seldin, Jonathan P. (1972). Combinatory Logic. Т. Vol. II. Amsterdam: North Holland. ISBN .
- Field, Anthony J.; (1998). Functional Programming. Addison-Wesley. ISBN .
- ; Meredith, David (1990), , , 55 (1), doi:10.2307/2274956, JSTOR 2274956, MR 1043546, архів оригіналу за 6 Січня 2017, процитовано 5 Березня 2019
- ; Seldin, J. P. (2008). . Cambridge University Press. Архів оригіналу за 10 Лютого 2017. Процитовано 5 Березня 2019.
- (1995). . University of Cambridge. Архів оригіналу за 5 Липня 2017. Процитовано 5 Березня 2019.
- Quine, W. V. (1960). Variables explained away. Proceedings of the American Philosophical Society. 104 (3): 343—347. JSTOR 985250. Reprinted as Chapter 23 of Quine's Selected Logic Papers (1966), pp. 227–235
- Schönfinkel, Moses, 1924, «Über die Bausteine der mathematischen Logik [ 8 Квітня 2018 у Wayback Machine.]», перекладена як «On the Building Blocks of Mathematical Logic» in From Frege to Gödel: a source book in mathematical logic, 1879—1931, Jean van Heijenoort, ed. Harvard University Press, 1967. . Стаття, яка започаткувала комбінаторну логіку.
- Smullyan, Raymond, 1985. . Knopf. . М'який вступ до комбінаторної логіки, представлений у вигляді ряду рекреаційних головоломок з використанням метафори «спостереження за птахами».
- --------, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. Глави 17–20 є більш формальним вступом до комбінаторної логіки, з особливим наголосом на фіксованих точках.
- Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. University of Copenhagen and University of Warsaw, 1999.
- Wolfengagen, V. E. (2003). Combinatory logic in programming: Computations with objects through examples and exercises (вид. 2nd). Moscow: "Center JurInfoR" Ltd. ISBN ..
Посилання
- Стенфордська філософська енциклопедія: «Комбінаторна логіка [ 11 Березня 2019 у Wayback Machine.]» від Katalin Bimbó.
- Keenan, David C. (2001) «Розкрити пересмішника: графічне позначення для лямбда-числення з анімованим зведенням [ 19 Лютого 2019 у Wayback Machine.]»
- Ратман, Кріс, «Комбінаторні птахи [ 17 Вересня 2008 у Wayback Machine.]» Таблиця, що виокремлює основну частину сутності книги Смалліана (1985).
- (Java-аплет)
- Комбінаторна логіка редукції вебсервера [ 15 Листопада 2011 у Wayback Machine.]
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Kombinatorna logika ce notaciya dlya usunennya neobhidnosti kilkisnih zminnih v matematichnij logici Vona bula vvedena Mojsejem Shejnfinkelem i Gaskellem Karri ta vikoristovuyetsya v informatici yak teoretichna model obchislen a takozh yak osnova dlya rozrobki funkcionalnih mov programuvannya Vona zasnovana na kombinatorah yaki buli vvedeni Shejnfinkelem u 1920 roci razom z ideyeyu stvorennya analogichnogo sposobu dlya pobudovi funkcij ta vidalennya bud yakih zgadok pro zminni osoblivo v logici predikativ Kombinator ce funkciya vishogo poryadku yaka vikoristovuye tilki zastosuvannya funkciyi ta ranishe viznacheni kombinatori shob viznachiti rezultat na svoyih argumentah U matematiciKombinatorna logika spochatku stvoryuvalasya yak pre logika yaka b poyasnyuvala rol kilkisnih zminnih v logici shlyahom yih usunennya Inshim sposobom usunennya kilkisnih zminnih ye logika predikativnogo funktora Kvajna Hocha viraznist kombinatornoyi logiki zazvichaj perevishuye za cim parametrom logiku pershogo poryadku viraznist logiki predikativnogo funktora identichna logici pershogo poryadku Kvajn 1960 1966 1976 Originalnij vinahidnik kombinatornoyi logiki Mojsejem Shenfinkelem ne opublikuvav nichogo pro kombinatornu logiku pislya svoyeyi originalnoyi statti 1924 roku Gaskell Karri znovu vidkriv kombinatori pracyuyuchi vikladachem v Prinstonskomu universiteti naprikinci 1927 roku U 1930 h rokah Alonzo Cherch i jogo uchni v Prinstoni vinajshli konkurentnij formalizm dlya funkcionalnoyi abstrakciyi lyambda chislennya sho viyavilosya bilsh populyarnim nizh kombinatorna logika Pidsumkom cih istorichnih obstavin bulo te sho do tih pir poki teoretichna informatika ne pochala cikavitisya kombinatornoyu logikoyu v 1960 h i 1970 h rokah majzhe vsya robota z cogo pitannya bula zroblena Gaskellem Karri ta jogo uchnyami i en v Belgiyi U stattyah napisanih Karri ta Fejsom 1958 i Karri ta inshi 1972 mozhna znajti oglyad rannoyi istoriyi kombinatornoyi logiki Dlya bilsh suchasnogo traktuvannya kombinatornoyi logiki ta lyambda chislennya div knigu Barendregta yaka rozglyadaye modeli Dana Skotta rozrobleni dlya kombinatornoyi logiki v 1960 h i 1970 h rokah V obchislyuvalnij tehniciU informatici kombinatorna logika vikoristovuyetsya yak sproshena model obchislen sho vikoristovuyetsya v teoriyi obchislyuvanosti ta teoriyi dovedennya Nezvazhayuchi na svoyu prostotu kombinatorna logika ohoplyuye bagato suttyevih osoblivostej obchislennya Kombinatornu logiku mozhna rozglyadati yak variant lyambda chislennya v yakomu lyambda virazi sho predstavlyayut funkcionalnu abstrakciyu zaminyuyutsya obmezhenim naborom kombinatoriv primitivnih funkcij v yakih vidsutni zv yazani zminni Lyambda virazi legko transformuvati v kombinatorni virazi a redukciya kombinatora nabagato prostishe nizh redukciya lyambdi Tomu kombinatorna logika bula vikoristana dlya modelyuvannya deyakih netrivkih funkcionalnih mov programuvannya ta en Najchistishoyu formoyu cogo poglyadu ye mova programuvannya en yedinim primitivom yakogo ye kombinatori S i K dopovneni simvolom vvodu vivodu Ne buduchi praktichnoyu movoyu programuvannya Unlambda predstavlyaye pevnij teoretichnij interes Kombinatornij logici mozhna nadati rizni interpretaciyi Bagato rannih robit Karri pokazali yak perevesti nabori aksiom dlya zvichajnoyi logiki v kombinatorni logichni rivnyannya Hindli i Meredit 1990 Dana Skott v 1960 h i 1970 h rokah pokazav yak poyednati teoriyu modelej ta kombinatornu logiku Oglyad lyambda chislennyaDokladnishe Lyambda chislennya Lyambda chislennya stosuyetsya ob yektiv yaki nazivayutsya lyambda virazami yaki mozhna predstaviti nastupnimi troma formami ryadkiv v l v E 1 displaystyle lambda v E 1 E 1 E 2 displaystyle E 1 E 2 de v im ya zminnoyi sho skladayetsya z poperedno viznachenogo neskinchennogo naboru imen zminnih i E 1 displaystyle E 1 ta E 2 displaystyle E 2 ye lyambda terminami Virazi tipu l v E 1 displaystyle lambda v E 1 nazivayutsya abstrakciyami Zminna v nazivayetsya formalnim parametrom abstrakciyi i E 1 displaystyle E 1 ye tilom abstrakciyi Viraz l v E 1 displaystyle lambda v E 1 predstavlyaye funkciyu yaka buduchi zastosovana do argumentu zv yazuye formalnij parametr v z cim argumentom a potim obchislyuye otrimane znachennya E 1 displaystyle E 1 tobto povertaye E 1 displaystyle E 1 u yakomu kozhne vhodzhennya v zamineno na argument Virazi tipu E 1 E 2 displaystyle E 1 E 2 nazivayutsya aplikaciyami Aplikaciyi modelyuyut viklik abo vikonannya funkciya predstavlena E 1 displaystyle E 1 povinna buti viklikana iz E 2 displaystyle E 2 u yakosti argumentu i rezultat obchislyuyetsya Yaksho E 1 displaystyle E 1 inodi jogo nazivayut aplikaciyeyu ye abstrakciyeyu termin mozhe buti redukovanij E 2 displaystyle E 2 sho ye argumentom mozhe buti zamishenij v tilo E 1 displaystyle E 1 zamist formalnogo parametra z E 1 displaystyle E 1 i rezultat novij lyambda viraz ekvivalentnij poperednomu Yaksho lyambda viraz ne mistit pidviraziv tipu l v E 1 E 2 displaystyle lambda v E 1 E 2 todi vin ne mozhe buti redukovanim ta vvazhayetsya sho vin perebuvaye u en Viraz E v a displaystyle E v a yavlyaye soboyu rezultat obrannya termina E i zamishennya v nomu vsih vilnih vhodzhen v na a Takim chinom mi zapisuyemo l v E a E v a displaystyle lambda v E a Rightarrow E v a Za domovlenistyu mi vvazhayemo a b c displaystyle abc skorochennyam a b c displaystyle ab c tobto zastosuvannya ye asociativnim zliva Motivaciyeyu dlya viznachennya cogo skorochennya ye te sho vono fiksuye istotnu povedinku vsih matematichnih funkcij Napriklad rozglyanemo funkciyu yaka obchislyuye kvadrat chisla Mi mozhemo napisati Kvadratom x ye x x displaystyle x x Vikoristovuyetsya displaystyle dlya vkazivki mnozhennya x tut ye formalnim parametrom funkciyi Shob ociniti kvadrat dlya konkretnogo argumentu skazhimo 3 vstavlyayemo jogo v viznachennya zamist formalnogo parametra Kvadratom 3 ye 3 3 displaystyle 3 3 Dlya ocinki otrimanogo virazu 3 3 displaystyle 3 3 nam dovedetsya vdatisya do nashih znan pro mnozhennya i chislo 3 Oskilki bud yake obchislennya ye prosto kompoziciyeyu ocinki vidpovidnih funkcij na vidpovidnih primitivnih argumentah cogo prostogo principu zamishennya dostatno shob zahopiti istotnij mehanizm obchislennya Bilsh togo u lyambda chislenni taki ponyattya yak 3 ta displaystyle mozhut buti predstavleni bez bud yakoyi potrebi u viznachenih zzovni primitivnih operatorah abo konstantah Mozhlivo identifikuvati termini v lyambda chislenni yaki yaksho yih pravilno interpretuvati vedut sebe yak chislo 3 i podibno operatoru mnozhennya yak u en Yak vidomo lyambda chislennya ye obchislyuvalno ekvivalentnim za potuzhnistyu dlya bagatoh inshih vidomih modelej dlya obchislennya vklyuchayuchi mashini Tyuringa tobto bud yakij rozrahunok yakij mozhna vikonati v bud yakij z cih inshih modelej mozhe buti virazhenij v lyambda chislenni i navpaki Zgidno z tezoyu Chercha Tyuringa obidvi modeli mozhut virazhati bud yaki mozhlivi obchislennya Mozhlivo divno sho lyambda chislennya spromozhne yavlyati soboyu bud yake mozhlive obchislennya vikoristovuyuchi lishe prosti ponyattya abstrakciyi ta aplikaciyi funkciyi zasnovani na prostomu tekstovomu zamishenni viraziv na zminni Ale she bilsh primitnim ye te sho abstrakciya navit ne potribna Kombinatorna logika ye modellyu obchislennya ekvivalentnoyu lyambda chislennyam ale bez abstrakciyi Perevaga cogo polyagaye v tomu sho ocinyuvannya viraziv u lyambda chislenni ye dosit skladnim oskilki semantika zamishennya povinna buti zadana z velikoyu oberezhnistyu shob uniknuti problem iz zahoplennyam zminnih Navpaki ocinyuvannya viraziv u kombinatornij logici nabagato prostishe oskilki ne isnuye ponyattya zamishennya Kombinatorne chislennyaOskilki abstrakciya ye yedinim sposobom virobnictva funkcij u lyambda chislenni shos maye zaminiti jogo v kombinatornomu chislenni Zamist abstrakciyi kombinatorne chislennya zabezpechuye obmezhenij nabir primitivnih funkcij z yakih mozhut buti pobudovani inshi funkciyi Kombinatorni virazi Kombinatornij viraz maye odnu z nastupnih form x P E 1 E 2 displaystyle E 1 E 2 de x zminna P odna z primitivnih funkcij i E 1 E 2 displaystyle E 1 E 2 ye zastosuvannya kombinatornih terminiv E 1 displaystyle E 1 i E 2 displaystyle E 2 Sami primitivni funkciyi ye kombinatorami abo funkciyami yaki yaksho rozglyadati yih yak lyambda virazi ne mistyat vilnih zminnih Shob skorotiti poznachennya zastosovuyetsya zagalna domovlenist E 1 E 2 E 3 E n displaystyle E 1 E 2 E 3 E n abo navit E 1 E 2 E 3 E n displaystyle E 1 E 2 E 3 E n poznachaye termin E 1 E 2 E 3 E n displaystyle E 1 E 2 E 3 E n Ce ta zh sama zagalna domovlenist liva asociativnist sho j dlya kilkoh aplikaciyi v lyambda chislenni Redukciya v kombinatornij logici U kombinatornij logici kozhen primitivnij kombinator maye pravilo redukciyi formi P x1 xn E de E termin sho poznachaye lishe zminni z mnozhini x1 xn Same takim chinom primitivni kombinatori vedut sebe podibno funkciyam Prikladi kombinatoriv Najprostishim prikladom kombinatora ye I kombinator identichnosti yakij viznachayetsya takim chinom I x x dlya vsih terminiv x Inshim prostim kombinatorom ye K yakij viroblyaye postijni funkciyi K x ce funkciya yaka dlya bud yakogo argumentu povertaye x tak sho mi govorimo K x y x dlya vsih viraziv x i y Abo vidpovidno do domovlenosti shodo kilkoh aplikacij K x y x Tretim kombinatorom ye S sho ye uzagalnenoyu versiyeyu aplikaciyi S xyz xz yz S zastosovuye x do y pislya pershoyi pidstanovki z v kozhen z nih Abo po inshomu x zastosovuyetsya do y vseredini seredovisha z Vrahovuyuchi S i K I ne potriben oskilki cej kombinator mozhe buti pobudovo z dvoh inshih SKK x SKK x K x K x x dd dlya bud yakogo virazu h Zauvazhimo sho hocha SKK x I x dlya bud yakogo x SKK sama po sobi ne dorivnyuye I Mi govorimo sho termini en Riven ekstensivnosti vidobrazhaye matematichne ponyattya rivnosti funkcij dvi funkciyi rivni yaksho voni zavzhdi dayut odnakovi rezultati dlya tih samih argumentiv Navpaki sami virazi razom iz redukciyeyu primitivnih kombinatoriv fiksuyut ponyattya intensionalnoyi rivnosti funkcij dvi funkciyi rivni tilki yaksho voni mayut identichni realizaciyi do rozshirennya primitivnih kombinatoriv koli voni zastosovani do dostatnoyi kilkosti argumentiv Isnuye bagato sposobiv realizaciyi funkciyi identichnosti SKK i I ye sered cih shlyahiv a takozh SKS Mi budemo vikoristovuvati slovo ekvivalentnist dlya poznachennya ekstensijnoyi rivnosti zalishayuchi rivnist dlya identichnih kombinatornih viraziv Bilsh cikavim kombinatorom ye en abo kombinator Y yakij mozhna vikoristovuvati dlya realizaciyi rekursiyi Povnota bazisu S K S i K mozhut buti skladeni tak shob viroblyati kombinatori yaki ye ekstensivno rivnimi bud yakomu lyambda virazu a otzhe za tezoyu Chercha do bud yakoyi obchislyuvalnoyi funkciyi Dokazom ye peretvorennya T yakij peretvoryuye dovilnij lyambda chlen v ekvivalentnij kombinator T mozhe buti viznacheno nastupnim chinom T x gt x T E E gt T E T E T lx E gt K T E yaksho x ne viyavlyayetsya vilnim v E T lx x gt I T lx ly E gt T lx T ly E yaksho x viyavlyayetsya vilnim v E T lx E E gt S T lx E T lx E yaksho x viyavlyayetsya vilnim v E abo E Cej proces takozh vidomij yak usunennya abstrakciyi Ce viznachennya ye vicherpnim bud yakij lyambda viraz bude pidporyadkovuvatisya rivno odnomu z cih pravil div Pidsumok lyambda chislennya vishe Ce pov yazano z procesom abstrakciyi v duzhkah yakij prijmaye viraz E pobudovanij zi zminnih i aplikaciyu ta povertaye kombinatornij viraz x E v yakomu zminna x ne ye vilnoyu tak sho x Ex E vikonuyetsya Duzhe prostij algoritm abstrakciyi v duzhkah viznachayetsya indukciyeyu za strukturoyu viraziv nastupnim chinom x y K y x x I x E E S x E x E Abstrakciya v duzhkah indukuye pereklad z lyambda terminiv na kombinatorni virazi interpretuyuchi lyambda abstrakciyi za dopomogoyu algoritmu abstrakciyi v duzhkah Peretvorennya lyambda viraza v ekvivalentnij kombinatornij termin Napriklad mi peretvorimo lyambda termin lx ly y x do kombinatornogo termina T lx ly u x T lx T ly y x za 5 m pravilom T lx S T ly y T ly x za 6 m T lx S I T ly x za 4 m T lx S I K T x za 3 m T lx S I K x za 1 m S T lx S I T lx K x za 6 m S K S I T lx K x za 3 m S K S I S T lx K T lx x za 6 m S K S I S K K T lx x za 3 m S K S I S K K I za 4 m dd Yaksho zastosuvati cej kombinatornij termin do bud yakih dvoh terminiv x i y vin zmenshuyetsya nastupnim chinom 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 dd Kombinatornij viraz S K SI S KK I nabagato dovshe za lyambda viraz lx ly uh sho ye tipovim Zagalom T konstrukciya mozhe rozshiriti lyambda viraz dovzhini n do kombinatornogo virazu dovzhini 8 n3 Poyasnennya T peretvorennya T peretvorennya motivuyetsya pragnennyam usunuti abstrakciyu Dva osoblivih vipadki pravila 3 ta 4 trivialni lx h yavno ekvivalentno I a lx E yavno ekvivalentno K T E yaksho x ne z yavlyayetsya vilno v E Pershi dva pravila takozh ye prostimi zminni peretvoryuyutsya sami na sebe a aplikaciyi dozvoleni v kombinatornih terminah peretvoryuyutsya na kombinatori prosto shlyahom peretvorennya aplikantu ta argumentu na kombinatori Interes predstavlyayut pravila 5 ta 6 Pravilo 5 prosto govorit sho dlya peretvorennya skladnoyi abstrakciyi na kombinator mi povinni spochatku peretvoriti jogo tilo na kombinator a potim vidaliti abstrakciyu Pravilo 6 faktichno vidalyaye abstrakciyu lx E E yavlyaye soboyu funkciyu yaka prijmaye argument skazhimo a i zaminyuye jogo na lyambda viraz E E zamist h otrimuyuchi E E h a Ale pidstavlyayuchi a v E E zamist x ce te zh same sho j pidstanovka jogo na obidva E i E takim chinom E E x a E x a E x a lx E E a lx E a lx E a S lx E l lx E a S lx E lx E a a dd dd dd dd Za ekstensijnoyi rivnosti lx E E S lx E lx E Tomu dlya znahodzhennya kombinatoru sho ekvivalentnij lx E E dostatno znajti kombinator sho ekvivalentnij S lx E lx E ta S T lx E T lx E ochevidno vidpovidaye umovam Kozhen z E ta E maye strogo menshu kilkist aplikacij nizh E E tomu rekursiya povinna zakinchuvatisya v lyambda virazi bez zhodnih aplikacij abo zminni abo virazi vidu lx E Sproshennya peretvorennya h redukciya Kombinatori sho generuyutsya T peretvorennyam mozhut buti zmensheni yaksho vzyati do uvagi pravilo h redukciyi T lx E x T E yaksho x ne vilna v E lx E x funkciya yaka prijmaye argument x i zastosovuye do nogo funkciyu E ce ekstensijno dorivnyuye samij funkciyi E Tomu dostatno peretvoriti E u kombinatornu formu Vrahovuyuchi ce sproshennya vinikaye cej priklad T lx ly y x S K S I T lx K x S K S I K za h redukciyeyu dd Cej kombinator ekvivalentnij bilsh rannomu dovshomu S K S I K x y K S I x K x y S I K x y I y K x y y K x y y x dd Analogichno originalna versiya T peretvorennya transformuvala funkciyu totozhnosti lf lx f x do S S K S S K K I K I Za pravilom h redukciyi lf lx f x peretvoryuyetsya v I Odnotochkovij bazis Isnuyut odnotochkovi bazisi z yakih kozhen kombinator mozhe buti skladenij ekstensijno rivnim bud yakomu lyambda chlenu Najprostishim prikladom takogo bazisu ye X de X lx xS K Ne vazhko perekonatisya sho X X X X hb K ta X X X X X hb S Oskilki K S ye bazisom to X takozh ye bazisom Mova programuvannya en vikoristovuye X v yakosti svogo yedinogo kombinatora Inshim prostim prikladom odnotochkovogo bazisu ye X lx x K S K z X X X b K ta X X X b S X ne potrebuye h kontrakciyi dlya otrimannya K i S Faktichno isnuye bezlich takih bazisiv Kombinatori B C Na dodatok do S i K stattya Shejnfinkelya vklyuchala v sebe dva kombinatori yaki zaraz nazivayutsya B i C z nastupnimi skorochennyami C f g x f x g B f g x f g x Vin takozh poyasnyuye yak voni v svoyu chergu mozhut buti virazheni vikoristovuyuchi tilki S i K B S K S K C S S K S K S K S K K Ci kombinatori nadzvichajno korisni pri perekladi logiki predikativ abo lyambda chislennya v kombinatorni virazi Yih takozh vikoristovuvali Karri i nabagato piznishe en chiye im ya bulo pov yazane z yih obchislyuvalnim vikoristannyam Vikoristovuyuchi yih mi mozhemo rozshiriti pravila peretvorennya takim chinom T x x T E E T E T E T lx E K T E yaksho x ne vilnij v E T lx x I T lx ly E T lx T ly E yaksho x vilnij v E T lx E E S T lx E T lx E yaksho x vilnij v oboh E i E T lx E E C T lx E T E yaksho x vilnij v E ale ne E T lx E E B T E T lx E yaksho x vilnij v E ale ne E Vikoristovuyuchi kombinatori B i C peretvorennya lx ly y x viglyadaye tak T lx ly y x T lx T ly y x T lx C T ly y x za pravilom 7 T lx C I x C I h redukciya C displaystyle mathbf C tradicijne kanonichne poznachennya X X I displaystyle mathbf X mathbf XI I displaystyle mathbf I tradicijne kanonichne poznachennya X C X displaystyle mathbf X mathbf CX I dijsno C I x y zmenshuyetsya do y x C I x y I y x y x Motivaciya tut polyagaye v tomu sho B i C ye obmezhenimi versiyami S U toj chas yak S prijmaye znachennya i zaminyuye jogo na obidva dodatki i jogo argument pered vikonannyam programi C vikonuye zaminu tilki v zastosuvanni a B tilki v argumenti Suchasni nazvi dlya kombinatoriv viplivayut z doktorskoyi disertaciyi Haskella Karri 1930 roku div en U originalnij roboti Shejnfinkelya te sho mi nazivayemo S K I B i C nazivali S C I Z i T vidpovidno Zmenshennya rozmiru kombinatora sho viplivaye z novih pravil peretvorennya takozh mozhe buti dosyagnuto bez vvedennya B i C yak pokazano v rozdili 3 2 CLK proti CLI chislennya Neobhidno rozriznyati CLK yak opisano v cij statti i obchislennya CLI Vidminnist polyagaye v tomu zh sho j mizh lK i lI chislennyam Na vidminu vid obchislennya lK obchislennya lI obmezhuye abstrakciyu do lx E de x maye prinajmni odne vilne vhodzhennya v E Yak naslidok kombinator K ne prisutnij u lI obchislennyah a takozh u chislenni CLI Konstantami CLI ye I B C i S yaki ye osnovoyu dlya skladannya vsih terminiv CLI rivnist po modulyu Kozhen termin lI mozhe buti peretvorenij v rivnij kombinator CLI zgidno z pravilami podibnimi do opisanih vishe dlya peretvorennya terminiv l K v kombinatori CLK Div rozdil 9 u Barendregta 1984 Zvorotne peretvorennya Peretvorennya L vid kombinatornih viraziv do lyambda viraziv trivialne L I lx x L K lx ly x L C lx ly lz x z y L B lx ly lz x y z L S lx ly lz h g u g L E E L E L E Zaznachimo odnak sho ce peretvorennya ne ye zvorotnim peretvorennyam bud yakoyi z versij T sho mi bachili Nerozv yaznist kombinatornogo chislennya en ye bud yakij kombinatornij termin v yakomu primitivni kombinatori yaki vinikayut yaksho taki ye ne zastosovuyutsya do dostatnoyi kilkosti sproshenih argumentiv Ne mozhna virishiti chi maye zagalnij kombinatornij termin normalnu formu chi ekvivalentni dva kombinatorni termini i t d Ce ekvivalentno nerozv yaznosti vidpovidnih zadach dlya lyambda viraziv Odnak pryamij dokaz polyagaye v nastupnomu Po pershe zauvazhte sho cej viraz W S I I S I I ne maye normalnoyi formi oskilki vona zvoditsya do sebe pislya troh krokiv a same S I I S I I I S I I I S I I S I I I S I I S I I S I I i ochevidno zhoden inshij poryadok zmenshennya ne mozhe zrobiti viraz bilsh korotkim Teper pripustimo sho N bulo kombinatorom dlya viyavlennya normalnih form takih sho N x T Yaksho x maye normalnu formu F inakshe displaystyle mathbf N x begin cases mathbf T text Yaksho x text maye normalnu formu mathbf F text inakshe end cases De T i F predstavlyayut zvichajni en dlya istinnogo i pomilkovogo lx ly x ta lx ly y peretvoreni do kombinatornoyi logiki Kombinatorni versiyi T K i F K I Teper nehaj Z C C B N S I I W I Teper rozglyanemo termin S I I Z Chi maye S I I Z normalnu formu Tak ale todi i tilki todi koli S I I Z I Z I Z Z I Z Z Z C C B N S I I W I Z viznachennya Z C B N S I I W Z I B N S I I Z W I N S I I Z W I Teper nam potribno zastosuvati N do S I I Z Abo S I I Z maye normalnu formu abo ni Yaksho vin maye normalnu formu to vishenavedene zmenshuyetsya nastupnim chinom N S I I Z W I K W I viznachennya N W ale W ne maye normalnoyi formi tomu mi mayemo protirichchya Ale yaksho S I I Z ne maye normalnoyi formi vishezgadane zmenshuyetsya nastupnim chinom N S I I Z W I K I W I viznachennya N I I I ce oznachaye sho normalna forma S I I Z prosto I inshe protirichchya Tomu gipotetichnij kombinator N normalnoyi formi ne mozhe isnuvati Analog teoremi Rajsa dlya kombinatornoyi logiki govorit sho nemaye povnogo netrivialnogo predikata Predikat ye kombinatorom yakij koli zastosovuyetsya povertaye abo T abo F Predikat N netrivialnij yaksho isnuyut dva argumenti A i B taki sho N A T i N B F Kombinator N povnij todi i tilki todi koli N M maye normalnu formu dlya kozhnogo argumentu M Todi analog teoremi Rajsa govorit sho kozhen povnij predikat trivialnij Dovedennya ciyeyi teoremi dosit proste Dokaz Za dopomogoyu reductio ad absurdum Pripustimo sho ye povnij netrivialnij predikat skazhimo N Oskilki N vvazhayetsya netrivialnim isnuyut kombinatori A i B taki sho N A T a N B F Viznachimo NEGATION lx Yaksho N x to B A lx N x B A Viznachiti ABSURDUM Y NEGATION Teorema z fiksovanoyu tochkoyu daye ABSURDUM NEGATION ABSURDUM dlya ABSURDUM ATION Y NEGACIYa NEGACIYa Y NEGACIYa NEGACIYa ABSURDUM Oskilki N maye buti povnim N ABSURDUM F abo N ABSURDUM T Vipadok 1 F N ABSURDUM N NEGACIYa ABSURDUM N A T protirichchya Vipadok 2 T N ABSURDUM N NEGACIYa ABSURDUMA N B F znovu protirichchya Otzhe N ABSURDUM ne ye ni T ni F sho superechit pripushennyu sho N bude povnim netrivialnim predikatom QED Z ciyeyi teoremi nerozv yaznosti vidrazu viplivaye sho nemaye povnogo predikata yakij mozhe rozriznyati termini yaki mayut normalnu formu i termini yaki ne mayut normalnoyi formi Takozh viplivaye sho nemaye povnogo predikata napriklad EQUAL tak sho EQUAL A B T yaksho A B i EQUAL A B F yaksho A B VikoristannyaKompilyaciya funkcionalnih mov Devid Terner vikoristovuvav svoyi kombinatori dlya realizaciyi en Kennet E Iverson vikoristovuvav primitivi na osnovi kombinatoriv Karri v jogo movi programuvannya J nastupniku APL Ce dozvolilo Iversonu zastosuvati tak zvane en tobto programuvannya u funkcionalnih virazah sho ne mistyat zminnih a takozh potuzhni instrumenti dlya roboti z takimi programami Viyavlyayetsya movchazne programuvannya mozhlive v bud yakij APL podibnij movi z viznachenimi koristuvachem operatorami Logika Izomorfizm Karri Govarda peredbachaye zv yazok mizh logikoyu i programuvannyam kozhne dovedennya teoremi intuyicionistskoyi logiki vidpovidaye skorochennyu tipovogo lyambda termina i navpaki Krim togo teoremi mozhna identifikuvati za dopomogoyu signatur tipu funkcij Zokrema tipizovana kombinatorna logika vidpovidaye sistemi Gilberta v teoriyi dokaziv Kombinatori K i S vidpovidayut aksiomam AK A B A AS A B C A B A C i zastosuvannya funkciyi vidpovidaye pravilu vidsharuvannya modus ponens MP vid A i A B vivesti B Obchislennya sho skladayetsya z AK AS i MP ye povnim dlya implikacijnogo fragmenta intuyicionistskoyi logiki sho mozhna pobachiti nastupnim chinom Rozglyanemo mnozhinu W vsih deduktivno zamknutih mnozhin formul uporyadkovanih za vklyuchennyam Todi W displaystyle langle W subseteq rangle ye intuyicionistichnim kadrom Kripke i mi viznachayemo model displaystyle Vdash v comu kadri takim chinom X A A X displaystyle X Vdash A iff A in X Ce viznachennya pidporyadkovuyetsya umovam zadovolennya z odnogo boku yaksho X A B displaystyle X Vdash A to B i Y W displaystyle Y in W take sho Y X displaystyle Y supseteq X i Y A displaystyle Y Vdash A to Y B displaystyle Y Vdash B za modus ponens Z inshogo boku yaksho X A B displaystyle X not Vdash A to B to X A B displaystyle X A not vdash B za teoremoyu pro dedukciyu takim chinom deduktivne zmikannya X A displaystyle X cup A ye elementom Y W displaystyle Y in W takim sho Y X displaystyle Y supseteq X Y A displaystyle Y Vdash A i Y B displaystyle Y not Vdash B Nehaj A bud yaka formula yaka ne ye dokazovoyu v chislenni Todi A ne nalezhit do deduktivnogo zamikannya X porozhnoyi mnozhini takim chinom X A displaystyle X not Vdash A i A ne ye intuyitivno dijsnim Div takozhKategorialna abstraktna mashina Lyambda chislennyaPrimitkiSchonfinkel Moses 1924 PDF Mathematische Annalen 92 305 316 doi 10 1007 bf01448013 Arhiv originalu PDF za 8 Kvitnya 2018 Procitovano 5 Bereznya 2019 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 Curry Haskell Brooks 1930 Grundlagen der Kombinatorischen Logik Foundations of combinatorial logic American Journal of Mathematics German The Johns Hopkins University Press 52 3 509 536 doi 10 2307 2370619 JSTOR 2370619 Wolfram Stephen 2002 A New Kind of Science Wolfram Media Inc s 1121 ISBN 1 57955 008 8 Seldin Jonathan 2008 PDF Arhiv originalu PDF za 16 Travnya 2017 Procitovano 23 Kvitnya 2019 Barendregt 1984 1979 Another Algorithm for Bracket Abstraction The Journal of Symbolic Logic 44 267 270 doi 10 2307 2273733 JSTOR 2273733 Lachowski Lukasz 2018 Reports on Mathematical Logic 53 19 42 doi 10 4467 20842589RM 18 002 8835 Arhiv originalu za 23 Kvitnya 2019 Procitovano 9 veresnya 2018 Goldberg Mayer 2004 Information Processing Letters 89 281 286 doi 10 1016 j ipl 2003 12 005 Arhiv originalu za 23 Kvitnya 2019 Procitovano 23 Kvitnya 2019 Tromp John 2008 Binary Lambda Calculus and Combinatory Logic U Calude Cristian S red Randomness And Complexity from Leibniz To Chaitin World Scientific Publishing Company Cherlin Edward 1991 Pure Functions in APL and J Proceedings of the international conference on APL 91 88 93 doi 10 1145 114054 114065 Podalshe chitannyaBarendregt Hendrik Pieter 1984 The Lambda Calculus Its Syntax and Semantics Studies in Logic and the Foundations of Mathematics T Volume 103 North Holland ISBN 0 444 87508 5 Curry Haskell B 1958 Combinatory Logic T Vol I Amsterdam North Holland ISBN 0 7204 2208 6 Curry Haskell B Seldin Jonathan P 1972 Combinatory Logic T Vol II Amsterdam North Holland ISBN 0 7204 2208 6 Field Anthony J 1998 Functional Programming Addison Wesley ISBN 0 201 19249 7 Meredith David 1990 55 1 doi 10 2307 2274956 JSTOR 2274956 MR 1043546 arhiv originalu za 6 Sichnya 2017 procitovano 5 Bereznya 2019 Seldin J P 2008 Cambridge University Press Arhiv originalu za 10 Lyutogo 2017 Procitovano 5 Bereznya 2019 1995 University of Cambridge Arhiv originalu za 5 Lipnya 2017 Procitovano 5 Bereznya 2019 Quine W V 1960 Variables explained away Proceedings of the American Philosophical Society 104 3 343 347 JSTOR 985250 Reprinted as Chapter 23 of Quine s Selected Logic Papers 1966 pp 227 235 Schonfinkel Moses 1924 Uber die Bausteine der mathematischen Logik 8 Kvitnya 2018 u Wayback Machine perekladena yak On the Building Blocks of Mathematical Logic in From Frege to Godel a source book in mathematical logic 1879 1931 Jean van Heijenoort ed Harvard University Press 1967 ISBN 0 674 32449 8 Stattya yaka zapochatkuvala kombinatornu logiku Smullyan Raymond 1985 Knopf ISBN 0 394 53491 3 M yakij vstup do kombinatornoyi logiki predstavlenij u viglyadi ryadu rekreacijnih golovolomok z vikoristannyam metafori sposterezhennya za ptahami 1994 Diagonalization and Self Reference Oxford Univ Press Glavi 17 20 ye bilsh formalnim vstupom do kombinatornoyi logiki z osoblivim nagolosom na fiksovanih tochkah Sorensen Morten Heine B and Pawel Urzyczyn 1999 University of Copenhagen and University of Warsaw 1999 Wolfengagen V E 2003 Combinatory logic in programming Computations with objects through examples and exercises vid 2nd Moscow Center JurInfoR Ltd ISBN 5 89158 101 9 PosilannyaStenfordska filosofska enciklopediya Kombinatorna logika 11 Bereznya 2019 u Wayback Machine vid Katalin Bimbo Keenan David C 2001 Rozkriti peresmishnika grafichne poznachennya dlya lyambda chislennya z animovanim zvedennyam 19 Lyutogo 2019 u Wayback Machine Ratman Kris Kombinatorni ptahi 17 Veresnya 2008 u Wayback Machine Tablicya sho viokremlyuye osnovnu chastinu sutnosti knigi Smalliana 1985 Java aplet Kombinatorna logika redukciyi vebservera 15 Listopada 2011 u Wayback Machine