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 = 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}"`

.

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 steps
```

Define 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 -> 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)`

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 =
of dvar
| DVar of db * db
| DApp of db | DAbs
```

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')
```

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)
```