Foundations1 assignment 2023
Submit by Monday of week 8 (30 October 2023)
by the deadline hour relevant to your campus.
Worth 15%
Submit only typed material
No handwritten material
NO EMAIL SUBMISSIONS
EACH CAMPUS WILL INFORM YOU WHERE
& HOW TO SUBMIT
WRITE YOUR FAMILYNAME+NAME+STUDENT ID (in this order) HERE
1
Background
• The syntax of the classical λ-calculus is given by M ::= V | (λV.M) | (MM).
We assume the usual notational conventions in M and use the reduction rule:
(λv.P)Q →β P[v := Q].
• The syntax of the λ-calculus in item notation is given by M0
::= V |[V]M0
| hM0
iM0
.
We use the reduction rule: hQ0
i[v]P
0 →β0 [v := Q0
]P
0
where [v := Q0
]P
0
is defined in a similar way to P[v := Q].
• In M, (P Q) stands for the application of function P to argument Q.
In M0
, hQ0
iP
0
stands for the application of function P
0
to argument Q0
(note the
reverse order).
For example:
(λx.x)y in M becomes hyi[x]x in M0
.
(λx.(λy.xy)z)(λz0
.z0
) in M becomes h[z
0
]z
0
i[x]hzi[y]hyix in M0
.
• The syntax of the classical λ-calculus with de Bruijn indices is given by
Λ ::= N | (λΛ) | (ΛΛ).
For example: (λ1) is a term (it is equivalent to λx.x and λy.y, etc).
Also (λ(λ1 2)) is also a term. It stands as you will see for λxy.yx.
Also, (λ(λ2 1)) is also a term. It stands as you will see for λxy.xy.
We will use similar parenthesis convention for Λ as in M, so ABC stands for ((AB)C),
but we cannot combine many λs into one. So, λλA cannot be written as λA, but we
know that λv.λv0
.A can be written as λvv0
.A.
• For [x1, · · · , xn] a list (not a set) of variables, we define ω[x1,··· ,xn]
: M 7→ Λ by:
1. ω[x1,··· ,xn]
(vi) = min{j : vi ≡ xj}
2. ω[x1,··· ,xn]
(AB) = ω[x1,··· ,xn]
(A)ω[x1,··· ,xn]
(B)
3. ω[x1,··· ,xn]
(λx.A) = λω[x,x1,··· ,xn]
(A)
Hence
– ω[x,y,x,y,z]
(x) = 1
– ω[x,y,x,y,z]
(y) = 2
– ω[x,y,x,y,z]
(z) = 5.
– Also ω[x,y,x,y,z]
(xyz) = 1 2 5.
– Also ω[x,y,x,y,z]
(λxy.xz) = λλ2 7.
• Translation from M to Λ: If our variables are ordered as v1, v2, v3, · · · , then we
define ω : M 7→ Λ by
0. ω(A) = ω[v1,··· ,vn]
(A) where F V (A) ⊆ {v1, · · · , vn}.
2
So for example, if our variables are ordered as
x, y, z, x0
, y0
, z0
, · · ·
then the translation of ω(λxyx0
.xzx0
) from M to Λ gives the term λλλ3 6 1. This
can be seen as follows:
ω(λxyx0
.xzx0
) =0
ω[x,y,z]
(λxyx0
.xzx0
) =3
λω[x,x,y,z]
(λyx0
.xzx0
) =3
λλω[y,x,x,y,z]
(λx0
.xzx0
) =3
λλλω[x0
,y,x,x,y,z]
(xzx0
) =2
λλλω[x0
,y,x,x,y,z]
(xz)ω[x0
,y,x,x,y,z]
(x
0
) =2
λλλω[x0
,y,x,x,y,z]
(x)ω[x0
,y,x,x,y,z]
(z)ω[x0
,y,x,x,y,z]
(x
0
) =1
λλλ3 ω[x0
,y,x,x,y,z]
(z)ω[x0
,y,x,x,y,z]
(x
0
) =1
λλλ3 6 ω[x0
,y,x,x,y,z]
(x
0
) =1
λλλ3 6 1.
• – We define v :: L as the consing of v to L as for example in v :: [2, 3, y] = [v, 2, 3, y].
– Assume an ordered list of variables
listorder = [x, y, z, x0
, y0
, z0
, x1, y1, z1, x2, y2, z2, . . . ].
– Let L = [a1, a2, · · · , an, · · · ] be a list whose number of elements is denoted as
|L|.
For example, |listorder| = ∞, |[x, y, z]| = 3, |[2, 3, 4, 5]| = 4, |[ ]| = 0.
Assume j ≤ |L|. We define:
∗ lel(j, L) = [a1, a2, · · · , aj ].
∗ el(j, L) = aj .
– Let S be a set of positive natural numbers. We define max(S) to be the largest
number ai
in S. I.e., max(S) = aj such that for every ai ∈ S we have ai ≤ aj .
– We define lams(n) = 0
lams(AB) = lams(A) + lams(B)
lams(λA) = 1 + lams(A).
– We define ω1 : Λ 7→ M as follows:
0. ω1(A) = ω
0
1
(n + 1, lel(n, listorder), A)
where n = max(F V (A)).
1. ω0
1
(n, l, m) = el(m, l)
2. ω0
1
(n, l, λA) = λv.ω0
1
(n + 1, v :: l, A) where v = el(n, listorder).
3. ω0
1
(n, l, AB) = ω
0
1
(n, l, A)ω
0
1
(n + lams(A), l, B)
3
For example, F V (λ1 2) = {1} and max(F V (λ1 2)) = 1. Hence
ω1(λ1 2) =0
ω
0
1
(2, lel(1, listorder), λ1 2) =
ω
0
1
(2, [x], λ1 2) =2
λy.ω0
1
(3, [y, x], 1 2) =3
λy.ω0
1
(3, [y, x], 1)ω
0
1
(3 + lams(1), [y, x], 2) =
λy.ω0
1
(3, [y, x], 1)ω
0
1
(3, [y, x], 2) =1
λy.el(1, [y, x])ω
0
1
(3, [y, x], 2) =1
λy.el(1, [y, x])el(2, [y, x]) =
λy.yel(2, [y, x]) =
λy.yx.
• Assume the following SML datatypes which implement M, Λ and M0
respectively
(here, if e1 implements A0
1
and e2 implements A0
2
, then IAPP(e1,e2) implements
hA0
1
iA0
2 which stands for the function A0
2
applied to argumentA0
1
):
datatype LEXP =
APP of LEXP * LEXP | LAM of string * LEXP | ID of string;
datatype BEXP =
BAPP of BEXP * BEXP | BLAM of BEXP | BID of int;
datatype IEXP =
IAPP of IEXP * IEXP | ILAM of string * IEXP | IID of string;
Recall the printing function on LEXP:
(*Prints a term in classical lambda calculus*)
fun printLEXP (ID v) =
print v
| printLEXP (LAM (v,e)) =
(print "(\\";
print v;
print ".";
printLEXP e;
print ")")
| printLEXP (APP(e1,e2)) =
(print "(";
printLEXP e1;
print " ";
4
printLEXP e2;
print ")");
• For each of BEXP and IEXP we can also write a printing function printBEXP (respectively printIEXP) that prints its elements nicely just like we wrote printLEXP
which prints nicely the elements of LEXP.
(*Prints a term in item lambda calculus*)
fun printIEXP (IID v) =
print v
| printIEXP (ILAM (v,e)) =
(print "[";
print v;
print "]";
printIEXP e
)
| printIEXP (IAPP(e1,e2)) =
(print "<";
printIEXP e1;
print ">";
printIEXP e2
);
(*Prints a term in classical lambda calculus with de Bruijn indices*)
fun printBEXP (BID n) =
print (Int.toString n)
| printBEXP (BLAM (e)) =
(print "(\\";
printBEXP e;
print ")")
| printBEXP (BAPP(e1,e2)) =
(print "(";
printBEXP e1;
print " ";
printBEXP e2;
print ")");
• At http://www.macs.hw.ac.uk/~fairouz/foundations-2023/slides/assign23-help.
sml, you find an implementation in SML of the set of terms M, M0
, and Λ including
printing their terms printLEXP, printIEXP and printBEXP, and many operations on
M like substitution and free variables etc. You can use all of these in your assignment.
Anything you use from here or elsewhere has to be well cited/referenced.
5
Questions
1. For each term A of the terms below, give its translation ω(A) from M to Λ showing
all the steps, their number and underlining all the parts you are working on, just like
we did in the above example:
(a) (λxy.x). (1)
ω(λxy.x) =0
.
.
.
(b) (λxyz.xz(yz)). (1)
ω(λxyz.xz(yz)) =0
.
.
.
(c) xz(λxy.z(λz.zy)x). (1.5)
ω(xz(λxy.z(λz.zy)x)) =0
.
.
.
2. Assume the following translation function f from M to M0
that will translate terms
in M to terms in M0
:
0. f(v) = v
1. f(λv.A) = [v]f(A)
2. f(AB) = hf(B)if(A)
So for example:
f((λx.x)y) =2
hf(y)if(λx.x) =0
hyif(λx.x) =1
hyi[x]f(x) =0
hyi[x]x.
Similarly you can show that: f((λx.(λy.xy)z)(λz0
.z0
)) = h[z
0
]z
0
i[x]hzi[y]hyix.
Use this translation function f to translate all the terms in Question 1 above into
terms of M0
. That is, give f(λxy.x) and f(λxyz.xz(yz)) and f(xz(λxy.z(λz.zy)x))
showing all the steps and underlining all the parts you are working on. (3.5)
• f(λxy.x) =1
.
.
.
6
• f(λxyz.xz(yz)) =1
.
.
.
• f(xz(λxy.z(λz.zy)x)) =2
.
.
.
3. Calculate ω1(λ1(λ21)3) showing, numbering and underlining all the steps you carry
out in the calculations. (4)
F V (λ1(λ2 1)3) = {2} and max(F V (λ1(λ2 1)3)) = 2.
Hence ω1(λ1(λ2 1)3) =0
.
.
.
4. In the SML files, you were given the following LEXP terms (which implement terms
of M):
val vx = (ID "x");
val vy = (ID "y");
val vz = (ID "z");
val t1 = (LAM("x",vx));
val t2 = (LAM("y",vx));
val t3 = (APP(APP(t1,t2),vz));
val t4 = (APP(t1,vz));
val t5 = (APP(t3,t3));
val t6 = (LAM("x",(LAM("y",(LAM("z",
(APP(APP(vx,vz),(APP(vy,vz))))))))));
val t7 = (APP(APP(t6,t1),t1));
val t8 = (LAM("z", (APP(vz,(APP(t1,vz))))));
val t9 = (APP(t8,t3));
For example vx implements the variable x. The SML term t1 implements the M
term λx.x.
Give the full term of M implemented by the SML LEXP term t9. (0.5)
The SML term t9 implements the M term · · ·
5. Give the term It8 of IEXP that correspond to t8 of LEXP. (0.5)
val It8 = ...
6. Give the term Bt2 of BEXP that corresponds to t2 of LEXP. (0.5)
7
val Bt2 = ....
7. Remote login to your university account (or do whatever you usually do to get to the
university machines, or if you have SML on your own computer then do the work on
your own computer).
On university machines, in the same directory in which you have the files assign21-
help.sml, type the following line (and hit return):
poly
You will get the prompt
>
Type at the prompt the following:
>use "assign21-help.sml";
If you want, read and understand the messages you get, but don’t bother if you don’t
want to, or you think you don’t udnerstand.
Then, test the commands below (in poly) and write the output of the following: (1)
subs vy "x" t2;
subs vx "y" t2;
>subs vy "x" t2;
val it ...
>subs vx "y" t2;
val it ...
8. Give (λy.x)[x := y] and compare with subs vy ”x” t2 above. (1.5)