Combinatory logic

From Esolang
(Redirected from SKI combinator calculus)
Jump to navigation Jump to search
Not to be confused with Combinational logic.

Combinatory logic is a model by which logical statements can be described as a combination of a small number of primitive elements called combinators. Each combinator is like a function or lambda abstraction, but without any free variables. A "sentence" in combinatory logic is called a combinatory term, and is composed of combinators, free variables, and applications of one combinatory term to another.

Combinatory logic can capture the meaning of any arithmetic or logical statement (and by extension, any non-interactive computer program), making it a Turing-complete computational model. It is often described and/or implemented in terms of rewriting (of graphs, trees, or terms).

Combinatory logic forces you to use pointfree programming style to write useful programs.

Syntax

The syntax commonly used for combinators is like that of the lambda calculus: each combinator only takes one argument (but may yield another combinator which will consume further arguments), application associates to the left, and parentheses are only used for disambiguation, not to delimit an argument list.

If you wish to see the grammar of pure combinatory logic, it is as such: 

combinator ::= Combinator_Symbol ;
app        ::= exp exp ;
parenexp   ::= "(" exp ")" ;
expression ::= app | parenexp | combinator ;

This is a fairly simple grammar, so it will not be explained here.

The syntax of the commonly-used combinatory logic (with assignments and such) is: 

combinator ::= Combinator_Symbol ;
var        ::= Var_Symbol ;
app        ::= exp exp ;
parenexp   ::= "(" exp ")" ;
expression ::= app | parenexp | combinator ;
assignment ::= combinator {var} "=" expression {var} ;
line       ::= expression | assignment ;

Combinators

SKI calculus

In 1924, Moses Schönfinkel devised the three traditional primitive combinators. All other expressions can be formed by application of these combinators to each other:

  • I, the identity combinator. Applied to some combinator x, it simply evaluates to x:
I x = x;
  • K, the constant-making combinator. Applied to some combinator x, it yields a combinator that always evaluates to x, no matter what it is applied to:
K x y = x;
  • S, the application combinator. Applied to three combinators, it applies each of the first two combinators to the last, then applies the first result of that to the second:
S f g x = f x (g x);

In fact, only two different combinators are strictly necessary; the I combinator can be formed from the S and K combinators: 

S K K x = I x = x

BCKW calculus

The original system of four primitive combinators, used by Haskell Curry and equivalent to SKI, were B, C, K, and W. These are defined by: 

B x y z = x (y z);
C x y z = x z y;
K x y = x;
W x y = x y y;

To define the B, C, K, W primitives from the SKI system, you can use the expressions: 

B = S (K S) K;
C = S (B B S) (K K);
K = K;
W = S S (S K);

Derivations to prove these (follow them by eta conversions): 

S (K S) K x y z = K S x (K x) y z = S (K x) y z = K x z (y z) = x (y z) = B x y z;
S (B B S) (K K) x y z = B B S x (K K x) y z = B B S x K y z = B (S x) K y z = S x (K y) z = x z (K y z) = x z y = C x y z;
S S (S K) x y = S x (S K x) y = x y (S K x y) = x y (K y (X y)) = x y y = W x y;

To define the S, K, I primitives from the BCKW system (two alternative definitions are given for S), use: 

S = B (B (B W) C) (B B) = B (B W) (B B C);
K = K;
I = W K;

Derivations to prove these (follow them by eta conversions): 

B (B W) (B B C) x y z = B W (B B C x) y z = W (B B C x y) z = B B C x y z z = B (C x) y z z = C x (y z) z = x z (y z) = S x y z;
B (B (B W) C) (B B) x y z = B (B W) C (B B x) y z = B W (C (B B x)) y z = W (C (B B x) y) z = C (B B x) y z z = B B x z y z = B (x z) y z = x z (y z) = S x y z;
I y = W K y = K y y = y;

Alternative Primitives

Though SK(I) is the traditional set of primitives, some alternative primitives have been created with different goals. For example, Iota, where ιx = (xs)k. or the minimal basis λx λy λz. x z (y (λ_.z)).

Non-primitives

Various other non-primitive combinators have been defined. For another, longer example, the named birds from "To Mock a Mockingbird" are: 

B = S(KS)K               #Bluebird
B[1] = BBB               #Blackbird
B[2] = B(BBB)B           #Bunting
B[3] = B(BB)B            #Becard
C = S(BBS)(KK)           #Cardinal
D = BB                   #Dove
D[1] = B(BB)             #Dickcissel
D[2] = BB(BB)            #Dovekies
E = B(BBB)               #Eagle
Ê = B(BBB)(B(BBB))       #Bald Eagle
F = ETTET                #Finch
G = BBC                  #Goldfinch
H = BW(BC)               #Hummingbird
I = SKK                  #Identity Bird/Idiot
J = B(BC)(W(BC(B(BBB)))) #Jay
L = CBM                  #Lark
M = SII                  #Mockingbird
M[2] = BM                #Double Mockingbird
O = SI                   #Owl
Q = CB                   #Queer Bird
Q[1] = BCB               #Quixotic Bird
Q[2] = C(BCB)            #Quizzical Bird
Q[3] = BT                #Quirky Bird
Q[4] = F*B               #Quacky Bird
R = BTT                  #Robin
T = CI                   #Thrush
U = LO                   #Turing (!!!)
V = BCT                  #Vireo/Pairing
W[1] = CW                #Converse Warbler
Y = SLL                  #Why Bird/Sage Bird
I* = S(SK)               #Identity Bird Once Removed
W* = BW                  #Warbler Once Removed
C* = BC                  #Cardinal Once Removed
R* = C*C*                #Robin Once Removed
F* = BC*R*               #Finch Once Removed
V* = C*F*                #Vireo Once Remvoed
W** = B(BW)              #Warbler Twice Removed
C** = BC*                #Cardinal Twice Removed
R** = BR*                #Robin Twice Removed
F** = BF*                #Finch Twice Removed
V** = BV*                #Vireo Twice Removed
ω = MM                   #OMEGA BIRD xD
θ = YO                   #Theta (Bird?)

Example

Let's trace through S K K x, both to show that it is equivalent to I x, and just as an example of how combinatory logic works.

First, S applies each of its first two arguments to its last argument, so the expression S K K x can be thought of as reducing to: 

K x (K x)

Further, for simplicity's sake, K x can be thought of as yielding a combinator that, when applied to anything, yields x. We'll call this combinator yields-x to demonstrate, even though it wouldn't really be used: 

yields-x yields-x

Finally, yields-x is applied to itself. But, no matter what it is applied to, even itself, the result will always be x: 

x

So from this we can see that S K K x is equivalent to I x.

See also

External resources

Retrieved from "https://esolangs.org/w/index.php?title=Combinatory_logic&oldid=146889"