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

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

Определение

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

• B x yz = x ( yz )
• C x yz = xzy
• К х у = х
• W x y = xyy

Интуитивно

• В й уге является композицией из аргументов х и у , приложенных к аргументу г ;
• C x yz меняет местами аргументы y и z ;
• K x y отбрасывает аргумент y ;
• W x y дублирует аргумент y .

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

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

• B = S ( KS ) K
• С = S ( S ( K ( S ( KS ) K )) S ) ( KK )
• К = К
• W = SS ( SK )

С другой стороны, SKI можно определить в терминах B, C, K, W как:

• I = WK
• К = К
• S = B ( B ( BW ) C ) ( BB ) = B ( BW ) ( BBC ).

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

Комбинаторы B , C , K и W соответствуют четырем хорошо известным аксиомам сентенциальной логики :

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

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

АК : А → ( В → А ),

AW : ( A → ( A → B )) → ( A → B ).

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

MP : от A и A → B Infer B .

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

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

Смотрите также

• Комбинаторная логика
• Расчет комбинатора SKI
• Лямбда-исчисление
• Издеваться над пересмешником

Примечания

использованная литература

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

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

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