Programming Languages

Problem Set 6

This problem set will be graded out of 20.

- baby
- The client of a factory can ask for the creation of a "baby" doll, one that is solid wood and contains no other doll.
- shell
- The client can return any doll
*d*to the factory and ask for a "shell" doll, a new, hollow doll*d'*that contains*d*. - box
- The client can pass a list of dolls back to the factory and ask for a
shipping carton (
`box`) containing them all. - weight
- The weight of a baby doll is 10 grams. The weight of a shell doll
containing
*n*dolls*10(n+1)*plus the weight of all the dolls contained. The weight of a box is 1000 grams plus the weight of the dolls contained. The client can ask for the weight of any box.

**Note:** A baby doll weighs 10 grams. A doll
`shell(baby)` weighs 30 grams: 20 for the shell, 10 for the baby. The
doll `shell(shell(baby))` weighs 60 grams: 30 for the outer shell, 20 for
the inner shell, 10 for the baby.

If I create

a = baby b = shell(a) c = baby d = shell(c) e = shell(d)Then I can create a box with the list [b,e].

bx = box([b,e])

2. [8 points] In class, we defined an extension of MinML with exceptions. Here is the syntax:

types

t ::= int | bool | t -> t | t cont

expressions

e ::= x | n | b | if e then e else e | fun
f(x:t) : t = e | e e | try e with e | fail

values

v ::= n | b | fun(x:t) : t = e

evaluation contexts (for call-by-value, left-to-right evaluation)

E ::= [] | if E then e else e | E e | v E |
try E with e

See the class note for the operational semantics and type system.
Notice that the operational semantics is defined by two judgments: top
level evaluation (e --> e) and beta reduction/ instruction rules (e -->i e).
The only rules for top-level evaluation are these:

e -->i e'

---------------

E[e] --> E[e']

(try E' with e) not in E

-------------------------

E[fail] --> fail

Let's think about how to prove type safety -- the statements of the lemmas
involved will obviously change slightly from our previous proofs since the
structure of the operational semantics has changed. Let's specifically
consider proving a type preservation lemma. Our goal is to prove that the
top-level operational relation is sound:

Theorem: Preservation of Top-level Evaluation: If |-- e
: t and e --> e' then |-- e' : t.

Proof: ??

In order to do this, we will have to reason about the beta-reduction rules. The beta-reduction rules and their typing are not substantially different from any of the systems we have looked at in the past, so we can prove the following lemma in the ordinary way:

Lemma: Preservation of Instruction Rules: If |-- e : t and e -->i e' then |-- e' : t.

Proof: By induction on the operational relation e -->i e'.

[8 points] Your job: assuming you have already proven the Preservation of
Instruction Rules Lemma + any Lemmas concerning Substitution, Weakening,
Exchange, Inversion of Typing, Canonical Forms that you would like, prove the
Preservation of Top-level Evaluation Lemma. **Hint:** define a typing
judgement (via a collection of inference rules) for contexts E and prove a lemma
about the typing relation for contexts.