Система B, C, K, W

Система B, C, K, W это вариант комбинаторной логики , который принимает в качестве примитива комбинаторы B, C, K и W. — Эта система была открыта Хаскеллом Карри в его докторской диссертации Grundlagen der kombinatorischen Logik , результаты которой изложены у Карри (1930).

Определение

Комбинаторы определяются следующим образом:

• B x yz знак равно x ( yz )
• C x yz = xzy
• К х у = х
• Ш х у = хуу

Интуитивно,

• B x — композиция x и y ; y
• C x — это x с перевернутым порядком аргументов ;
• K x — функция «константа x », которая отбрасывает следующий аргумент;
• W дублирует свой второй аргумент для удвоенного приложения в первый. Таким образом, он «объединяет» два ожидания ввода своего первого аргумента в одно.

Подключение к другим комбинаторам

В последние десятилетия комбинаторное исчисление SKI , имеющее только два примитивных комбинатора, K и S , стало каноническим подходом к комбинаторной логике . B, C и W можно выразить через S и K следующим образом:

• Б знак равно S ( КС ) К
• C знак равно S ( S ( K ( S ( KS ) K )) S ) ( KK )
• К = К
• W = СС ( СК )

Другой способ — после определения B , как указано выше, дополнительно определить C = S ( BBS )( KK ) и W = CSI .

В другом направлении SKI можно определить через B, C, K, W как:

• Я = ВК
• К = К
• S знак равно B ( B ( BW ) C ) ( BB ) знак равно B ( BW ) ( BBC ).

Также следует отметить, что комбинатор Y имеет короткое выражение в этой системе: Y = BU ( CBU ), где U = WI = SII — комбинатор для самостоятельного применения. Тогда Y г = U ( B г U ) = B г U ( B г U ) = г ( U ( B г U )) = г ( Y г ).

Связь с интуиционистской логикой

Комбинаторы B , C , K и W соответствуют четырем известным аксиомам логики предложений :

AB : ( B → C ) → (( A → B ) → ( A → C )),

AC : ( A → ( B → C )) → ( B → ( A → C )),

АК : А → ( Б → А ),

АВ : ( А → ( А → Б )) → ( А → Б ).

Применение функции соответствует правилу modus ponens :

МП : А → Б и А выводится Б. из

Аксиомы AB , AC , AK и AW , а также правило MP полны для импликативного фрагмента интуиционистской логики . Чтобы комбинаторная логика имела в качестве модели:

• Импликативный фрагмент классической логики потребовал бы комбинаторного аналога закона исключенного третьего , например, закона Пирса ;
• Полная классическая логика комбинаторного аналога аксиомы предложений F → A. потребовала бы

См. также

• Комбинаторная логика
• Комбинаторный расчет SKI
• Лямбда-исчисление
• Посмеяться над пересмешником

Ссылки

• Хендрик Питер Барендрегт (1984) Лямбда-исчисление, его синтаксис и семантика , Vol. 103 в исследованиях по логике и основам математики . Северная Голландия. ISBN   0-444-87508-5
• Хаскелл Карри (1930) «Основы комбинаторной логики», Amer. J Math 52 : 509–536; 789-834. https://doi.org/10.2307/2370619
• Карри, Хаскелл Б .; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Том. II. Амстердам: Северная Голландия. ISBN  0-7204-2208-6 .
• Раймонд Смалльян (1994) Диагонализация и самореференция . Оксфордский университет. Нажимать.

Внешние ссылки

• Кинан, Дэвид К. (2001) « Препарировать пересмешника » .
• Рэтман, Крис, « . Птицы-комбинаторы »
• Комбинаторы перетаскивания (Java-апплет). "