Untyped lambda calculus interpreter in OCaml

A while back during the Christmas holidays I got interested in type theory and picked up Type Theory and Formal Proof: An Introduction by Rob Nederpelt and Herman Geuvers. Different kinds of lambda calculi play a big role in the book and to understand them better I decided to begin incrementally writing a lambda calculus interpreter as I progressed through the chapters describing the the topic. This post introduces the first version of the interpreter written based on the book's first chapter Untyped lambda calculus. This was also a great opportunity for me to learn a new language, OCaml, which is popular in the fields of computer science related to type theory and formal proof. Lexical analyzer was generated using ocamllex and Menhir was the parser generator of choice. This post does not go into details on using them, so feel free to check out the links provided for further reading. The implementation is quite straight forward, and it was easy to write while reading through the chapter. I also used it to do some of the exercises, which further helped the learning process. The mathematical theory presented in the following chapters is taken directly from the book.

Grammar

The grammar of the untyped lambda calculus can easily be derived from the following definition of the set $\Lambda$ of all of its expressions, also known as $\lambda$-terms. A $\lambda$-term is one of three types:

1. Variable – Let $V$ be an infinite set of variables. If $u\in V$, then $u\in\Lambda$.
2. Abstraction – If $M,N\in\Lambda$, then $(M N)\in\Lambda$.
3. Application – If $u\in V$ and $M\in\Lambda$, then $(\lambda u.M)\in\Lambda$.

From this definition we can form grammar

which looks a lot more like something we can implement for our interpreter. We begin the implementation by defining the grammar in ast.ml:

type term = Var of string | App of term * term | Abs of string * term
            

Notice that a term instance is essentially a node in an abstract syntac tree (AST) (thus the ast.ml). In order for the program to construct $\lambda$-terms from the user input we will need to add grammar definitions in parser.mly and lexer definitions in lexer.mll.

In parser.mly:

%{
    open Ast
%}

%token <string> VAR
%token DOT
%token LAMBDA
%token LPAREN
%token RPAREN
%token EOF

%start <Ast.term> prog

%%

prog:
    | t = term; EOF { t }
    ;

term:
    | x = VAR { Var (x) }
    | LPAREN; t1 = term; t2 = term; RPAREN { App (t1, t2) }
    | LPAREN; LAMBDA; x = VAR; DOT; t = term; RPAREN { Abs (x, t) }
    ;
            

In lexer.mll:

{
    open Parser
}

let white = [' ' '\t' '\n' ]+
let lod = ['a'-'z' 'A'-'Z' '0'-'9']
let var = lod+

rule read =
    parse
    | white     { read lexbuf }
    | "."       { DOT }
    | "lambda"  { LAMBDA }
    | "("       { LPAREN }
    | ")"       { RPAREN }
    | var       { VAR (Lexing.lexeme lexbuf) }
    | eof       { EOF }
            

Note that intead of λ we use lambda to make writing $\lambda$-terms easier on a computer. Finally, we add the following in out main.ml:

let parse (s : string) : term =
    let lexbuf = Lexing.from_string s in
    let ast = Parser.prog Lexer.read lexbuf in
    ast
            

Operations on $\lambda$-terms

Next we need to implement some useful operations to be performed on a $lambda$-term. One of them is $FV$, which determines the set of free variables of a $\lambda$-term. It has the following definition:

1. $FV(x)=\left\{x\right\}$, for each $x\in V$,
2. $FV((MN))=FV(M)\cup FV(N)$, for $N,M\in\Lambda$,
3. $FV((\lambda x.M))=FV(M)\setminus\left\{x\right\}$, for $x\in V, M\in\Lambda$.

Based on the definition we implement:

(* Free variables *)
let rec fv (ast : Ast.term) : string list =
    match ast with
    | Var v ->
        [v]
    | App (t1, t2) ->
        fv t1 @ fv t2
    | Abs (v, t) ->
        List.filter (fun e -> e <> v) (fv t)
            

Another operation that is $BV$, which determines the set of binding variables of a $\lambda$-term:

1. $BV(x)=\emptyset$, for each $x\in V$,
2. $BV((MN))=BV(M)\cup BV(N)$, for $N,M\in\Lambda$,
3. $BV((\lambda x.M))=\left\{x\right\}\cup BV(M)$, for $x\in V, M\in\Lambda$.

The implementation is straightforward:

(* Binding variables *)
let rec bv (ast : Ast.term) : string list =
    match ast with
    | Var _ ->
        []
    | App (t1, t2) ->
        bv t1 @ bv t2
    | Abs (v, t) ->
        let bvt = bv t in
        if not (List.mem v bvt) then [v] @ bvt else bvt
        

