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
- error [EML]?
- 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;