Комбінаторна логіка

Комбінаторна логіка — це нотація для усунення необхідності кількісних змінних в математичній логіці. Вона була введена Мойсейем Шейнфінкелем і Гаскеллем Каррі, та використовується в інформатиці як теоретична модель обчислень, а також як основа для розробки функціональних мов програмування. Вона заснована на комбінаторах, які були введені Шейнфінкелем у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів. Комбінатор — це функція вищого порядку, яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах.

У математиці

Комбінаторна логіка спочатку створювалася як «пре-логіка», яка б пояснювала роль кількісних змінних в логіці шляхом їх усунення. Іншим способом усунення кількісних змінних є логіка предикативного функтора Квайна. Хоча виразність комбінаторної логіки зазвичай перевищує за цим параметром логіку першого порядку, виразність логіки предикативного функтора ідентична логіці першого порядку (Квайн 1960, 1966, 1976).

Оригінальний винахідник комбінаторної логіки, Мойсейем Шенфінкелем, не опублікував нічого про комбінаторну логіку після своєї оригінальної статті 1924 року. Гаскелл Каррі знову відкрив комбінатори, працюючи викладачем в Принстонському університеті наприкінці 1927 року. У 1930-х роках Алонзо Черч і його учні в Принстоні винайшли конкурентний формалізм для функціональної абстракції — лямбда-числення, що виявилося більш популярним, ніж комбінаторна логіка. Підсумком цих історичних обставин було те, що до тих пір, поки теоретична інформатика не почала цікавитися комбінаторною логікою в 1960-х і 1970-х роках, майже вся робота з цього питання була зроблена Гаскеллем Каррі та його учнями, i Робертом Фейсом в Бельгії. У статтях написаних Каррі та Фейсом (1958) і Каррі та інші (1972) можна знайти огляд ранньої історії комбінаторної логіки. Для більш сучасного трактування комбінаторної логіки та лямбда-числення див. книгу Барендрегта, яка розглядає моделі Дана Скотта, розроблені для комбінаторної логіки в 1960-х і 1970-х роках.

В обчислювальній техніці

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

Комбінаторну логіку можна розглядати як варіант лямбда-числення, в якому лямбда-вирази (що представляють функціональну абстракцію) замінюються обмеженим набором комбінаторів, примітивних функцій, в яких відсутні зв'язані змінні. Лямбда-вирази легко трансформувати в комбінаторні вирази, а редукція комбінатора набагато простіше, ніж редукція лямбди. Тому комбінаторна логіка була використана для моделювання деяких нетривких функціональних мов програмування та апаратного забезпечення. Найчистішою формою цього погляду є мова програмування Unlambda, єдиним примітивом якого є комбінатори S і K, доповнені символом вводу/виводу. Не будучи практичною мовою програмування, Unlambda представляє певний теоретичний інтерес.

Комбінаторній логіці можна надати різні інтерпретації. Багато ранніх робіт Каррі показали, як перевести набори аксіом для звичайної логіки в комбінаторні логічні рівняння (Хіндлі і Мередіт 1990). Дана Скотт в 1960-х і 1970-х роках показав, як поєднати теорію моделей та комбінаторну логіку.

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

Лямбда-числення стосується об'єктів, які називаються лямбда-виразами, які можна представити наступними трьома формами рядків:

• v
• $\lambda v.E_{1}$

• $(E_{1}E_{2})$

де v — ім'я змінної, що складається з попередньо визначеного нескінченного набору імен змінних, і $E_{1}$та $E_{2}$ є лямбда-термінами.

Вирази типу $\lambda v.E_{1}$називаються абстракціями. Змінна v називається формальним параметром абстракції, і $E_{1}$ є тілом абстракції. Вираз $\lambda v.E_{1}$представляє функцію, яка, будучи застосована до аргументу, зв'язує формальний параметр v з цим аргументом, а потім обчислює отримане значення $E_{1}$— тобто повертає $E_{1}$, у якому кожне входження v замінено на аргумент.

