The λ-calculus

Samuel Mimram

1 Implementing the λ-calculus

We recall that λ-terms are generated by the grammar

\[ t,u \qquad::=\qquad x \quad|\quad t u \quad|\quad λx.t \]

and the β-reduction rule is

\[ (λx.t) u \quad\longrightarrow\quad t[u/x] \]

where \(t[u/x]\) is the capture-avoiding substitution of \(x\) by \(u\) in \(t\).

1.1 λ-terms

We define a type for variables

type var = string

Define a type t for λ-terms (its constructors should be named Var, App and Abs).

Define a function to_string of type t -> string providing a string representation of a λ-term (we recall that the concatenation of two strings s and t is s ^ t). For instance,

let () =
  print_endline (to_string (Abs ("x", App (Var "y", Var "x"))));
  print_endline (to_string (App (Abs ("x", Var "y"), Var "x")))

should print something like

(λx.(y x))
((λx.y) x)

Note that we need to have parenthesis, otherwise both terms would be printed as λx.y x. In case you cannot copy and paste the character λ, you can also type it in a string as "\u{03bb}".

1.2 Free variables

Define a function has_fv of type var -> t -> bool which indicates whether a variable is free in a term.

You can test it with

let () =
  let t = App (Var "x", Abs ("y", App (Var "y", Var "z"))) in
  assert (has_fv "x" t);
  assert (not (has_fv "y" t));
  assert (has_fv "z" t);
  assert (not (has_fv "w" t))

1.3 Fresh variables

Define a function fresh of type unit -> var which returns a fresh variable. For instance, successive calls to the function might return "x0", "x1", "x2" and so on.

We recall that you can create a reference with something like let n = ref 2, get the value of the reference with !n and modify the reference with n := 5. You can convert an integer to a string using string_of_int.

1.4 Substitution

Define a function sub of type var -> t -> t -> t such that sub x u t returns the capture-avoiding substitution of x by u in t.

Some basic tests should include:

let () =
  let t = App (Var "x", Abs ("y", Var "x")) in
  let i = Abs ("x", Var "x") in
  let ti = App (Abs ("x", Var "x"), Abs ("y", Abs ("x", Var "x"))) in
  assert (sub "x" i t = ti);
  assert (not (sub "x" (Var "y") (Abs ("y", Var "x")) = Abs("y", Var "y")))

1.5 β-reduction

Define a function red of type t -> t option which performs a β-reduction step.

Define a function normalize of type t -> t which computes the normal form of a λ-term (this function might loop forever if the term has no normal form).

Define a function reduction of type t -> t which prints the reduction steps from a given term (and, if you have time for it, the total number of those to reach a normal form). We recall that a string can be displayed with the print_endline function. For instance,

let _ =
  let id = Abs ("x", Var "x") in
  let id2 = App (id, id) in
  reduction (App (id2, id2))

will output something like

   (((λx.x) (λx.x)) ((λx.x) (λx.x)))
-> ((λx.x) ((λx.x) (λx.x)))
-> ((λx.x) (λx.x))
-> (λx.x)
3 reduction steps

1.6 Equivalence

Define a function eq of type t -> t -> bool which compares the normal forms of two terms. Test it with:

let () =
  let id = Abs ("x", Var "x") in
  let id2 = App (id, id) in
  assert (eq (App (id2, id2)) id2)

1.7 Proper β-equivalence of λ-terms

Define a function alpha of type t -> t -> bool which determines whether two λ-terms are α-equivalent. It can be useful to use the List.assoc function of type ('a * 'b) list -> 'a -> 'b which, given a list l and a value x, finds the first value y such that the pair (x,y) belongs to l. Test your function with

let () =
  assert (alpha (Abs ("x", Var "x")) (Abs ("y", Var "y")));
  assert (not (alpha (Abs ("x", Var "x")) (Abs ("x", Var "y"))))

Modify the function eq of type t -> t -> bool so that determines whether two λ-terms, which are supposed to be normalizing, are equivalent up to α- and β-equivalence. Test it with

let () =
  let t = App (Abs ("x", Abs ("y", Var "x")), Var "y") in
  print_endline (to_string (normalize t));
  assert (eq t (Abs ("z", Var "y")))

2 Computing in the λ-calculus

This should be enough in practice for most tests because equality is included in β-equivalence.

2.1 Identity

Define the identity λ-term id (of type t).

2.2 Booleans

