本次澳洲代写是Principles of Programming Languages的一个assignment

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

Exercise 2 (Semantic Equivalence)

Question 5 Prove cases “if then E2 else E3” and “while E1 do ” of the Congruence theorem for
semantic equivalence (Slide 20, Lecture 13).