HW 4  COSC 4780

HW 4 
COSC 4780
Discussion:
We say two lambda terms are α-equivalent (read “alpha equivalent”)
if they have the same shape modulo the names of bound variables. For
example:
λx.x =α λy.y
λx.λy.xy =α λy.λx.yx
λx.λy.x(λx.x) =α λy.λx.y(λz.z)
The following definition specifies when a pair of terms are α-equivalent:
x =α y
def =

true if x and y are identically the same variable.
f alse otherwise
MN =α M0N0 def = M =α M0 ∧ N =α N0
(λx.M) =α (λy.N)
def = M[x := z] =α N[y := z]
where z is fresh with respect to fv(M) and fv(N).
M =α N
def = f alse otherwise
The first line says that variables are α-equivalent iff they are the same
variable. The second line says simply that an application M N is α-equivalent
iff their respective parts are. The third line says that abstractions are αequivalent if the the substitution instances of their bodies are, after the free
occurrences of the bound variable have been renamed by a fresh variable. A
variable is fresh if it is not x, is not y, and is not free in either M or N. The
renaming is performed using capture-avoiding substitution. The final condition covers all the cases where M and N are lambda terms having different
constructors. For example, no variable is α-equivalent to an abstraction or
application.
1
In OCaml, the following codes checks whether two terms are α-equivalent.
type lambda = Var of string | Ap of lambda * lambda | Abs of string * lambda ;;
let rec fv m =
match m with
Var x -> [x]
| Ap (m,n) -> fv m @ fv n
| Abs (x,m) -> List.filter (fun y -> y <> x) (fv m)
(* alphaeq : term -> term -> bool *)
let rec alphaeq m n =
match (m,n) with
(Var x, Var y) -> x = y
| (Ap(m,n),Ap(m’,n’)) -> m = m’ && n = n’
| (Abs(x,m),Abs(y,n)) ->
let z = fresh ‘‘z’’ ([x;y] @ (fv m) @ (fv n)) in
alphaeq (subst (x,Var z) m) (subst (y,Var z) n)
| -> false ;;
0.1 DeBruijn Indicies
An alternative to checking alpha-equivalence as above is to eliminate bound
variables using DeBruijn indices1
In this representation, α-equivalent terms
are syntactically identical.
Example 0.1. Here’s a list of lambda terms and their corresponding representations using DeBruijn indices. Note that α-equivalent terms have
identical representations ad DeBruijn terms.
lambda term DeBruijn term
λx.x λ1
λy.y λ1
λx.λy.y x λλ1 2
λx.λz.z x λλ1 2
λx.λy.w x y λλw 2 1
λx.λy.w x x λλw 2 2
λz.λy.w z z λλw 2 2
λx.(λx.x)(λy, x y) (λ((λ1)(λ(21))))
1
In the Wikipedia article [https://en.wikipedia.org/wiki/De Bruijn index] they start
at 1.
2
To code up an algorithm that translates lambda terms into DeBruijn
terms, we’ll need to represent DeBruijn terms as an OCaml type. Here’s
one way
type deBruijn = DBIndex of int
| DBVar of string
| DBAp of debruijn * debruijn
| DBAbs of debruijn
;;
We have two kinds of variables now - in a lambda term, free variables of the
form (Var ‘‘x’’) are represented as deBruijn terms as (dbVar‘‘x’’).
Within a lambda term, a bound variable of the form Var ‘‘x’’ will become
a deBruijn term of the form DBIndex k where k is the number of lambdas
up the syntax tree that binds that variable. Note that a lambda term of
the form Abs ‘‘x’’ M will be translated into a deBruijn term of the form
DBAbs Mˆ where Mˆ is the translation of the lambda term M into a deBruijn
term.
Mathematically, we can write the transformation as follows. We use a
function f to map variables to their indices. Recall the point-wise update
of a function.
update f (x, v) = fun y -> if x = y then v else f y;;
The idea is to update the function f on input x to have value v.
Example 0.2. If f x = x + 1 and f’ = update f (2,2) then f 2 = 3
and f’ 2 = 2. In every other case, f’ behaves like f. We have updated the
function f at the input (point) 2.
We’ll use a function to keep track of DeBruijn indices. When a bound
variable is encountered it will be mapped to a deBruijn (term) with the
We use a similar idea for keeping track of, and updating DeBruijn indices.
The update function will map functions from strings to deBruijn (terms) to
new functions of the same type. If the string is we need to add a new index
and update the indexes of all the others to add one. The value returned
by the updated function is determined by the values of the function being
updated!
dbUpdate :: (string → deBruijn) → string → (string → deBruijn)
let dbUpdate f x =
3
fun y -> if x = y then
dBIndex 1
else
match (f y) with
(dBIndex k) -> (dBIndex (k+1)
| -> dBVar y
;;
The dbUpdate function really will turn out to do all the work of keeping
track of the indices.
Here’s a definition of the transformation (7→f ), that transforms lambda
terms into deBruijn terms. Note that f is a parameter to the transformation
and intially fx = DBVar x - i.e. it maps all strings to a DBVar.
V ar x 7→f f x
Ap(m, n) 7→f dbAp (m0
, n0
) where m 7→f m0 ∧ n 7→f n
0
Abs(x, m) 7→f dBAbs m0 where m 7→f
0 m0 and f
0 = dbUpdate fx
The transformation uses the function f to figure out how variables get
mapped – to DeBruijn indices or just to variables. Initially f is the function
that maps a string x to the DeBruijn DBVar x. When it encounters an
abstraction of the form λx.m (ABs(x,m)), it has to update f so that the
free occurrences of x in M get mapped to the DeBruijn index DBIndex 1.
If another abstraction is encountered, f will be updated again to map x to
index 1, and all the other indices will be incremented to indicate another
depth of abstraction has been encountered. This worked, even if f is updated
for x a second (or third, or fourth) time.
Problem 0.1. Implement a function debruijnize which maps lambda terms
to their equivalent DeBruijn representation.
Problem 0.2. Write a program that uses the DeBruijn representation to
check for α-equivalence and provide some test cases to convince the grader
your code works.
4