© P. Ho¨fner
COMP3610/6361 Principles of Programming Languages
Assignment 3
ver 1.0
Submission Guidelines
• Due time: Oct 12, 2023, 23:59pm (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 (Data Structure) (40 Marks)
Next to products, sums and records we want to extend our language by the data structure of binary trees.
Nodes (and leaves) in the tree should carry values of type T .
The new syntax should be
E ::= empty[T ] // empty tree of type T
fork[T ] E E E //tree constructor of the form < node>< tree>< tree>
right[T ] E //right subtree
left[T ] E //left subtree
content[T ] E //content of node
isEmpty[T ] E //test for emptyness
isLeaf[T ] E //test whether the tree consist of a single node only
Question 1 Define values and types necessary to define binary trees.
Question 2 Define meaningful semantics (small step) for trees, based on the given syntax. (The mean-
ing of the expressions should be obvious.) You can use a variant of IMP that features error handling (you
choose which kind).
Question 3 Provide typing rules for your semantics.
Question 4 Argue (or prove) that the progress and preservation theorems hold for your extension, when
assuming our while language IMP as base, including booleans.
(Remember to justify your answers.)
2 COMP3610/6361
Exercise 2 (Semantic Equivalence) (35 Marks)
Question 5 Prove cases “if then E2 else E3” and “while E1 do ” of the Congruence theorem for
semantic equivalence (Lecture 20/09).
Question 6 Prove that if Γ1 ⊢ E1 :unit and Γ2 ⊢ E2 :unit with Γ1 disjoint from Γ2 then, for Γ= Γ1∪Γ2,
E1 ; E2 ≃unitΓ E2 ; E1 .
Question 7 Prove that the programs l : int ref ⊢ l := 0:unit and l : int ref ⊢ l := 1:unit are not contex-
tually equivalent. Hint: find a context that will diverge for one of them, but not for the other.
Exercise 3 (Denotational Semantics) (25 Marks)
Question 8 Using denotational semantics (as defined in the lecture), prove that skip ; c and c ; skip are
equivalent. That means, show
C [[skip ; c]] = C [[c ; skip]] .
Question 9 For the definition of the semantics of while, we used the function
F( f ) ={(s,s) | (s,false) ∈B[[b]]} ∪
{(s,s′) | (s,true) ∈B[[b]] ∧
∃s′′. (s,s′′) ∈ C [[c]]∧ (s′′,s′) ∈ f}
(see lecture). By Kleene’s fixed point theorem we have that fix (F) =
⋃
i≥0F i( /0)
• Prove that while false do c is equivalent to skip. Hint: prove (by induction) that F i( /0) = {(s,s)}.
• Calculate C [[while true do skip]] using the same technique.
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