Вирази типу $(E_{1}E_{2})$називаються аплікаціями. Аплікації моделюють виклик або виконання: функція, представлена $E_{1}$, повинна бути викликана із $E_{2}$у якості аргументу, і результат обчислюється. Якщо $E_{1}$ (іноді його називають аплікацією) є абстракцією, термін може бути редукований: $E_{2}$, що є аргументом, може бути заміщений в тіло $E_{1}$ замість формального параметра з $E_{1}$, і результат — новий лямбда-вираз, еквівалентний попередньому. Якщо лямбда-вираз не містить підвиразів типу $((\lambda v.E_{1})E_{2})$, тоді він не може бути редукованим, та вважається, що він перебуває у нормальній формі.

Вираз $E[v:=a]$ являє собою результат обрання терміна E і заміщення в ньому всіх вільних входжень v на a. Таким чином, ми записуємо:

$((\lambda v.E)a)\Rightarrow E[v:=a]$

За домовленістю, ми вважаємо $(abc)$ скороченням $((ab)c)$ (тобто, застосування є асоціативним зліва).

Мотивацією для визначення цього скорочення є те, що воно фіксує істотну поведінку всіх математичних функцій. Наприклад, розглянемо функцію, яка обчислює квадрат числа. Ми можемо написати: Квадратом x є $x*x$

(Використовується «$*$» для вказівки множення) x тут є формальним параметром функції. Щоб оцінити квадрат для конкретного аргументу, скажімо 3, вставляємо його в визначення замість формального параметра:

Квадратом 3 є $3*3$

Для оцінки отриманого виразу $3*3$, нам доведеться вдатися до наших знань про множення і число 3. Оскільки будь-яке обчислення є просто композицією оцінки відповідних функцій на відповідних примітивних аргументах, цього простого принципу заміщення достатньо, щоб захопити істотний механізм обчислення. Більш того, у лямбда-численні такі поняття, як '3' та '$*$' можуть бути представлені без будь-якої потреби у визначених ззовні примітивних операторах або константах. Можливо ідентифікувати терміни в лямбда-численні, які, якщо їх правильно інтерпретувати, ведуть себе як число 3 і подібно оператору множення, як у кодуванні Черча.

Як відомо, лямбда-числення є обчислювально еквівалентним за потужністю для багатьох інших відомих моделей для обчислення (включаючи машини Тьюринга); тобто будь-який розрахунок, який можна виконати в будь-якій з цих інших моделей, може бути виражений в лямбда-численні і навпаки. Згідно з тезою Черча-Тюрінга, обидві моделі можуть виражати будь-які можливі обчислення.

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

Комбінаторне числення

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

Комбінаторні вирази

Комбінаторний вираз має одну з наступних форм:

• x
• P
• $(E_{1}E_{2})$

де x — змінна, P — одна з примітивних функцій, і $(E_{1}E_{2})$є застосування комбінаторних термінів $E_{1}$і $E_{2}$. Самі примітивні функції є комбінаторами, або функціями, які, якщо розглядати їх як лямбда-вирази, не містять вільних змінних. Щоб скоротити позначення, застосовується загальна домовленість $(E_{1}E_{2}E_{3}...E_{n})$, або навіть $E_{1}E_{2}E_{3}...E_{n}$, позначає термін $(...((E_{1}E_{2})E_{3})...E_{n})$. Це та ж сама загальна домовленість (ліва асоціативність) що й для кількох аплікації в лямбда-численні.

Редукція в комбінаторній логіці

У комбінаторній логіці кожен примітивний комбінатор має правило редукції форми

(P x₁ ... x_n) = E

де Е — термін, що позначає лише змінні з множини x₁ ... x_n . Саме таким чином примітивні комбінатори ведуть себе подібно функціям.

Приклади комбінаторів

Найпростішим прикладом комбінатора є 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[ ] може бути визначено наступним чином:

