CS430/530 Assignment 6

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:
   • MULT: Multiplication of two natural numbers
   • PRED: The predecessor function for natural numbers. (Hint: read chapter 17.2!)
   • MINUS: The subtraction operation for natural numbers.
   • GT: For two natural numbers $n_1$ and $n_2$, returns true if $n_1 > n_2$, and false otherwise.
   • LENGTH: Returns the length of a list.
   • APPEND: Appends one list to another.
   • POWER: Given a natural number $N$, the stream of successive powers of $N$: $(N^0, N^1, N^2, \cdots)$
   • FACTORIAL: The stream of factorials of successive numbers ([n!] = 1, 2, 6, 24, ...)
   • TAKE: Given a stream S and a natural number N, returns a list having the N first numbers in S.
   • MERGE: Given two increasing streams, returns a merged increasing stream.
   Notes:
   • The type of natural numbers is: $\mu_i t.unit + t$, of lists: $\mu_i t.unit + nat \times t$, and of streams: $\mu_f t.nat \times t$.
   • If you want, you can develop these in Coq, using the following file: chap15.v. The function PLUS is provided as an example. Please don't use Coq's native types and pattern matching constructs; this file is provided so that you can stay close to Harper's syntax.

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:

   • $\vdash e_0 : \forall t.t \to t$
   • $\vdash e_1 : \forall t_1.\forall t_2.\forall t_3.(t_1 \to t_2) \to (t_2 \to t_3) \to (t_1 \to t_3)$
   • $\vdash \lambda (x : \forall t.t \to t)~x [\tau_0] (x [\tau_1]) : \tau_2$
   • $\vdash \lambda (x : \forall t.t \to t)~x [\tau_3] x : \tau_4$
   • $\vdash \lambda (x : \forall t.t \to t)~\Lambda t.x [\tau_5] (x [t]) : \tau_6$
   • $\vdash \lambda (m : nat)\lambda (n : nat)~\Lambda t.n [t \to t] (m [t]) : \tau_7$
   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:
   

   • $STACK = \exists t.\langle emp : t, push : nat \to t \to t, pop : t \to nat \times t + unit \rangle$
   • $e_{impl} : STACK$
   • $STACKext = \exists t.\langle emp : t, push : nat \to t \to t, pop : t \to nat \times t + unit, peek2 : t \to nat + unit\rangle$
   • $e_{client} : STACK \to STACKext$

   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} $$