SKI combinators - Lambda to SKI
2017-05-27 18:25
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
Lambda Calculus
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 * lambda
Here’s an example lambda term, representing the application of an identity function to an identity function:
Translating lambda to SKI
Let us conjure an ideal function that will do such a translation, it should take a lambda term to an SKI term:
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_comb
Let’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))
.
References
- Wikipedia SKI Combinator calculus
- Wikipedia Combinatory Logic
- Wikipedia Lambda Calculus