An experiment in SKI combinator calculus, below are the accompanying blog posts, originally on my blog:
S, K, and I are the name of three combinators. Perhaps surprisingly, these combinators together is sufficient to form a Turing-complete language 1, albeit very tedious to write. Any expression in lambda calculus can be translated into the SKI combinator calculus via a process called abstraction elimination, and that is what this post will be exploring.
Combinators are functions without free variables, for example, in pseudo-Haskell syntax:
id x = x is a combinator that returns it's argument unchanged.
And here is what the SKI combinators do:
I x = x
K x y = x
S x y z = x z (y z)
I is the identity function, K behaves like a two argument identity function, returning the first argument passed to it, S performs substitution (function application). Here are some examples:
I I = I
K K I = K
S K S K = K K (S K) = K
To be more precise, the SKI combinator calculus is made up of terms:
- S, K, and I are terms
(x y)are terms ifxandyare terms
Thus an expression in the SKI system can be visualized as a binary tree, each leaf node being S, K, or I, and an inner node representing the parentheses.
Let's define an abstract syntax tree for an SKI expression like so:
type ski =
| I
| K
| S
| T of ski * skiThus the terms used in the examples above can be constructed as such:
T (I, I) (* I I *)
T (T (K, K), I) (* K K I *)
T (T (T (S, K), S), K) (* S K S K *)With the abstract syntax tree, we can now try to reduce or interpret the SKI expressions. We will be looking at two different ways of doing so, the first is by interpreting recursively, the second is by running it as a stack machine.
We interpret expressions by pattern matching on the structure of the abstract syntax tree:
let rec interp c =
match c with
(* leaf node, remain unchanged *)
| I | K | S -> c
(* an I term, reduce argument *)
| T (I, x) -> interp x
(* a K term, reduce first argument *)
| T (T (K, x), y) -> interp x
(* an S term, perform substitution *)
| T (T (T (S, x), y), z) ->
interp (T (T (x, z), T (y, z)))
(* any other term *)
(* the goal here is to check if terms are reducible *)
(* to prevent infinite recursion *)
| T (c1, c2) ->
let c1' = interp c1 in
let c2' = interp c2 in
if c1 = c1' && c2 = c2'
then T (c1, c2)
else interp (T (c1', c2'))The idea for a stack machine based reduction of the SKI calculus is from 2
First we define a step function for the machine, which works on the current term, and updates the stack based on the calculus rules.
type step =
(* able to perform next step with term and current stack *)
| Step of (ski * ski list)
(* no reduction possible anymore *)
| End of ski
let step term stack =
match (term, stack) with
(* I term, work on the top term in the stack *)
| I, x::s -> Step(x , s)
(* K term, work on the top term, discard the second *)
| K, x::y::s -> Step(x, s)
(* works on the substituted term *)
| S, x::y::z::s ->
Step(T (T (x, z), T(y, z)), s)
(* push the second pargument onto the stack *)
| T (c1, c2), s -> Step(c1, c2 :: s)
(* empty stack, return as the result of reduction *)
| e, [] -> End e
(* no idea how to handle this *)
| _ -> failwith "Unrecognized term"Then a full run of an expression will be running the step function until we hit the end:
let run term =
let rec go term stack =
match step term stack with
| End e -> e
| Step (e, s') -> go e s'
in
go term []Next up: translating terms in lambda calculus to SKI combinators.
- Wikipedia SKI Combinator calculus
- Wikipedia Combinatory Logic
- The SKI Combinator Calculus a universal formal system
- eperdew's implementation in OCaml
- bmjames' implementation in Erlang
- yager's implementation in Haskell
- ac1235's implementation in Haskell's happy
In a previous post, we looked at what SKI combinators are, and how to encode and interpret them. We also mentioned that these 3 combinators form a Turing-complete language, because every lambda calculus term can be translated into an SKI combinator term.
Source code is available here
The lambda calculus is a simple Turing-complete language.
Lambda calculus is made up of three terms:
- Variable, such as
x, - Lambda abstraction, such as
fun x -> x, - Application, such as
(y x).
(* lambda calculus AST *)
type name = string
type lambda =
| Var of name
| App of lambda * lambda
| Abs of name * lambdaHere's an example lambda term, representing the application of an identity function to an identity function:
App (Abs ('x', Var 'x'), Abs ('y', Var 'y'))Let us conjure an ideal function that will do such a translation, it should take a lambda term to an SKI term:
let convert (e : lambda) : ski = (??)What this means is that we can either have a lambda term, or an ski term, with no in-betweens, i.e. we cannot have a lambda term containing an ski term.
However, if we look at the translation rules, we find that we will need a intermediate structure that can hold both lambda terms and ski terms.
For example in clause 5, T[λx.λy.E] => T[λx.T[λy.E]],
the translated term T[λy.E], which by definition is an SKI term,
is the body of a lambda abstraction.
So it is helpful to define such a structure, which allows lambda calculus terms and SKI terms to coexist:
(* Intermediate AST for converting lambda calculus into SKI combinators.
* This is needed because when converting, intermediate terms can be
* a mixture of both lambda terms and SKI terms, for example
* a lambda expression with a SKI body, \x . K
* *)
type ls =
| Var of name
| App of ls * ls
| Abs of name * ls
| Sl
| Kl
| Il
| Tl of ls * ls
(* String representation of ls *)
let rec string_of_ls (l : ls) : string = match l with
| Var x -> x
| App (e1, e2) -> "(" ^ (string_of_ls e1) ^ (string_of_ls e2) ^ ")"
| Abs (x, e) -> "\\" ^ x ^ (string_of_ls e)
| Sl -> "S"
| Kl -> "K"
| Il -> "I"
| Tl (e1, e2) -> "(T " ^ (string_of_ls e1) ^ (string_of_ls e2) ^ ")"We will also need a helper function to determine if a variable is free in an expression:
(* Is x free in the expression e? *)
let free x (e : ls) =
(* Get free variables of an expression *)
let rec fv (e : ls) = match e with
| Var x -> [x]
| App (e1, e2) -> fv e1 @ fv e2
| Abs (x, e) -> List.filter (fun v -> v != x) (fv e)
| Tl (e1, e2) -> fv e1 @ fv e2
| _ -> []
in
List.mem x (fv e)The core translation algorithm then follows the translation scheme
described in the
Wikipedia article.
We make use of the intermediate structure, ls, when translating.
The signature of this structure doesn't say much, it looks like an identity function,
but the assumption is that the input term is converted from a lambda term,
made up of Var, App, and Abs, and the output term will only contain
Sl, Kl, Il, and Tl, i.e. the terms that can be converted
directly into the SKI combinators.
(* This is the core algorithm to translate ls terms (made up of lambda)
* into ls terms (made up of SKI combinators).
* The clauses described here follows the rules of the T function described at
* https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
* *)
let rec translate (e : ls) : ls = match e with
(* clause 1. *)
(* you can't do much with a variable *)
| Var x ->
Var x
(* clause 2. *)
(* an application remains an application, but with the terms translated *)
| App (e1, e2) ->
App (translate e1, translate e2)
(* clause 3. *)
(* when x is not free in e, there can be two cases:
* 1. x does not appear in e at all,
* 2. x appears bound in e, Abs (x, e') is in e
* In both cases, whatever you apply this lambda term to will not affect
* the result of application:
* 1. since x is not used, you can ignore it
* 2. the x is bound to an inner argument, so it's really a different x from this
* hence this is really a constant term e,
* which is the same as the K combinator with e as the first argument.
* (recall that: K x y = x) *)
| Abs (x, e) when not (free x e) ->
App (Kl, translate e)
(* clause 4. *)
| Abs (x, Var x') ->
(* this is the identity function, which is the I combinator *)
if x = x'
then Il
(* we will never hit this case because, when x != x',
* we end up in clause 3, as x is not free in Var x' *)
else failwith "error"
(* clause 5. *)
| Abs (x, Abs (y, e)) ->
(* when x is free in e, the x in e is the argument,
* we first translate the body into a combinator, to eliminate a layer of abstraction *)
if free x e
then translate (Abs (x, translate (Abs (y, e))))
else failwith "error"
(* clause 6. *)
| Abs (x, App (e1, e2)) ->
(* eliminate the abstraction via application *)
(* Recall that S x y z = x z (y z),
* so applying the term Abs (x, App (e1, e2)) to an argument x
* will result in substituting x into the body of e1, x z,
* and e2, y z, and applying e1 to e2, x z (y z) *)
if free x e1 || free x e2
then App (App (Sl, (translate (Abs (x, e1)))), translate (Abs (x, e2)))
else failwith "error"
| Kl -> Kl
| Sl -> Sl
| Il -> Il
| _ ->
failwith ("no matches for " ^ (string_of_ls e))Finally we can write the top level convert function we imagined earlier:
(* Converts a lambda term into an SKI term *)
let convert (e : lambda) : ski =
(* Convert lambda term into intermediate ls term *)
let rec ls_of_lambda (e : lambda) =
match e with
| Var x -> Var x
| App (e1, e2) -> App (ls_of_lambda e1, ls_of_lambda e2)
| Abs (x, e) -> Abs (x, ls_of_lambda e)
in
(* Convert intermediate ls term into ski term *)
let rec ski_of_ls (e : ls) : ski =
match e with
| Var _ -> failwith "should not have Var anymore"
| Abs _ -> failwith "should not have Abs anymore"
| App (e1, e2) -> T (ski_of_ls e1, ski_of_ls e2)
| Sl -> S
| Kl -> K
| Il -> I
| Tl (e1, e2) -> T (ski_of_ls e1, ski_of_ls e2)
in
(* convert lambda term into ls term *)
let ls_term = ls_of_lambda e in
(* translate ls term of lambda into ls term of combinators *)
let ls_comb = translate ls_term in
(* convert ls term into ski *)
ski_of_ls ls_combLet's try it with the example given by Wikipedia:
(* Example lambda terms *)
let l2 : lambda = Abs ("x", Abs ("y", App (Var "y", Var "x")))
let _ = print_endline (string_of_ski (convert l2))The output T(T(S,T(K,T(S,I))),T(T(S,T(K,K)),I)), is the same as (S (K (S I)) (S (K K) I)).
- Wikipedia SKI Combinator calculus
- Wikipedia Combinatory Logic
- Wikipedia Lambda Calculus
Footnotes
-
Wikipedia Combinatory Logic ↩