B,C,K,Wシステムのソースを表示

'''B, C, K, W'''システムは、基本的な4つの定数記号 '''B, C, K, W''' からなる[[コンビネータ論理]]の変種である。この体系は[[ハスケル・カリー]]の博士論文''Grundlagen der kombinatorischen Logik''によるもので、その結論部分はCurry 1930において示された。

== 概要 ==
定数記号 '''B, C, K, W''' の簡約基の簡約規則は次のように定義される：
* '''B''' ''x y z'' → ''x'' (''y z'')
* '''C''' ''x y z'' → ''x z y''
* '''K''' ''x y'' → ''x''
* '''W''' ''x y'' → ''x y y''

これらのコンビネータは、直感的に次のような働きをするものと考えられる：
* '''B''' ''x y'' は関数合成。
* '''C''' ''x y z'' は引数交換。
* '''K''' ''x y'' は破棄；
* '''W''' ''x y'' は複製。

2つの基本的な定数記号 '''S, K'''（及び '''SKK''' と外延的に同値な閉項 '''I'''）からなる[[SKIコンビネータ計算]]があり、ここでは '''B, C, W''' は '''S, K''' からなる項によって次のように表現できる：
* '''B''' = '''S''' ('''K S''') '''K'''
* '''C''' = '''S''' ('''S''' ('''K''' ('''S''' ('''K S''') '''K''')) '''S''') ('''K K''')
* '''K''' = '''K'''
* '''W''' = '''S S''' ('''S K''')

一方で、'''S, K, I''' は '''B, C, K, W''' からなる項によって次のように表現できる：
* '''I''' = '''W K'''
* '''K''' = '''K'''
* '''S''' = '''B''' ('''B''' ('''B W''') '''C''') ('''B B''') = '''B''' ('''B W''') ('''B B C''').<ref>[[Raymond Smullyan]] (1994) ''Diagonalization and
Self-Reference''. Oxford Univ. Press: 344, 3.6(d) and 3.7.</ref>

すなわち、SKIコンビネータ計算とB,C,K,Wシステムは等価な計算体系である。

== 直観主義論理との関係 ==
定数記号 '''B, C, K, W''' はそれぞれよく知られた4つの[[命題論理]]の公理と対応する<ref>より正確には、定数記号の型と公理図式とが対応する。</ref>：

: '''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''': <math>A\to B,A\vdash B</math>

公理 '''AB, AC, AK, AW''' 及び推論規則 '''MP''' は、[[直観主義論理|直観主義命題論理]]の{{仮リンク|含意断片|en|Implicational propositional calculus}}に対して完全である。この体系に[[爆発原理]] '''F''' → '''A''' と[[排中律]]に類する規則（例：[[パースの法則]]）を加えたものは[[命題論理|古典命題論理]]と対応する。コンビネータ '''W''' とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-&lambda;計算と対応するものである。

== 関連項目 ==
* [[コンビネータ論理]]
* [[SKIコンビネータ計算]]
* [[ラムダ計算]]
* [[カリー＝ハワード同型対応]]
* {{仮リンク|To Mock a Mockingbird|en|To_Mock_a_Mockingbird}}

== 脚注 ==
{{Reflist}}

== 参考文献 ==
* [[Hendrik Pieter Barendregt]] (1984) ''The Lambda Calculus, Its Syntax and Semantics'', Vol. 103 in ''Studies in Logic and the Foundations of Mathematics''. North-Holland. ISBN 0-444-87508-5
* [[Haskell Curry]] (1930) "Grundlagen der kombinatorischen Logik," ''Amer.  J. Math. 52'': 509-536; 789-834.
* {{Cite book
| last1 = Curry | first1 = Haskell B.
| first2 = J. Roger | last2 = Hindley
| first3 = Jonathan P. | last3 = Seldin
| authorlink1 = Haskell Curry
| authorlink2 = J. Roger Hindley
| authorlink3 = Jonathan P. Seldin
| title = Combinatory Logic
| volume = Vol. II
| year = 1972
| publisher = North Holland
| location = Amsterdam
| isbn = 0-7204-2208-6
}}
* [[Raymond Smullyan]] (1994) ''Diagonalization and Self-Reference''. Oxford Univ. Press.

== 外部リンク ==
* Keenan, David C. (2001) "[http://dkeenan.com/Lambda/index.htm To Dissect a Mockingbird.]"
* Rathman, Chris, "[http://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.]"
* "[http://cstein.kings.cam.ac.uk/~chris/combinators.html "Drag 'n' Drop Combinators (Java Applet).]"

[[Category:コンビネータ論理]]