Define the booleans btrue and bfalse λ-terms, which are functions taking two arguments and returning the first (resp. the second).

2.3 Helper functions

Define a function abss of type var list -> t -> t which performs an abstraction over a list of variables: it corresponds to the usual notation in λ-calculus

\[ λxyz.t\quad=\quad λx.λy.λz.t \]

and should pass the following test:

let () =
  let t = Var "t" in
  assert (abss ["x"; "y"; "z"] t = Abs ("x", Abs ("y", Abs ("z", t))))

Define a function apps of type t list -> t which computes the application of a list of terms (supposed to be non-empty), bracketed on the left. We recall that you can reverse a list with List.rev (or you can use an auxiliary function with an extra argument). Your function should pass the following test:

let () =
  let t = Var "t" in
  let u = Var "u" in
  let v = Var "v" in
  let w = Var "w" in
  assert (apps [t; u; v; w] = App (App (App (t, u), v), w))

2.4 Conditional

Define the conditional bif. It should pass the following test:

let () =
  let t = Var "t" in
  let u = Var "u" in
  assert (eq (apps [bif; btrue; t; u]) t);
  assert (eq (apps [bif; bfalse; t; u]) u)

2.5 Natural numbers

Define the natural number function nat of type int -> t. The encoding \(\underline{n}\) of a natural number \(n\) should follow the pattern:

\[ \begin{align*} \underline{0}&=λf.λx.x & \underline{1}&=λf.λx.fx & \underline{2}&=λf.λx.f(fx) \\ \underline{3}&=λf.λx.f(f(fx)) & \underline{4}&=λf.λx.f(f(f(fx))) & \underline{5}&=λf.λx.f(f(f(f(fx)))) \end{align*} \]

and so on. These are called Church natural numbers.

2.6 Successor

Define the successor λ-term succ:

let () =
  assert (eq (apps [succ; nat 5]) (nat 6))

2.7 Addition

Define the addition λ-term add:

let () =
  assert (eq (apps [add; nat 6; nat 5]) (nat 11))

2.8 Multiplication

Define the multiplication λ-term mul:

let () =
  assert (eq (apps [mul; nat 3; nat 4]) (nat 12))

Show the corresponding reduction

let () = reduction (apps [mul; nat 3; nat 4]);

and observe the number of reduction steps of the multiplication of \(m\) and \(n\) for various values of \(m\) and \(n\). What is the exact number of steps in terms of \(m\) and \(n\)?

2.9 Is zero

Define the comparison to zero λ-term iszero and test it with

let () =
  assert (eq (apps [iszero; nat 5]) bfalse);
  assert (eq (apps [iszero; nat 0]) btrue)

2.10 Pairs

Define the pairing λ-term pair and the two projections fst and snd λ-terms:

let () =
  let t = Var "t" in
  let u = Var "u" in
  assert (eq (apps [fst; apps [pair; t; u]]) t);
  assert (eq (apps [snd; apps [pair; t; u]]) u)

2.11 Predecessor: Fibonacci as a warmup

As a warmup to computing predecessors, recall that the Fibonacci sequence \((f_n)\) is defined by \(f_0=0\), \(f_1=1\), and \(f_{n}=f_{n-1}+f_{n-2}\) for \(n\geq 2\).

Provide a naive implementation fib_naive of type int -> int of the sequence. What is its complexity? Test it with

let () = assert (fib_naive 10 = 55)

We now want to implement this function with a linear complexity. First, implement a function fib_fun of type int * int -> int * int such that fib_fun \((f_n,f_{n+1})=(f_{n+1},f_{n+2})\).

