# 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^{1},
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 =
of name
| Var of lambda * lambda
| App of name * lambda | Abs
```

Here’s an example lambda term, representing the application of an identity function to an identity function:

`'x', Var 'x'), Abs ('y', Var 'y')) App (Abs (`

## 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:

`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 =
of name
| Var of ls * ls
| App of name * ls
| Abs
| Sl
| Kl
| Ilof ls * ls
| Tl
(* String representation of ls *)
let rec string_of_ls (l : ls) : string = match l with
| Var x -> x"(" ^ (string_of_ls e1) ^ (string_of_ls e2) ^ ")"
| App (e1, e2) -> "\\" ^ x ^ (string_of_ls e)
| Abs (x, e) -> "S"
| Sl -> "K"
| Kl -> "I"
| Il -> "(T " ^ (string_of_ls e1) ^ (string_of_ls e2) ^ ")" | Tl (e1, 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 e2List.filter (fun v -> v != x) (fv e)
| Abs (x, 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) *)
when not (free x e) ->
| Abs (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
failwith "should not have Var anymore"
| Var _ -> failwith "should not have Abs anymore"
| Abs _ ->
| 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