Перегляд вихідного коду сторінки Комбінаторна логіка

'''Комбінаторна логіка'''&nbsp;— це нотація для усунення необхідності [[Квантор|кількісних]] змінних в [[Математична логіка|математичній логіці]]. Вона була введена [[Шейнфінкель Мойсей Ейлєвич|Мойсеєм Шейнфінкелем]]<ref>{{cite journal |first=Moses |last=Schönfinkel |authorlink=Шейнфінкель Мойсей Ейлєвич |year=1924 |url=http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf |title=Über die Bausteine der mathematischen Logik |journal=Mathematische Annalen |volume=92 |pages=305–316 |doi=10.1007/bf01448013 |accessdate=5 Березня 2019 |archive-date=8 Квітня 2018 |archive-url=https://web.archive.org/web/20180408210251/http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf }} 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&ndash;1931''. Harvard Univ. Press: 355&ndash;66.</ref> і [[Гаскелл Каррі|Гаскеллем Каррі]],<ref>{{cite journal|last=Curry|first=Haskell Brooks|title=Grundlagen der Kombinatorischen Logik|url=https://archive.org/details/sim_american-journal-of-mathematics_1930-07_52_3/page/509|journal=American Journal of Mathematics|year=1930|volume=52|issue=3|pages=509–536|authorlink=Гаскелл Каррі|trans-title=Foundations of combinatorial logic|publisher=The Johns Hopkins University Press|language=German|doi=10.2307/2370619|jstor=2370619}}</ref> та використовується в [[Інформатика|інформатиці]] як теоретична модель [[Обчислення (інформатика)|обчислень]], а також як основа для розробки [[Функційне програмування|функціональних мов програмування]]. Вона заснована на '''комбінаторах,''' які були введені [[Шейнфінкель Мойсей Ейлєвич|Шейнфінкелем]] у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів.<ref>{{cite book|last=Wolfram|first=Stephen|title=A New Kind of Science|publisher=Wolfram Media, Inc.|year=2002|page=[https://archive.org/details/newkindofscience00wolf/page/1121 1121]|isbn=1-57955-008-8|url=https://archive.org/details/newkindofscience00wolf/page/1121}}</ref> Комбінатор&nbsp;— це [[Функція вищого порядку|функція вищого порядку,]] яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах.

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

Оригінальний винахідник комбінаторної логіки, [[Шейнфінкель Мойсей Ейлєвич|Мойсеєм Шенфінкелем]], не опублікував нічого про комбінаторну логіку після своєї оригінальної статті 1924 року. [[Гаскелл Каррі]] знову відкрив комбінатори, працюючи викладачем в [[Принстонський університет|Принстонському університеті]] наприкінці 1927 року.<ref name="Seldin 2006">{{cite journal|last=Seldin|first=Jonathan|title=The Logic of Curry and Church|year=2008|url=http://people.uleth.ca/%7Ejonathan.seldin/CCL.pdf|journal=|accessdate=23 Квітня 2019|archive-date=16 Травня 2017|archive-url=https://web.archive.org/web/20170516203511/http://people.uleth.ca/~jonathan.seldin/CCL.pdf}}</ref> У 1930-х роках [[Алонзо Черч]] і його учні в Принстоні винайшли конкурентний формалізм для функціональної абстракції&nbsp;— [[лямбда-числення]], що виявилося більш популярним, ніж комбінаторна логіка. Підсумком цих історичних обставин було те, що до тих пір, поки теоретична інформатика не почала цікавитися комбінаторною логікою в 1960-х і 1970-х роках, майже вся робота з цього питання була зроблена Гаскеллем [[Гаскелл Каррі|Каррі]] та його учнями, i {{Нп|Роберт Фейс|Робертом Фейсом||Robert Feys}} в [[Бельгія|Бельгії]]. У статтях написаних Каррі та Фейсом (1958) і Каррі та інші (1972) можна знайти огляд ранньої історії комбінаторної логіки. Для більш сучасного трактування комбінаторної логіки та лямбда-числення див. книгу Барендрегта{{sfn|Barendregt|1984}}, яка розглядає [[Теорія моделей|моделі]] [[Дана Скотт]]а, розроблені для комбінаторної логіки в 1960-х і 1970-х роках.

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

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

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

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

* {{Mvar|v}}
* {{tmath|\lambda v.E_1}}

* {{tmath|(E_1 E_2)}}

де ''v''&nbsp;— ім'я змінної, що складається з попередньо визначеного нескінченного набору імен змінних, і {{tmath|E_1}}та {{tmath|E_2}} є лямбда-термінами.

Вирази типу {{tmath|\lambda v.E_1}}називаються ''абстракціями''. Змінна ''v'' називається [[Параметр (програмування)|формальним параметром]] абстракції, і {{tmath|E_1}} є ''тілом'' абстракції. Вираз {{tmath|\lambda v.E_1}}представляє функцію, яка, будучи застосована до аргументу, зв'язує формальний параметр ''v'' з цим аргументом, а потім обчислює отримане значення {{tmath|E_1}}— тобто повертає {{tmath|E_1}}, у якому кожне входження ''v'' замінено на аргумент.

Вирази типу {{tmath|(E_1 E_2)}}називаються ''аплікаціями''. Аплікації моделюють виклик або виконання: функція, представлена {{tmath|E_1}}, повинна бути викликана із {{tmath|E_2}}у якості аргументу, і результат обчислюється. Якщо {{tmath|E_1}} (іноді його називають ''аплікацією'') є абстракцією, термін може бути ''редукований'': {{tmath|E_2}}, що є аргументом, може бути заміщений в тіло {{tmath|E_1}} замість формального параметра з {{tmath|E_1}}, і результат&nbsp;— новий лямбда-вираз, ''еквівалентний'' попередньому. Якщо лямбда-вираз не містить підвиразів типу {{tmath|((\lambda v.E_1) E_2)}}, тоді він не може бути редукованим, та вважається, що він перебуває у {{Нп|Бета нормальна форма|нормальній формі||Beta normal form}}.

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

: {{tmath|((\lambda v.E) a) \Rightarrow E[v :{{=}} a]}}

За домовленістю, ми вважаємо {{tmath|(a b c)}} скороченням {{tmath|((a b) c)}} (тобто, застосування є [[Асоціативність|асоціативним зліва]]).

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

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

: Квадратом 3 є {{tmath|3*3}}

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

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

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

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

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

* {{Mvar|x}}
* {{Mvar|P}}
* {{tmath|(E_1 E_2)}}

де {{Mvar|x}}&nbsp;— змінна, {{Mvar|P}}&nbsp;— одна з примітивних функцій, і {{tmath|(E_1 E_2)}}є застосування комбінаторних термінів {{tmath|E_1}}і {{tmath|E_2}}. Самі примітивні функції є ''комбінаторами'', або функціями, які, якщо розглядати їх як лямбда-вирази, не містять [[Вільні і зв'язані змінні|вільних змінних]]. Щоб скоротити позначення, застосовується загальна домовленість {{tmath|(E_1 E_2 E_3 ... E_n)}}, або навіть {{tmath|E_1 E_2 E_3... E_n}}, позначає термін {{tmath|(...((E_1 E_2) E_3)... E_n)}}. Це та ж сама загальна домовленість (ліва асоціативність) що й для кількох аплікації в лямбда-численні.

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

: {{Math|1=(''P'' ''x''<sub>1</sub> ... ''x<sub>n</sub>'') = ''E''}}

де ''Е''&nbsp;— термін, що позначає лише змінні з множини {{{Math|''x''<sub>1</sub> ... ''x<sub>n</sub>''}}}. Саме таким чином примітивні комбінатори ведуть себе подібно функціям.

=== Приклади комбінаторів ===
Найпростішим прикладом комбінатора є '''I''' , комбінатор ідентичності, який визначається таким чином: ('''I''' ''x'') = ''x'' для всіх термінів ''x''.

Іншим простим комбінатором є '''K''' , який виробляє постійні функції: ('''K''' ''x'')&nbsp;— це функція, яка, для будь-якого аргументу, повертає ''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.''' Ми говоримо, що терміни {{Нп|Екстенсіональна рівність|поширюються однаково||Extensional equality}}. Рівень екстенсивності відображає математичне поняття рівності функцій: дві функції ''рівні,'' якщо вони завжди дають однакові результати для тих самих аргументів. Навпаки, самі вирази, разом із редукцією примітивних комбінаторів, фіксують поняття ''інтенсіональної рівності'' функцій: дві функції ''рівні,'' тільки якщо вони мають ідентичні реалізації до розширення примітивних комбінаторів, коли вони застосовані до достатньої кількості аргументів. Існує багато способів реалізації функції ідентичності; ('''SKK''') і '''I''' є серед цих шляхів, а також ('''SKS'''). Ми будемо використовувати слово ''еквівалентність'' для позначення екстенсійної рівності, залишаючи ''рівність'' для ідентичних комбінаторних виразів.

Більш цікавим комбінатором є {{Нп|Комбінатор фіксованої точки|комбінатор фіксованої точки||Fixed point combinator}} або комбінатор '''Y''' , який можна використовувати для реалізації [[Рекурсія|рекурсії]].

=== Повнота базису S-K ===
'''S''' і '''K''' можуть бути складені так, щоб виробляти комбінатори, які є екстенсивно рівними ''будь-якому'' лямбда-виразу, а отже, за тезою Черча, до будь-якої обчислювальної функції. Доказом є перетворення, ''T''[ ], який перетворює довільний лямбда-член в еквівалентний комбінатор.

''T''[&nbsp;] може бути визначено таким чином<ref name="Turner 1979">{{cite journal|last=Turner|first=David A.|authorlink=David Turner (computer scientist)|title=Another Algorithm for Bracket Abstraction|journal=The Journal of Symbolic Logic|volume=44|pages=267–270|year=1979|doi=10.2307/2273733|jstor=2273733}}</ref>:

# ''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''[&nbsp;] конструкція може розширити лямбда-вираз довжини ''n'' до комбінаторного виразу довжини [[Нотація Ландау|Θ]](''n''<sup>3</sup>)<ref>{{cite journal |last1=Lachowski |first1=Łukasz |title=On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic |journal=Reports on Mathematical Logic |date=2018 |issue=53 |pages=19-42 |doi=10.4467/20842589RM.18.002.8835 |url=http://www.ejournals.eu/rml/2018/Number-53/art/12285 |accessdate=9 вересня 2018 |archive-date=23 Квітня 2019 |archive-url=https://web.archive.org/web/20190423003138/http://www.ejournals.eu/rml/2018/Number-53/art/12285 }}</ref>.

==== Пояснення ''Т''[&nbsp;] перетворення ====
''T''[&nbsp;] перетворення мотивується прагненням усунути абстракцію. Два особливих випадки, правила 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''₂), тому рекурсія повинна закінчуватися в лямбда-виразі без жодних аплікацій&nbsp;— або змінні, або вирази виду ''λx''.''E.''

=== Спрощення перетворення ===

==== η-редукція ====
Комбінатори, що генеруються ''T''[&nbsp;] перетворенням можуть бути зменшені, якщо взяти до уваги правило ''η-редукції'' :

: ''T''[''λx''.(''E'' ''x'')] = ''T''[''E''] (якщо ''x'' не вільна в ''E'')

''λx''.(''E'' x)&nbsp;— функція, яка приймає аргумент ''x'', і застосовує до нього функцію ''E''; це екстенсійно дорівнює самій функції ''E.'' Тому достатньо перетворити ''E'' у комбінаторну форму.

Враховуючи це спрощення, виникає цей приклад:

: &nbsp; ''T''[''λx''.''λy''.(''y'' ''x'')]
:: = …
:: = ('''S''' ('''K''' ('''S I''')) ''T''[''λx''.('''K''' ''x'')])
:: = ('''S''' ('''K''' ('''S I''')) '''K''') (за η-редукцією)

Цей комбінатор еквівалентний більш ранньому, довшому:

: &nbsp; ('''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''[&nbsp;] перетворення трансформувала функцію тотожності ''λf''.''λx''.(''f'' ''x'') до ('''S''' ('''S''' ('''K S''') ('''S''' ('''K K''') '''I''')) ('''K I''')). За правилом η-редукції ''λf''.''λx''.(''f'' ''x'') перетворюється в '''I.'''

==== Одноточковий базис ====
Існують одноточкові базиси, з яких кожен комбінатор може бути складений екстенсійно рівним ''будь-якому'' лямбда-члену. Найпростішим прикладом такого базису є {'''X'''}, де:

: '''X''' ≡ ''λx''.((x'''S''')'''K''')

Не важко переконатися, що:

: '''X''' ('''X''' ('''X''' '''X''')) =<sup>ηβ</sup> '''K''' та
: '''X''' ('''X''' ('''X''' ('''X''' '''X'''))) = <sup>ηβ</sup> '''S.'''

Оскільки {'''K''', '''S'''} є базисом, то {'''X'''} також є базисом. Мова програмування {{Нп|Iota and Jot|Iota||Iota and Jot}} використовує '''X''' в якості свого єдиного комбінатора.

Іншим простим прикладом одноточкового базису є:

: '''X'''' ≡ ''λx''.(x '''K''' '''S''' '''K''') з: ('''X'''' '''X'''') '''X'''' =<sup>β</sup> '''K''' та
: '''X'''' ('''X'''' '''X'''') = <sup>β</sup> '''S'''

'''X'''' не потребує η контракції для отримання '''K''' і '''S.''' Фактично існує безліч таких базисів.<ref>{{cite journal | first=Mayer | last=Goldberg | url=http://www.sciencedirect.com/science/article/pii/S0020019003005416 | doi=10.1016/j.ipl.2003.12.005 | volume=89 | year=2004 | title=A construction of one-point bases in extended lambda calculi | journal=Information Processing Letters | pages=281–286 | accessdate=23 Квітня 2019 | archive-date=23 Квітня 2019 | archive-url=https://web.archive.org/web/20190423001642/https://www.sciencedirect.com/science/article/pii/S0020019003005416 }}</ref>

==== Комбінатори 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'''))

Ці комбінатори надзвичайно корисні при перекладі логіки предикатів або лямбда-числення в комбінаторні вирази. Їх також використовували [[Гаскелл Каррі|Каррі]], і набагато пізніше {{Нп|Девід Тернер|Девід Тернер||David Turner (computer scientist)}}, чиє ім'я було пов'язане з їх обчислювальним використанням. Використовуючи їх, ми можемо розширити правила перетворення таким чином:

# ''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'') виглядає так:

: &nbsp;&nbsp; ''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''') (η-редукція)
: = <math>\mathbf{C}_{*}</math> (традиційне канонічне позначення: <math>\mathbf{X}_{*} = \mathbf{X I}</math>)
: = <math>\mathbf{I}'</math>(традиційне канонічне позначення: <math>\mathbf{X}' = \mathbf{C X}</math>)

І дійсно, ('''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|B, C, K, W System||B, C, K, W System}}). У оригінальній роботі [[Шейнфінкель Мойсей Ейлєвич|Шейнфінкеля]] те, що ми називаємо '''S''', '''K''', '''I''', '''B''' і '''C''', називали '''S''' , '''C''' , '''I''' , '''Z''' і '''T''' відповідно.

Зменшення розміру комбінатора, що випливає з нових правил перетворення, також може бути досягнуто без введення '''B''' і '''C''', як показано в розділі 3.2.<ref>{{Cite book|title=Randomness And Complexity, from Leibniz To Chaitin|last=Tromp|first=John|year=2008|editor-last=Calude|editor-first=Cristian S.|publisher=World Scientific Publishing Company|chapter=Binary Lambda Calculus and Combinatory Logic}}</ref>

===== CL<sub>K</sub> проти CL<sub>I</sub> числення =====
Необхідно розрізняти '''CL'''<sub>K</sub>, як описано в цій статті, і обчислення '''CL'''<sub>I</sub>. Відмінність полягає в тому ж, що й між λ<sub>K</sub> і λ<sub>I</sub> численням.

На відміну від обчислення λ<sub>K</sub>, обчислення λ<sub>I</sub> обмежує абстракцію до ''λx''.''E'' де ''x'' має принаймні одне вільне входження в ''E''.

Як наслідок, комбінатор '''K''' не присутній у λ<sub>I</sub> обчисленнях, а також у численні '''CL'''<sub>I</sub>. Константами '''CL'''<sub>I</sub> є: '''I''', '''B''', '''C''' і '''S''', які є основою для складання всіх термінів '''CL'''<sub>I</sub> (рівність по модулю). Кожен термін λ<sub>I</sub> може бути перетворений в рівний комбінатор '''CL'''<sub>I</sub> згідно з правилами, подібними до описаних вище для перетворення термінів λ <sub>K</sub> в комбінатори '''CL'''<sub>K</sub>. Див. розділ 9 у Барендрегта (1984).

=== Зворотне перетворення ===
Перетворення ''L''[&nbsp;] від комбінаторних виразів до лямбда-виразів тривіальне:

: ''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''[&nbsp;] що ми бачили.

== Нерозв'язність комбінаторного числення ==
{{Нп|Нормальна форма (абстрактний рерайтинг)|Нормальною формою||Normal form (abstract rewriting)}} є будь-який комбінаторний термін, в якому примітивні комбінатори, які виникають, якщо такі є, не застосовуються до достатньої кількості спрощених аргументів. Не можна вирішити, чи має загальний комбінаторний термін нормальну форму; чи еквівалентні два комбінаторні терміни, і&nbsp;т.&nbsp;д. Це еквівалентно нерозв'язності відповідних задач для лямбда-виразів. Однак прямий доказ полягає в такому: По-перше, зауважте, що цей вираз

: '''Ω''' = '''(S''' ''''''I''' I''' '''(S''' ''''''I I))''''''