Deduce from the previous function, an linear-time implementation fib (of type int -> int) of the Fibonacci sequence. You can use Pervasives.fst (of type 'a * 'b -> 'a) to retrieve the first component of a pair. Test it with

let () = assert (fib 10 = 55)

2.12 Predecessor

Define the λ-term pred_fun which given a pair \((m,n)\), encoded as a λ-term, produces the pair \((n,n+1)\). Test it with

let () =
  assert (eq (apps [pred_fun; apps [pair; nat 1; nat 5]]) (apps [pair; nat 5; nat 6]))

What is the value of

pred_fun (p,q)
pred_fun (pred_fun (p,q))
pred_fun (pred_fun (pred_fun (p,q)))

and more generally of pred_fun applied \(n\) times to (p,q)?

Define the predecessor λ-term pred and test it with

let () =
  assert (eq (apps [pred; nat 11]) (nat 10));
  assert (eq (apps [pred; nat 0]) (nat 0))

2.13 Subtraction

Define the subtraction λ-term sub and test it with

let () =
  assert (eq (apps [sub; nat 14; nat 5]) (nat 9))

2.14 Warmup on the factorial

Define a function fact_fun of type

(int -> int) -> int -> int

which takes as arguments a function f and a number n, and computes the factorial function, supposing that f is the factorial function but works only on values strictly smaller than n. Your function should not be recursive.

Using the fixpoint function

let rec fix f n = f (fix f) n

deduce an implementation fact of the factorial and test it with

let () = assert (fact 5 = 120)

2.15 Fixpoint

Define the fixpoint λ-term fixpoint, which corresponds to

\[ Y \quad=\quad λf.(λx.f(xx))(λx.f(xx)) \]

and satisfies

\[ Yt\quad\overset*\longrightarrow\quad t(Yt) \]

for every term \(t\). Test its implementation with

let () =
  let t = Var "t" in
  reduction (apps [fixpoint; t])

Note you can use the shortcut C-c C-c to interrupt a computation in the evaluation buffer.

2.16 Factorial

Define, using the same strategy as above, the factorial λ-term factorial. Test it with

let () = assert (eq (App (factorial, nat 5)) (nat 120))

2.17 Optional: η-equivalence

Implement a function etaeq which test equivalence of λ-terms up to α-, β- and η-equivalences. For instance, it should pass the following test:

let () =
  let t = (Abs ("x", App (Abs ("y", Abs ("z", App (Var "y", Var "z"))), Var "x"))) in
  let u = Abs ("t", Var "t") in
  assert (etaeq t u)

3 Optional: De Bruijn indices

Although it looks like a minor problem, handling λ-terms up to α-conversion is a major source of inefficiencies and correctness issues. In order to avoid it, we now consider an alternative representation of λ-terms, with so called de Bruijn indices. Here, abstractions do not carry a variable name, and a variable is a natural number \(n\) indicating that it refers to the \(n\)-th λ-abstraction when going up in the syntactic tree. For instance, the λ-term in traditional notation

\[ λx.λy.x(λz.x)(λx.xy) \]

will be written, in de Bruijn notation,

\[ λ.λ.1(λ.2)(λ.01) \]

A variable which does not refer to a λ-abstraction is considered as free. For instance, in the term

\[ λ.012 \]

there are two free variables (those of indices 1 and 2): the term namely corresponds to

\[ λ \]

We define a type for λ-terms with de Bruijn indices by

type dvar = int

type db =
  | DVar of dvar
  | DApp of db * db
  | DAbs of db

3.1 Conversion

Define a function db_of_term of type t -> db which converts a closed λ-term into one with de Bruijn indices. Test it on the above term:

  let () =
    let t = Abs ("x", Abs ("y", App (App (Var "x", Abs ("z", Var "x")), Abs ("x", App (Var "x", Var "y"))))) in
    let t' = DAbs (DAbs (DApp (DApp (DVar 1, DAbs (DVar 2)), DAbs (DApp (DVar 0, DVar 1))))) in
    assert (of_term t = t')

3.2 Lifting

Define a function lift of type int -> db -> db which increases by 1 all free variables of a term of index greater or equal than the first argument. In particular, lift 0 should increase by 1 all free variables:

let () =
  let t = lift 0 (DAbs (DApp (DVar 0, DVar 1))) in
  let t' = DAbs (DApp (DVar 0, DVar 2)) in
  assert (t = t')

3.3 Unlifting

Define a function unlift of type int -> dvar -> dvar which decreases by 1 all variables of index greater than the first argument. The function will never be called with two equal arguments. For instance,

  let () =
    assert (unlift 5 1 = 1);
    assert (unlift 5 4 = 4);
    assert (unlift 5 6 = 5);
    assert (unlift 5 9 = 8)

3.4 Substitution

Using the two above functions, define a function sub of type int -> db -> db -> db which replaces a variable x by a term u in a term t. Think hard about the way variables should be handled in the cases of variable and abstraction.

3.5 Reduction

Use it to implement reduction and a normalization function dnormalize of type db -> db. Perform the above tests on it, for instance

let () =
  let t = of_term (apps [factorial; nat 4]) in
  let u = of_term (nat 24) in
  assert (dnormalize t = dnormalize u)