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.

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

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