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\).
We define a type for variables
type var = stringDefine 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}".
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))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.
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")))Define a function red of type
t -> t option
which performs a β-reduction step (it should return None if there is
no 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 stepsDefine a function eq of type
t -> t -> bool
which compares the normal forms of two terms (note: the equality
function = of OCaml works as expected on recursive types).
Test it with:
let () =
let id = Abs ("x", Var "x") in
let id2 = App (id, id) in
assert (eq (App (id2, id2)) id2)Define a function alpha of type
t -> t -> bool
which determines whether two λ-terms are α-equivalent. When comparing
two abstractions, you can rename the variable to a common fresh
variable! 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")))NB : the above implementation is inefficient, because we are
constantly renaming variables. Another approach can be based on the use
of 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. In this way we can maintain the information of which
pairs of variables from the left and the right should be considered as
the same without actually performing a renaming.
This should be enough in practice for most tests because equality is included in β-equivalence.
Define the identity λ-term id (of type t).
Define the booleans btrue and bfalse λ-terms, which are functions
taking two arguments and returning the first (resp. the second).
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))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)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.
Define the successor λ-term succ:
let () =
assert (eq (apps [succ; nat 5]) (nat 6))Define the addition λ-term add:
let () =
assert (eq (apps [add; nat 6; nat 5]) (nat 11))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\)?
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)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)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 Stdlib.fst
(of type 'a * 'b -> 'a) to retrieve the first component
of a pair. Test it with
let () = assert (fib 10 = 55)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))Define the subtraction λ-term sub and test it
with
let () =
assert (eq (apps [sub; nat 14; nat 5]) (nat 9))Define a function fact_fun of
type
(int -> int) -> int -> intwhich 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) ndeduce an implementation fact
of the factorial and test it with
let () = assert (fact 5 = 120)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.
Define, using the same strategy as above, the factorial
λ-term factorial. Test it with
let () = assert (eq (App (factorial, nat 5)) (nat 120))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)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
\[ λx.xyz \]
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 dbDefine 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')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')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)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.
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)