B，_C，_K，_W_system
B、C、K、Wシステムの変形である結合論理結合子プリミティブとして受け取りB、C、K、およびW。このシステムは、ハスケル・カリーが博士論文Grundlagen der kombinatorischen Logikで発見し、その結果はカリー（1930）に示されています。
コンテンツ
1 意味
2 他のコンビネータへの接続
3 直観主義論理への接続
4 も参照してください
5 ノート
6 参考文献
7 外部リンク
意味
コンビネータは次のように定義されます。
B x yz = x（yz）
C x yz = xzy
K x y = x
W x y = xyy
直感的に、
Bは、 YZは、xである組成物の引数 のxとyは引数に適用Z。
C x yzは、引数yとzを交換します。
Kは、 Yは、X引数廃棄Yを、
W 、X yは引数複製Yを。
他のコンビネータへの接続
ここ数十年で、KとSの2つのプリミティブコンビネータのみを備えたSKIコンビネータ計算は、コンビネータ論理への標準的なアプローチになりました。B、C、およびWは、次のようにSおよびKで表すことができます。
B = S（KS）K
C = S（S（K（S（KS）K））S）（KK）
K = K
W = SS（SK）
反対方向に進むと、SKIはB、C、K、Wの観点から次のように定義できます。
I = WK
K = K
S = B（B（BW）C）（BB）= B（BW）（BBC）。
直観主義論理への接続
コンビネータB、C、K、およびWは、センテンス論理の4つのよく知られた公理に対応します。
AB：（B C）（（A B）（A C））、
AC：（A （B C））（B （A C））、 AK： A （B A）、
AW：（A （A B））（A B）。
関数適用はルールモーダスポネンスに対応します：
MP：からと
B推論 B。 公理AB、AC、AK、AW、およびルールMPは、直観主義論理の含意的な断片に対して完全です。コンビネータ論理をモデルとして持つためには：
implicationalフラグメントの古典論理は、へコンビナトリーアナログが必要となる排中律、例えば、パースの法則を。
完全な古典論理は、知覚公理F Aの組み合わせアナログを必要とします。
も参照してください
コンビネータ論理
SKIコンビネータ計算
ラムダ計算
モッキンバードをあざけるには
ノート
^ Raymond Smullyan（1994）対角化と自己参照。オックスフォード大学 プレス：344、3.6（d）および3.7。
参考文献
Hendrik Pieter Barendregt（1984）The Lambda Calculus、its Syntax and Semantics、Vol。論理学と数学の基礎の103 。北ホラント。ISBN 0-444-87508-5
Haskell Curry（1930）「Grundlagender kombinatorischen Logik」、Amer。J.数学。52：509–536; 789〜834。https://doi.org/10.2307/2370619
カリー、ハスケルB。; ハインドリー、J。ロジャー; セルディン、ジョナサンP.（1972）。コンビネータ論理。巻 II。アムステルダム：北ホラント。ISBN 0-7204-2208-6。 |volume=余分なテキストがあります（ヘルプ）
Raymond Smullyan（1994）対角化と自己参照。オックスフォード大学 押す。
外部リンク
キーナン、デビッドC.（2001）「モッキンバードを解剖する。」
ラスマン、クリス、「コンビネーターバード」。
” “ドラッグ ‘n’ドロップコンビネータ（Javaアプレット）。「」