SKI COMBINATORS computation with no variables at all
Three constants — S, K, I — and two rewrite rules turn any lambda program into a tree of applications with no bound variables. Rules: I x = x; K x y = x; S x y z = x z (y z). That is Turing-complete: every computable function is a fixed tree of S/K/I. And I is redundant — I = S K K — so two combinators suffice.
THE TECHNIQUE pure rewriting, no names
Reduce S K K x by the rules alone: S K K x → K x (K x) → x. So S K K behaves exactly like I — the identity, built with no variable ever named. Below: the reduction, step by step, variable-free. live demo
HISTORY & CREDIT Schönfinkel 1920, not Curry, not Turner
“Curry invented combinators” — no; Schönfinkel introduced them in a 1920 Göttingen talk; Curry invented independently rediscovered them (1927) and built the formal theory. cited
1920 / 1924 · Moses Schönfinkel — “Über die Bausteine der mathematischen Logik”: combinators to eliminate bound variables. (His letters were S, C, I, Z, T — C was the constant K.) 1927–30 · Haskell Curry independently rediscovers them at Princeton, coins the theory of combinatory logic and the modern letters B, C, K, W. 1936–37 · Church / Turing — the lambda calculus (hence SKI) computes exactly the Turing-computable functions: SKI is Turing-complete. (Church-Rosser, 1936, separately gives confluence — a unique normal form.) 1958 / 1979 · Curry & Feys consolidate bracket abstraction (compile any lambda to S/K/I); David Turner compiles a lazy functional language to SK combinators and runs it by graph reduction (dart 145) — engineering, not the calculus.
You do not even need I (= S K K), and Schönfinkel showed S and K alone suffice; a single-combinator basis (Iota) came in 2001. Schönfinkel, 1920
RECOMMEND FOR I-13 the variable-free calculus — nothing to store
Because there are no variables, there is no environment to store — the rules are pure tag-dispatch rewriting, and the identity falls out:
$ i13 run ski.i13 # rules only, x encoded as the value 7
I 7 = 7 K 7 99 = 7
S K K 7 = (K 7)(K 7) = 7 == I 7 -> S K K = I, with NO variables anywhere
Recommend: the rules are LIT — S, K, I are tag-dispatched reducers over an argument stack; a combinator with enough arguments fires its rule; there is no environment because there are no variables to bind (verified I 7 = 7, K 7 99 = 7, and S K K 7 = 7 = I 7, so S K K = I). This is the corpus’s computed-not-stored axis in its purest form: identity is computed by reduction, never a stored name. Note: a general term is a graph of applications (a node arena, PS-015) reduced by graph reduction (dart 145); the corpus grounds the reduction rules on the saturated redex. Combinators are how Turner ran a real functional language with no variables at all — the same closureless fit as defunctionalization (dart 147).