Home

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 language1, 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:

  1. Variable, such as x,
  2. Lambda abstraction, such as fun x -> x,
  3. 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:

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

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 =
  | 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

  1. Wikipedia SKI Combinator calculus
  2. Wikipedia Combinatory Logic
  3. Wikipedia Lambda Calculus