1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] => (K T[E]) (якщо x не виявляється вільним в E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (якщо x виявляється вільним в E)
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (якщо x виявляється вільним в E₁ або E₂)

Цей процес також відомий як усунення абстракції. Це визначення є вичерпним: будь-який лямбда-вираз буде підпорядковуватися рівно одному з цих правил (див. Підсумок лямбда-числення вище).

Це пов'язано з процесом абстракції в дужках, який приймає вираз E, побудований зі змінних, і аплікацію, та повертає комбінаторний вираз [x]E, в якому змінна x не є вільною, так що [x]Ex = E виконується. Дуже простий алгоритм абстракції в дужках визначається індукцією за структурою виразів наступним чином:

1. [x]y := K y
2. [x]x := I
3. [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 до комбінаторного виразу довжини Θ(n³).

Пояснення Т[ ] перетворення

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} також є базисом. Мова програмування Iota використовує 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))

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

1. T[x] ⇒ x
2. T[(E₁ E₂)] ⇒ (T[E₁] T[E₂])
3. T[λx.E] ⇒ (K T[E]) (якщо x не вільний в E)
4. T[λx.x] ⇒ I
5. T[λx.λy.E] ⇒ T[λx.T[λy.E]] (якщо x вільний в E)
6. T[λx.(E₁ E₂)] ⇒ (S T[λx.E₁] T[λx.E₂]) (якщо x вільний в обох E₁ і E₂)
7. T[λx.(E₁ E₂)] ⇒ (C T[λx.E₁] T[E₂]) (якщо x вільний в E₁, але не E₂)
8. 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) (η-редукція)

= $\mathbf {C} _{*}$ (традиційне канонічне позначення: $\mathbf {X} _{*}=\mathbf {XI}$)

= $\mathbf {I} '$(традиційне канонічне позначення: $\mathbf {X} '=\mathbf {CX}$)

І дійсно, (C I x y) зменшується до (y x):

(C I x y)

= (I y x)

= (y x)

Мотивація тут полягає в тому, що B і C є обмеженими версіями S. У той час як S приймає значення і замінює його на обидва додатки і його аргумент перед виконанням програми, C виконує заміну тільки в застосуванні, а B - тільки в аргументі.

Сучасні назви для комбінаторів випливають з докторської дисертації Хаскелла Каррі 1930 року (див. B, C, K, W System). У оригінальній роботі Шейнфінкеля те, що ми називаємо S, K, I, B і C, називали S , C , I , Z і T відповідно.

Зменшення розміру комбінатора, що випливає з нових правил перетворення, також може бути досягнуто без введення B і C, як показано в розділі 3.2.

CL_K проти CL_I числення

Необхідно розрізняти CL_K, як описано в цій статті, і обчислення CL_I. Відмінність полягає в тому ж, що й між λ_K і λ_I численням.

На відміну від обчислення λ_K, обчислення λ_I обмежує абстракцію до λx.E де x має принаймні одне вільне входження в E.

Як наслідок, комбінатор K не присутній у λ_I обчисленнях, а також у численні CL_I. Константами CL_I є: I, B, C і S, які є основою для складання всіх термінів CL_I (рівність по модулю). Кожен термін λ_I може бути перетворений в рівний комбінатор CL_I згідно з правилами, подібними до описаних вище для перетворення термінів λ _K в комбінатори CL_K. Див. розділ 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[ ] що ми бачили.

Нерозв'язність комбінаторного числення

Нормальною формою є будь-який комбінаторний термін, в якому примітивні комбінатори, які виникають, якщо такі є, не застосовуються до достатньої кількості спрощених аргументів. Не можна вирішити, чи має загальний комбінаторний термін нормальну форму; чи еквівалентні два комбінаторні терміни, і т. д. Це еквівалентно нерозв'язності відповідних задач для лямбда-виразів. Однак прямий доказ полягає в наступному: По-перше, зауважте, що цей вираз

