B,C,K,W system
Encyclopedia : B : BC : BCK : B,C,K,W system
Haskell Curry, in his doctoral thesis Grundlagen der kombinatorischen Logik [GKL], already proposed a system with separated functional characteristics: association, conversion, cancellation and duplication. If in addition we request regular, proper (and between these, minimals) combinators they are, B, C, K and W (today nomenclature). As it is difficult to have the original system of combinatorial axioms we reproduce here the version given by Rosenbloom in The Elements of Mathematical Logic, where he uses application prefix which we change into usual infix notation and, in the context to recover [GKL], leave I without defining it: so, beware!.
Contents
Axioms
- 1) BI = I
- 2) C(BB(BBB))B = B(BB)B
- 3) C(BB(BBB))C = B(BC)(BBB)
- 4) C(BBB)W = B(BW)(BBB)
- 5) C(BBB)K = B(BK)I
- 6) CBI = I
- 7) B(B(BC)C)(BB) = BBC
- 8) B(B(B(B(BW)W)(BC)))(BB)(BB) = BBW
- * error [EML]?
- ** 8) B(B(B(B(BW)W)(BC)))B(BB)B = BBW
- 9) BBK =BKK
- 10) BCC = I
- 11) B(B(BC)C)(BC) = B(BC(BC))C
- 12) B(B(BW)C)(BC) = BCW
- 13) BCK = BK
- 14) BWC = W
- 15) BW(BW) = BWW
- 16) BWK = I
Rules
We assume the rules of the equality.
Combinatorial ones are presented like equations:
- B x y z = x (y z)
- C x y z = x z y
- K x y = x
- W x y = x y y
See also
Works
- [GKL] Curry, Haskell B.; Grundlagen der kombinatorischen Logik; Amer. J. Math.; 52:509-536;789-834 (1930)
- [EML] Rosenbloom, Paul C.; The Elements of Mathematical Logic, Dover 1950;
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.