B,C,K,W system

From TheBestLinks.com

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!.

Table of 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 asume 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

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;

es:Sistema B,C,K,W

Discussion

Last posted 0 of 0 messages

[no messages posted yet]

>> post message >>

Watch

You can add this article to your own "watchlist" and receive e-mail notification about all changes in this page.

Retrieved from "http://www.thebestlinks.com/B__2C__C__2C__K__2C__W_system.html"