BCKW System( http://en.wikipedia.org/wiki/B,C,K,W_system )

BCKW

The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W.
BCKWシステムとは、B、C、K、Wの四つの組み込みコンビネータを持つコンビネータ算法の一種である。
This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930).
このシステムは、ハスケル・カリーによって
The combinators are defined as follows:
四つのコンビネータは以下のように定義される。
B x y z = x (y z)
C x y z = x z y
K x y = x
W x y = x y y
Intuitively,
B x y is the composition of the arguments x and y;
C x y z swaps the arguments y and z;
K x y discards the argument y;
W x y duplicates the argument y.
直感的には、
B x y は、引数のxとyを関数合成し、
C c y z は、引数のyとzを入れ替え、
K x y は、引数のyを単に捨て、
W x y は、引数のyを複製する。 
In recent decades, the SKI combinator calculus, with only two primitive combinators, K and S, has become the canonical approach to combinatory logic. 
近年では、KとSのみを組み込みのコンビネータに持つSKIコンビネータ算法が、コンビネータ算法の主力である。(？？)
B, C, and W can be expressed in terms of S and K as follows:
B、C、K、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)
Going the other direction, SKI can be defined in terms of B,C,K,W as:
逆に、S、K、IもそれぞれBCKWを用いて以下のように表すことができる。
I = W K
K = K
S = B (B (B W) C) (B B) = B (B W) (B B C).[1]
Contents  [hide] 
1 Connection to intuitionistic logic
2 See also
3 Notes
4 References
5 External links
[edit]Connection to intuitionistic logic

The combinators B, C, K and W correspond to four well-known axioms of sentential logic:
BCKWのコンビネータは、それぞれ四つのよく知られた命題論理の公理に対応する。
AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).
Function application corresponds to the rule modus ponens:
関数適用は、モーダスポネンスに対応する。
MP: from A and A → B infer B.
The axioms AB, AC, AK and AW, and the rule MP are complete for the implicational fragment of intuitionistic logic. 
AB、AC、AK、AWの公理、MPの推論規則は直感主義論理に対応するものを構成する。
In order for combinatory logic to have as a model:
The implicational fragment of classical logic, would require the combinatory analog to the law of excluded middle, e.g., Peirce's law;
Complete classical logic, would require the combinatory analog to the sentential axiom F → A.
[edit]See also

Combinatory logic
SKI combinator calculus
Lambda calculus
To Mock a Mockingbird
[edit]Notes

^ Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.
[edit]References

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.
Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press.
[edit]External links

Keenan, David C. (2001) "To Dissect a Mockingbird."
Rathman, Chris, "Combinator Birds."
""Drag 'n' Drop Combinators (Java Applet)."
View page ratings
Rate this page
What's this?
Trustworthy
Objective
Complete
Well-written
I am highly knowledgeable about this topic (optional)

Submit ratings
Categories: Combinatory logicLambda calculus