Now that we have $\mathrm{FV}$ and $\mathrm{BV}$ implemented, we can move on to $\alpha$-conversion which provides a set of rules for renaming bound variables (e.g. $x$ in $(\lambda x.M)$. It has the following definition

1. Let $M^{x\rightarrow y}$ represent the result of renaming every $x$ in $M$ to $y$. $\lambda x.M=_\alpha\lambda y.M^{x\rightarrow y}$, if $y\notin FV(M)$ and $y\notin BV(M)$,
2. If $M=_\alpha N$, then $ML=_\alpha NL$, $LM=_\alpha LN$, and $\lambda z.M=_\alpha\lambda z.N$ for arbitrary $z$,
3. $M=_\alpha M$,
4. If $M=_\alpha N$ then $N=_\alpha M$,
5. IF $L=_\alpha M$ and $L=_\alpha N$, then $L=_\alpha N$.

The implementation takes form

(* Alpha conversion *)
let alpha_conv (ast : Ast.term) (x : string) (y : string) : Ast.term =
    let rec conv (t : Ast.term) (x : string) (y : string) : Ast.term =
        match t with
        | Var v as term ->
            if v = x then Var y else term
        | App (t1, t2) ->
            App (conv t1 x y, conv t2 x y)
        | Abs (v, t) ->
            if v = x then Abs (y, conv t x y) else Abs (v, conv t x y)
    in
    match ast with
    | Var _ as term ->
        term
    | App _ as term ->
        term
    | Abs (v, t) as term ->
        let bvt = bv t in
        let fvt = fv t in
        if (not (List.mem y bvt)) && (not (List.mem y fvt)) && v = x then
          Abs (y, conv t x y)
        else term
        

The $\alpha$-conversion implementation allows us to introduce substitution, which is defined as:

1. $x\left[x:=N\right]=N$,
2. $y\left[x:=N\right]=y$ if $x\not\equiv y$,
3. $(PQ)\left[x:=N\right]\equiv(P\left[x:=N\right])(Q\left[x:=N\right]))$,
4. $(\lambda y.P)\left[x:=N\right]\equiv\lambda z.(P^{y\rightarrow z}\left[x:=N\right])$, if $\lambda z.P^{y\rightarrow z}$ is a $\alpha$-variant of $\lambda y.P$ such that $z\notin FV(N)$.

We end up with implementation

(* Substitution *)
let rec sub (ast : Ast.term) (x : string) (st : Ast.term) : Ast.term =
    match ast with
    | Var v as term ->
        if v = x then st else term
    | App (t1, t2) ->
        App (sub t1 x st, sub t2 x st)
    | Abs (v, t) as term ->
        if v = x then term
        else if List.mem v (fv st) then
          let av = "_" ^ v in
          let at = alpha_conv term v av in
          sub at x st
        else Abs (v, sub t x st)
        

Last operation to be implemented is the $\beta$-reduction, which is at the core of our interpreter. The main function of the interpreter is to evaluate the $\lambda$-term given by the user and reduce it to its normal form, which in simple terms is form that can not be further reduced. A single $\beta$-reduction step is defined as:

1. $(\lambda x.M)N\rightarrow_\beta M\left[x:=N\right]$,
2. If $M\rightarrow_\beta N$, then $ML\rightarrow_\beta NL$, $LM\rightarrow_\beta LN$, and $\lambda x.M\rightarrow_\beta\lambda x.N$.

(* One-step Beta reduction *)
let rec reduce (ast : Ast.term) : Ast.term =
    match ast with
    | Var _ as term ->
        term
    | App (t1, t2) as term ->
        let t =
            match t1 with
            | Abs (v, t) ->
                sub t v t2
            | _ ->
                let r = App (reduce t1, t2) in
                if r = term then App (t1, reduce t2) else r
        in
        t
    | Abs (v, t) ->
        Abs (v, reduce t)
        

For an application that is not equal to the $\lambda$-term in part 1. of the single $\beta$-reduction step definition, the implementation first tries to reduce the left $\lambda$-term. If it did not reduce, the implementation then reduces the right $\lambda$-term. We can now perform $\beta$-reduction by calling reduce until the $\lambda$-term returned by it is equivalent to the one we passed as parameter. In main.ml:

let print (ast : Ast.term) =
    let rec print_term t =
        match t with
        | Var v ->
            print_string v
        | App (t1, t2) ->
            print_string "(" ;
            print_term t1 ;
            print_string " " ;
            print_term t2 ;
            print_string ")"
        | Abs (v, t) ->
            print_string ("λ " ^ v ^ ".") ;
            print_term t
    in
    print_term ast ; print_string "\n"

let () =
    let rec beta t =
        let r = reduce t in
        if r = t then r else beta r
    in
    let filename = Sys.argv.(1) in
    let ic = open_in filename in
    let s = In_channel.input_all ic in
    let ast = parse s in
    let reduced = beta ast in
    print_string "Original expression:\n" ;
    print ast ;
    print_string "Beta reduced expression:\n" ;
    print reduced
        

We now have a untyped lambda calculus interpreter capable of $\beta$-reducing $\lambda$-terms to their normal form.

Example: Church numerals

Let us define the first three Church numerals as well as addition and multiplication of Church numerals

Passing $\lambda$-term $((add~one) one)$

(((lambda m . (lambda n . (lambda f . (lambda x . ((m f) ((n f) x))))))
  (lambda f . (lambda x . (f x))))
 (lambda f . (lambda x . (f x))))
        

Original expression:
((λ m.λ n.λ f.λ x.((m f) ((n f) x)) λ f.λ x.(f x)) λ f.λ x.(f x))
Beta reduced expression:
λ f.λ x.(f (f x))
        

which equals to $two$. Another $\lambda$-term $((mul~one) zero)$

(((lambda m . (lambda n . (lambda f . (lambda x . ((m (n f)) x)))))
 (lambda f . (lambda x . (f x)))) (lambda f . (lambda x . x)))
        

reduces to

Original expression:
((λ m.λ n.λ f.λ x.((m (n f)) x) λ f.λ x.(f x)) λ f.λ x.x)
Beta reduced expression:
λ f.λ x.x
        

which corresponds to $zero$.