не має нормальної форми, оскільки вона зводиться до себе після трьох кроків, а саме:

: {{Spaces|2}} ('''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''' було комбінатором для виявлення нормальних форм, таких що

: <math>(\mathbf{N} \  x) = \begin{cases} \mathbf{T}, \text{ Якщо } x \text{ має нормальну форму} \\
\mathbf{F}, \text{ інакше.} \end{cases}</math>
: (Де {{Math|'''T'''}} і {{Math|'''F'''}} представляють звичайні {{Нп|Кодування Черча|кодування Черча||Church encoding}} для істинного і помилкового, ''λx''.''λy''.''x'' та ''λx''.''λy''.''y'', перетворені до комбінаторної логіки. Комбінаторні версії: {{Math|1='''T''' = '''K'''}} і {{Math|1='''F''' = ('''K''' '''I''')}} .)

Тепер нехай

: ''Z'' = ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''')

Тепер розглянемо термін ('''S''' '''I''' '''I''' ''Z''). Чи має ('''S''' '''I''' '''I''' ''Z'') нормальну форму? Так, але тоді і тільки тоді, коли:

: {{Spaces|2}} ('''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'') має нормальну форму, або ні. Якщо він має нормальну форму, то вищенаведене зменшується таким чином:

: {{Spaces|2}} ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
: = ('''K''' '''Ω''' '''I''')&nbsp; (визначення '''N)'''
: = '''Ω'''

але '''Ω''' ''не'' має нормальної форми, тому ми маємо протиріччя. Але якщо ('''S''' '''I''' '''I''' ''Z'') ''не'' має нормальної форми, вищезгадане зменшується таким чином:

: {{Spaces|2}} '''(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.'' Тоді аналог теореми Райса говорить, що кожен повний предикат тривіальний.  Доведення цієї теореми досить просте. <blockquote> '''Доказ:''' За допомогою 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''' буде повним нетривіальним предикатом.  '''[[Q.E.D.|QED]]''' </blockquote> З цієї теореми нерозв'язності відразу випливає, що немає повного предиката, який може розрізняти терміни, які мають нормальну форму, і терміни, які не мають нормальної форми.  Також випливає, що '''немає''' повного предиката, наприклад EQUAL, так що: 

: (EQUAL ''A B'') = '''T,''' якщо ''A'' = ''B'' і: (EQUAL ''A B'') = '''F,''' якщо ''A'' ≠ ''B''.

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

=== Компіляція функціональних мов ===
Девід Тернер використовував свої комбінатори для реалізації {{Нп|SASL (мова програмування)|мови програмування SASL||SASL programming language}}.

[[Кеннет Айверсон|Кеннет Е. Іверсон]] використовував примітиви на основі комбінаторів Каррі в його [[J (мова програмування)|мові програмування J]], наступнику [[APL]]. Це дозволило Іверсону застосувати так зване {{Нп|Мовчазне програмування|мовчазне програмування||Tacit programming}}, тобто програмування у функціональних виразах, що не містять змінних, а також потужні інструменти для роботи з такими програмами. Виявляється, мовчазне програмування можливе в будь-якій APL-подібній мові з визначеними користувачем операторами.<ref>{{cite journal |title=Pure Functions in APL and J |journal=Proceedings of the international conference on APL '91 |first=Edward |last=Cherlin |pages=88–93 |year=1991 |doi=10.1145/114054.114065}}</ref>

=== Логіка ===
[[Відповідність Каррі — Говарда|Ізоморфізм Каррі-Говарда]] передбачає зв'язок між логікою і програмуванням: кожне доведення теореми [[Інтуїціоністська логіка|інтуїціоністської логіки]] відповідає скороченню типового лямбда-терміна і навпаки. Крім того, теореми можна ідентифікувати за допомогою сигнатур типу функцій. Зокрема, типізована комбінаторна логіка відповідає системі Гільберта в [[Теорія доведення|теорії доказів]].

Комбінатори '''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'' всіх дедуктивно замкнутих множин формул, упорядкованих за [[Підмножина|включенням]]. Тоді <math>\langle W,\subseteq\rangle</math> є інтуїціоністичним [[Семантика Кріпке|кадром Крипке]], і ми визначаємо модель <math>\Vdash</math> в цьому кадрі таким чином: <math>X\Vdash A\iff A\in X</math>.

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

== Див. також ==
* [[Категоріальна абстрактна машина]]
* [[Лямбда-числення]]

== Примітки ==
{{reflist}}

== Подальше читання ==
* {{Cite book|title=The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics|last=Barendregt|first=Hendrik Pieter|authorlink1=Henk Barendregt|year=1984|publisher=North Holland|volume=Volume 103|isbn=0-444-87508-5|ref=harv}}
* {{Cite book|title=Combinatory Logic|last=Curry|first=Haskell B.|authorlink1=Гаскелл Каррі|last2=Feys|first2=Robert|authorlink2=Robert Feys|year=1958|publisher=North Holland|volume=Vol. I|location=Amsterdam|isbn=0-7204-2208-6}}
* {{Cite book|title=Combinatory Logic|last=Curry|first=Haskell B.|authorlink1=Гаскелл Каррі|last2=Hindley|first2=J. Roger|authorlink2=J. Roger Hindley|last3=Seldin|first3=Jonathan P.|year=1972|publisher=North Holland|volume=Vol. II|location=Amsterdam|isbn=0-7204-2208-6}}
* {{Cite book|title=Functional Programming|last=Field|first=Anthony J.|last2=Harrison|first2=Peter G.|authorlink2=Peter G. Harrison|year=1998|publisher=Addison-Wesley|isbn=0-201-19249-7|url-access=registration|url=https://archive.org/details/functionalprogra0000fiel}}
* {{Citation|last=Hindley|first=J. Roger|title=Principal type-schemes and condensed detachment|url=http://projecteuclid.org/euclid.jsl/1183743187|number=1|year=1990|last2=Meredith|first2=David|author-link=J. Roger Hindley|journal=[[Journal of Symbolic Logic]]|volume=55|doi=10.2307/2274956|jstor=2274956|mr=1043546|accessdate=5 Березня 2019|archive-date=6 Січня 2017|archive-url=https://web.archive.org/web/20170106013633/http://projecteuclid.org/euclid.jsl/1183743187}}
* {{Cite book|url=http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850|title=λ-calculus and Combinators: An Introduction|last=Hindley|first=J. R.|authorlink1=J. Roger Hindley|last2=Seldin|first2=J. P.|year=2008|publisher=Cambridge University Press|accessdate=5 Березня 2019|archive-date=10 Лютого 2017|archive-url=https://web.archive.org/web/20170210132003/http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850}}
* {{Cite book|url=http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz|title=Foundations of Functional Programming|last=Paulson|first=Lawrence C.|authorlink1=Lawrence Paulson|year=1995|publisher=University of Cambridge|accessdate=5 Березня 2019|archive-date=5 Липня 2017|archive-url=https://web.archive.org/web/20170705155443/http://www.cl.cam.ac.uk/teaching/Lectures/founds-fp/Founds-FP.ps.gz}}
* <span id="Quine 1960">{{cite journal |authorlink=Віллард Ван Орман Квайн |last=Quine |first=W. V. |year=1960 |title=Variables explained away |journal=Proceedings of the American Philosophical Society |volume=104 |issue=3 |pages=343–347 |jstor=985250}} Reprinted as Chapter 23 of Quine's ''Selected Logic Papers'' (1966), pp.&nbsp;227–235</span>
* [[Шейнфінкель Мойсей Ейлєвич|Schönfinkel, Moses]], 1924, «[http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf Über die Bausteine der mathematischen Logik] {{Webarchive|url=https://web.archive.org/web/20180408210251/http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf |date=8 Квітня 2018 }}», перекладена як «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. ''[https://web.archive.org/web/20051016213140/http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf Лекції з ізоморфізму Каррі-Говарда.]'' University of Copenhagen and University of Warsaw, 1999.
* {{cite book |last=Wolfengagen |first=V. E. |url=https://archive.org/details/CLP-2003_780 |title=Combinatory logic in programming: Computations with objects through examples and exercises |edition=2nd |location=Moscow |publisher="Center JurInfoR" Ltd. |year=2003 |isbn=5-89158-101-9}}.

== Посилання ==

* [[Стенфордська філософська енциклопедія]]: «[http://plato.stanford.edu/entries/logic-combinatory/ Комбінаторна логіка] {{Webarchive|url=https://web.archive.org/web/20190311113137/https://plato.stanford.edu/entries/logic-combinatory/ |date=11 Березня 2019 }}» від Katalin Bimbó.
* [https://web.archive.org/web/20070209093802/http://www.sadl.uleth.ca/gsdl/cgi-bin/library?a=p&p=about&c=curry 1920–1931&nbsp;рр. Блок-записки Каррі.]
* Keenan, David C. (2001) «[http://dkeenan.com/Lambda/index.htm Розкрити пересмішника: графічне позначення для лямбда-числення з анімованим зведенням] {{Webarchive|url=https://web.archive.org/web/20190219015653/http://dkeenan.com/Lambda/index.htm |date=19 Лютого 2019 }}»
* Ратман, Кріс, «[http://www.angelfire.com/tx4/cus/combinator/birds.html Комбінаторні птахи] {{Webarchive|url=https://web.archive.org/web/20080917002340/http://www.angelfire.com/tx4/cus/combinator/birds.html |date=17 Вересня 2008 }}» Таблиця, що виокремлює основну частину сутності книги Смалліана (1985).
* [https://web.archive.org/web/20081029051502/http://cstein.kings.cam.ac.uk/~chris/combinators.html Комбінатори перетягування.] (Java-аплет)
* [https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf Бінарне лямбда-числення та комбінаторна логіка.]
* [http://code.google.com/p/clache Комбінаторна логіка редукції вебсервера] {{Webarchive|url=https://web.archive.org/web/20111115204356/http://code.google.com/p/clache/ |date=15 Листопада 2011 }}

{{Бібліоінформація }}
[[Категорія:Лямбда-числення]]
[[Категорія:Математична логіка]]
[[Категорія:Логіка в інформатиці]]