SKI combinators

Three combinators, S x y z = x z (y z), K x y = x and I x = x, from which every closed lambda term can be built by application alone, with no variables. I is redundant, since S K K x = x. The translation from lambda terms is called bracket abstraction.

S x y z K x y I x = x z (y z) = x = x

$I$ is not needed:

S K K x = K x (K x) = x

Bracket abstraction $[x] M$ removes a variable from a combinator term, so that $([x] M) N$ behaves like $M$ with $N$ for $x$ :

[x] M = ⎩ ⎨ ⎧ I K M S ([x] P) ([x] Q) M = x x \in / FV (M) M = P Q

The last rule is correct because $S ([x] P) ([x] Q) N = ([x] P) N (([x] Q) N) = P [N / x] Q [N / x] = (P Q) [N / x]$ . A λ-term compiles innermost binder first.

A compiler from λ-terms to S, K, I, and a reducer for the result.

type lam = V of string | L of string * lam | A of lam * lam
type ski = S | K | I | Var of string | App of ski * ski
 
let rec free x = function
  | Var y -> x = y
  | App (a, b) -> free x a || free x b
  | S | K | I -> false
 
(* Bracket abstraction: [x] M is a combinator term that, applied to N,
   behaves like M with N for x. *)
let rec abstract x = function
  | Var y when y = x -> I
  | m when not (free x m) -> App (K, m)
  | App (m, n) -> App (App (S, abstract x m), abstract x n)
  | _ -> assert false
 
let rec compile = function
  | V x -> Var x
  | A (m, n) -> App (compile m, compile n)
  | L (x, m) -> abstract x (compile m)
 
(* Weak reduction: S x y z -> x z (y z), K x y -> x, I x -> x. *)
let rec whnf t =
  match t with
  | App (I, x) -> whnf x
  | App (App (K, x), _) -> whnf x
  | App (App (App (S, x), y), z) -> whnf (App (App (x, z), App (y, z)))
  | App (f, x) ->
      let f' = whnf f in
      if f' == f then t else whnf (App (f', x))
  | _ -> t
 
let rec normal t = match whnf t with App (f, x) -> App (normal f, normal x) | t -> t
 
let rec show = function
  | S -> "S" | K -> "K" | I -> "I" | Var x -> x
  | App (f, (App _ as x)) -> show f ^ " (" ^ show x ^ ")"
  | App (f, x) -> show f ^ " " ^ show x

Running it.

S K K x                ->  x
compile (\x. \y. x)    ->  S (K K) I
compile flip           ->  S (S (K S) (S (K K) (S (K S) (S (S (K S) (S (K K) I)) (K I))))) (K (S (K K) I))
(compile flip) g u v   ->  g v u

$λ x . λ y . x$ compiles to $S (K K) I$ , which is $K$ only after the η-rule $[x] (M x) = M$ . flip, three binders deep, is already 25 combinators. Turner added $B x y z = x (y z)$ and $C x y z = x z y$ , for applications where only one side mentions the variable, and implemented SASL and Miranda this way:^[3] compile to combinators, then reduce a graph of them.