COMP3610/6361 Principles of Programming Languages
Assignment 1
ver 1.1
Submission Guidelines
Due time: Aug 31, 2023, 11am (Canberra Time)
Submit a pdf via Wattle.
Scans of hand-written text are fine, as long as they are readable and neat.
Please read and sign the declaration on the last page and attach a copy to your submission.
No late submission, deadline is strict
Exercise 1 (Type Preservation) (15 Marks)
In the lecture we discussed alternatives for the semantics rule for assignment and sequential composition.
Among others we looked at the following:
Does Type Preservation hold for the variant language with rules (assign1’) and (seq1’) instead of (as-
sign1) and (seq1)?
If not, give an example, and explain which changes to the typing rules would be needed to get the prop-
erty back; if yes, sketch a proof.
Exercise 2 (Structural Induction) (25 Marks)
A BTree is defined by the following grammar.
T ::= Id | One T | Two T T
That means that leaves are labelled ‘Id’, and inner nodes can have One or Two children.
Question 1 Define a function leaves that determines the number of leaves for a given tree.
Question 2 Define a function two succ that determines the number of nodes with two children.
Question 3 Derive an induction principle for BTree
Question 4 Prove that any tree B with n leaves has exactly n+1 nodes with two children:
leaves B= (two succ B)?1
2 COMP3610/6361
Exercise 3 (Functions) (25 Marks)
Question 5 Calculate the free variables of the following expressions:
1. x+(fn y : int? z)
2. (fn y : int? (fn y : int? (fn y : int? y)))
3. while !l0 ≥ y do l0 := x
Draw also their abstract syntax trees (up to alpha equivalence).
Question 6 Perform the following substitutions:
1. {y z/x}(fn x : int y x)
2. {z x/x}(fn y : int y x)
3. {z x/x}(fn z : int (fn x : int y x) x z)
Exercise 4 (Nested substitution) (25 Marks)
Question 7 For the language variant featuring while, if-statement and functions (no recursion), show
the following statement.
{E3/y}{E2/x}E1 = {({E3/y}E2)/x}{E3/y}E1
where x and y are variable with x = y, and E1, E2 and E3 expressions with x ∈ fv(E3). Clearly state your
proof strategy and mark the places where the assumptions are used.
Exercise 5 (Exception Handling) (10 Marks)
When using error handling in its simplest form (see lecture), the progress property does not hold.
Question 8 Explain why the property is broken and give an example.
Question 9 Fix the progress theorem in a way that it still captures the essence of progress. The theorem
should hold for languages with error handling. Other properties such as type preservation and type safety
should stay valid.
P. Ho¨fner 3
Academic Integrity
I declare that this work upholds the principles of academic integrity, as defined in the University Aca-
demic Misconduct Rule; is entirely my own work, with only the exceptions listed; is produced for the
purposes of this assessment task and has not been submitted for assessment in any other context, except
where authorised in writing by the course convener; gives appropriate acknowledgement of the ideas,
scholarship and intellectual property of others insofar as these have been used; in no part involves copy-
ing, cheating, collusion, fabrication, plagiarism or recycling.
Date Signature