CS430/530 Assignment 6

Last modified: November 18, 2013.
Solution posted: November 25, 2013

Due: Thursday, November 17, 2013 (extended)
Due: Thursday, November 21, 2013

  1. In the language $\mathcal{L}\{\mu_i\mu_f\}$ of chapter 15, write the following terms: Notes:
  2. Find expressions $e_0$, $e_1$ and types $\tau_0$, $\tau_1$, $\tau_2$, $\tau_3$, $\tau_4$, $\tau_5$, $\tau_6$, and $\tau_7$ such that the following typing judgements are derivable in System F:

    In the last case, nat is defined as $\forall t.(t \to t) \to t \to t$.
    Which of these examples are invalid in the predicative fragment and which in the prenex fragment?
  3. Write an implementation of the stack abstract data type in the language $\mathcal{L}\{\to\forall\exists\}$ of Harper's chapter 21. You should support three operations: formation of the empty stack, push value on top of the stack, and pop value off the top of the stack. Also, show how a client function can be defined which takes a stack of an arbitrary implementation of the abstract data type, and extends that implementation with a peek2 function that returns the second element from the top of the stack (or unit if the stack has less than two elements). You should give two expressions:

    You can assume that the language supports (labeled) products, sums, recursive types, and the fixpoint construct.

  4. What is the correspondence between the semantics using the control machine (Harper, chapter 27) and contextual dynamic semantics (based on evaluation contexts) as defined in (Harper, chapter 5.3)? Make this correspondence formal by stating soundness and completeness conditions (as in 27.3), and the main lemmas that you would use in proving these.

    Contextual semantics for $\mathcal{L}\{nat \to\}$ are defined as follows:

    $e := z \; | \; s(e) \; | \; ifz(e;e_1;x.e_2) \; |\; ap(e_1;e_2) \; |\; lam[\tau](x.e) \; |\; x \; |\; fix[\tau](x.e)$
    $v := z \; | \; s(v) \; |\; lam[\tau](x.e)$
    $\mathcal{E} := \circ \; | \; s(\mathcal{E}) \; | \; ifz(\mathcal{E};e_1;x.e_2) \; |\; ap(\mathcal{E};e_2)$
    $$ \frac{e \longrightarrow e'}{\mathcal{E}[e] \longrightarrow \mathcal{E}[e']} $$ $$ \frac{}{ifz(z;e_1;x.e_2) \longrightarrow e_1} $$ $$ \frac{}{ifz(s(v);e_1;x.e_2) \longrightarrow [v/x]e_2} $$ $$ \frac{}{ap(lam[\tau](x.e);e') \longrightarrow [e'/x]e} $$ $$ \frac{}{fix[\tau](x.e) \longrightarrow [fix[\tau](x.e)/x]e} $$

Sample Solutions

Sample solutions are here as well as on the Zoo machine /c/cs430/as/as6/as6-sol.v.