Ω = (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 було комбінатором для виявлення нормальних форм, таких що

$(\mathbf {N} \ x)={\begin{cases}\mathbf {T} ,{\text{ Якщо }}x{\text{ має нормальну форму}}\\\mathbf {F} ,{\text{ інакше.}}\end{cases}}$

(Де T і F представляють звичайні кодування Черча для істинного і помилкового, λ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 має бути повним:

1. (N ABSURDUM) = F або
2. (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.

Використання

Компіляція функціональних мов

Девід Тернер використовував свої комбінатори для реалізації мови програмування SASL.

Кеннет Е. Іверсон використовував примітиви на основі комбінаторів Каррі в його мові програмування J, наступнику APL . Це дозволило Іверсону застосувати так зване мовчазне програмування, тобто програмування у функціональних виразах, що не містять змінних, а також потужні інструменти для роботи з такими програмами. Виявляється, мовчазне програмування можливе в будь-якій 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 всіх дедуктивно замкнутих множин формул, упорядкованих за включенням. Тоді $\langle W,\subseteq \rangle$ є інтуїціоністичним кадром Крипке, і ми визначаємо модель $\Vdash$ в цьому кадрі таким чином: $X\Vdash A\iff A\in X$.

Це визначення підпорядковується умовам задоволення →: з одного боку, якщо $X\Vdash A\to B$, і $Y\in W$таке, що $Y\supseteq X$ і $Y\Vdash A$, то $Y\Vdash B$ за modus ponens. З іншого боку, якщо $X\not \Vdash A\to B$, то $X,A\not \vdash B$ за теоремою про дедукцію, таким чином, дедуктивне змикання $X\cup \{A\}$ є елементом $Y\in W$ таким, що $Y\supseteq X$, $Y\Vdash A$, і $Y\not \Vdash B$. Нехай A будь-яка формула, яка не є доказовою в численні. Тоді A не належить до дедуктивного замикання X порожньої множини, таким чином $X\not \Vdash A$і А не є інтуїтивно дійсним.

Див. також

• Категоріальна абстрактна машина
• Лямбда-числення

Подальше читання

• Barendregt, Hendrik Pieter (1984). The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Т. Volume 103. North Holland. ISBN 0-444-87508-5.
• Curry, Haskell B.; Feys, Robert (1958). Combinatory Logic. Т. Vol. I. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Т. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Field, Anthony J.; Harrison, Peter G. (1998). Functional Programming. Addison-Wesley. ISBN 0-201-19249-7.
• Hindley, J. Roger; Meredith, David (1990), Principal type-schemes and condensed detachment, Journal of Symbolic Logic, 55 (1), doi:10.2307/2274956, JSTOR 2274956, MR 1043546, архів оригіналу за 6 Січня 2017, процитовано 5 Березня 2019
• Hindley, J. R.; Seldin, J. P. (2008). λ-calculus and Combinators: An Introduction. Cambridge University Press. Архів оригіналу за 10 Лютого 2017. Процитовано 5 Березня 2019.
• Paulson, Lawrence C. (1995). Foundations of Functional Programming. 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. ISBN 0-674-32449-8. Стаття, яка започаткувала комбінаторну логіку.
• Smullyan, Raymond, 1985. To Mock a Mockingbird. Knopf. ISBN 0-394-53491-3. М'який вступ до комбінаторної логіки, представлений у вигляді ряду рекреаційних головоломок з використанням метафори «спостереження за птахами».
• --------, 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 5-89158-101-9..

Посилання

• Стенфордська філософська енциклопедія: «Комбінаторна логіка [Архівовано 11 Березня 2019 у Wayback Machine.]» від Katalin Bimbó.
• 1920–1931 рр. Блок-записки Каррі.
• Keenan, David C. (2001) «Розкрити пересмішника: графічне позначення для лямбда-числення з анімованим зведенням [Архівовано 19 Лютого 2019 у Wayback Machine.]»
• Ратман, Кріс, «Комбінаторні птахи [Архівовано 17 Вересня 2008 у Wayback Machine.]» Таблиця, що виокремлює основну частину сутності книги Смалліана (1985).
• Комбінатори перетягування. (Java-аплет)
• Бінарне лямбда-числення та комбінаторна логіка.
• Комбінаторна логіка редукції вебсервера [Архівовано 15 Листопада 2011 у Wayback Machine.]