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 ). [1]
Связь с интуиционистской логикой [ править ]
Комбинаторы 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 .
См. Также [ править ]
Заметки [ править ]
Ссылки [ править ]
- Хендрик Питер Барендрегт (1984) Лямбда-исчисление, его синтаксис и семантика , Vol. 103 в исследованиях по логике и основам математики . Северная Голландия. ISBN 0-444-87508-5
- Хаскелл Карри (1930) "Grundlagen der kombinatorischen Logik", Amer. J. Math. 52 : 509–536; 789–834.
- Карри, Хаскелл Б .; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Vol. II. Амстердам: Северная Голландия. ISBN 0-7204-2208-6.
|volume=имеет дополнительный текст ( справка )CS1 maint: обескураженный параметр ( ссылка ) - Раймонд Смуллян (1994) Диагонализация и самоотнесение . Oxford Univ. Нажмите.
Внешние ссылки [ править ]
- Кинан, Дэвид С. (2001) « Чтобы рассечь пересмешника ».
- Ратман, Крис, « Комбинатор птиц ».
- " " Комбинаторы перетаскивания (Java-апплет). "
