\documentclass[letterpaper]{kwart}

\usepackage{../notation}
\usepackage{../assign}
\usepackage{../proof}

\deftok{|}{\mathrel|}
\deftok{#}{\mathbin\#}
\deftok{=>}{\Rightarrow}
\deftok{|->}{\mathrel\mapsto}
\deftok{__}{\_}
\deftok{~}{\;}
\deftok{@}{\>}
\deftok{->}{\mathrel\rightarrow}
\deftok{...}{\ldots}
\deftok{.}{\mathpunct.}
\deftok{::}{::}
\easynotation

\begin{document}
  \title{Assignment 3: Adding streams to MinML}
  \author{15-312: Foundations of Programming Languages \\
    Kevin Watkins $\langle$kw@cmu.edu$\rangle$}
  \date{Out: Thursday, February 10, 2005 \\
    Due: Thursday, February 17, 2005 (10:30 a.m.) \\[1ex]
    50 points total}
  \maketitle

  In this written assignment, you're asked to add recursive streams
  to MinML. You'll have to provide the static and dynamic semantics
  for the new constructs and prove type safety for the extended language.

\kwd{nil}\kwd{cons}\kwd{rec}\kwd{case}\kwd{of}
  \section*{MinML with recursive streams}
  Our new version of MinML is the language from Assignment~2 extended with
  the following constructs for recursive streams.

  \medskip\centerline{%
  \begin{tabular}{lll}
    Construct & Concrete & Abstract (h.o.a.s.) \\
    \hline
    Empty stream & >nil & >{nil()} \\
    Recursive cons & >{cons~rec~x = e1#e2} & >{cons(x.e1,x.e2)} \\
    Case of stream & >{case~e~of~nil => e1 | x#y => e2} &
      >{case(e,e1,x.y.e2)} \\
  \end{tabular}}\medbreak

  Right now, you have no idea what these constructs mean.  Below, we try
  to give some intuition for what they should mean by example.  But part
  of your job for this assignment is to say, yourself, precisely what
  they mean, by giving static and dynamic semantics for them.

  The recursive cons >{cons~rec~x=e1#e2} constructs a stream with head~>e1
  and tail~>e2. The quirk that makes a recursive stream different from an
  ML list, say, is that the variable >x stands for the stream itself
  within >e1~and~>e2 (so >x~is a bound variable with >e1~and~>e2 as its
  scope). In this way a recursive stream can refer to itself within its
  definition. You can think of the symbol~># as being analogous to ML's
  list constructor~>::. If >x~doesn't actually occur in >e1~or~>e2, then
  the recursive cons is more like a list cons, and we can abbreviate
  >{cons~rec~x=e1#e2} as >{cons~rec~__=e1#e2} or even just >{e1#e2}.

  There is a new case construct for taking a stream apart. The meaning of
  >>{case~e~of~nil=>e1|x#y=>e2} is~>e1 if >e~is~>nil, or~>e2 if >e~is a
  cons. When it's a cons, the variables >x~and~>y stand for the head and
  tail of the stream. Their scope is~>e2.

\kwd{stream}
  The operational semantics of streams is lazy; in >{cons~rec~x=e1#e2},
  >e1~and~>e2 are not evaluated until the value is needed. It's hard to
  see how recursive streams could be defined in a non-lazy way without
  leading to infinite looping in the examples below.
  To keep things simple, we only consider streams of integers; these
  have type >stream.

  Now we present a few examples intended to guide you
  in defining the \emph{precise} static and dynamic semantics of
  recursive streams. In the informal descriptions we write
  >{[x,y,z,...]} for the finite or infinite sequence of integers
  making up a stream.

\kwd{fun}\kwd{is}\vname{plus}\kwd{end}
  \begin{quote}
    \qquad >{cons~rec~x=1#(cons~rec~y=2#nil)}

    The finite stream >{[1, 2].}

    \qquad >{1#2#nil}

    The same, abbreviated.

\vname{ones}
    \qquad >{ones = (cons~rec~x=1#x)}

    The infinite stream >{[1, 1, ...]}.

    \qquad >\begin{array}{@{}l@{}}
      plus = fun~plus(s1:stream):stream -> stream~is\\
      \quad fun~p(s2:stream):stream~is\\
      \qquad case~s1~of\\
      \qquad\quad nil => nil\\
      \qquad\quad {}| x1#s1' => case~s2~of\\
      \qquad\qquad nil => nil\\
      \qquad\qquad {}| x2#s2' => (x1+x2)#plus@s1'@s2'\\
      \quad end\\
      end\\
    \end{array}

    Add finite or infinite streams >{[x1, y1, ...]}
      and >{[x2, y2, ...]}, yielding >{[x1+x2, y1+y2, ...]}.

\vname{map}\kwd{int}
    \qquad >\begin{array}{@{}l@{}}
      map = fun~map(f:int->int):stream->stream~is\\
      \quad fun~m(s:stream):stream~is\\
      \qquad case~s~of\\
      \qquad\quad nil => nil\\
      \qquad\quad {}| x#s' => (f@x)#(m@s')\\
      \quad end\\
      end\\
    \end{array}

    Map >f over the finite or infinite stream >{[x1, x2, ...]},
      yielding >{[f@x1,f@x2,...]}.

\vname{nats}
    \qquad >{nats=(cons~rec~s=0#(plus@ones@s))}

    The infinite stream >{[0,1,2,3,...]}.

\vname{fibs}
    \qquad >{fibs=(cons~rec~s=0#(cons~rec~t=1#(plus@s@t)))}

    The Fibonacci numbers >{[0,1,1,2,3,5,8,...]}.
  \end{quote}



\defvariable{G}{\Gamma}
\defvariable{t}{\tau}
\deftok{|-}{\mathrel\vdash}
\fname{dom}
\rname{VarTyp}\rname{NumTyp}\rname{TrueTyp}\rname{FalseTyp}
\rname{IfTyp}\rname{FunTyp}\rname{AppTyp}\rname{OpTyp}
\rname{LetTyp}
\kwd{int}\kwd{bool}\kwd{true}\kwd{false}\kwd{if}\kwd{then}
\kwd{let}\kwd{in}\kwd{else}
\deftok{&}{&}
  \begin{figure}
    \renewcommand{\arraystretch}{2}
    >>\begin{array}{cc}
      \rul[VarTyp] G(x) = t \over{G |- x : t} &

      \ax[NumTyp]{G |- k : int} \\

      \ax[TrueTyp]{G |- true : bool} &

      \ax[FalseTyp]{G |- false : bool} \\

      \rul[IfTyp] G |- e : bool \quad G |- e1 : t \quad G |- e2 : t
        \over{G |- if~e~then~e1~else~e2~end : t} &

      \rul[OpTyp] G |- e1 : to1 \quad ... \quad G |- en : ton
        \over{G |- o(e1,...,en) : to} \\

      \rul[FunTyp^{1}] G,(f:t1->t2),(x:t1) |- e : t2
        \over{G |- fun~f(x:t1):t2~is~e~end : t1 -> t2} &

      \rul[AppTyp] G |- e1 : t2 -> t \quad G |- e2 : t2
        \over{G |- e1@e2 : t} \\

      \rul[LetTyp^{2}] G |- e1 : t1 \quad G, x:t1 |- e2 : t2
        \over{G |- let~x=e1~in~e2~end : t2} &

      {}^{1}\enspace f,x \notin dom@G
      \hfil{}^{2}\enspace x \notin dom@G
    \end{array}

    \caption{Static semantics of the original MinML}
    \label{fig:minml-static}
  \end{figure}



  \section{Static semantics}
  The static semantics of the original MinML is shown in Figure~\ref{fig:minml-static} for your reference.

  \begin{question}{1.1}\points{5}%
    Write the full grammar of MinML types~>t and expressions~>e
    extended with the new constructs. (Include only the ``official'' syntax,
    not the abbreviations.)
  \end{question}

  \begin{question}{1.2}\points{5}%
    Define the typing judgment >{G |- e : t} for each of the new syntactic
    constructs.
  \end{question}



\rname{OpArg}\rname{OpVals}\rname{IfCond}\rname{IfTrue}\rname{IfFalse}
\rname{AppFun}\rname{AppArg}\rname{AppCall}\rname{LetArg}\rname{LetVal}
  \begin{figure}
    \renewcommand{\arraystretch}{2}
    >>\begin{array}{c}
      \rul[OpArg] ei |-> ei'
        \over{o(v1,...,ei,...,en) |-> o(v1,...,ei',...,en)} \\

      \rul[OpVals] \hbox{(by primop $o$)}
        \over{o(v1,...,vn) |-> v} \\

      \rul[IfCond] e |-> e'
        \over{if~e~then~e1~else~e2~end |-> if~e'~then~e1~else~e2~end} \\

      \ax[IfTrue]{if~true~then~e1~else~e2~end |-> e1} \\

      \ax[IfFalse]{if~false~then~e1~else~e2~end |-> e2} \\

      \rul[AppFun] e1 |-> e1'
        \over{e1@e2 |-> e1'@e2} \hfil 

      \rul[AppArg] e2 |-> e2'
        \over{v1@e2 |-> v1@e2'} \\

      \rul[AppCall] (v1 = fun~f(x:t1):t2~is~e~end)
        \over{v1@v2 |-> \{v1,v2/f,x\}e} \\

      \rul[LetArg] e1 |-> e1'
        \over{let~x=e1~in~e2~end |-> let~x=e1'~in~e2~end} \\

      \ax[LetVal]{let~x=v1~in~e2~end |-> \{v1/x\}e2} \\
    \end{array}
    \caption{Dynamic semantics of the original MinML}
    \label{fig:minml-dynamic}
  \end{figure}



  \section{Dynamic semantics}
  The dynamic semantics of the original MinML is shown in Figure~\ref{fig:minml-dynamic} for your reference.

  \begin{question}{2.1}\points{5}%
    Write the grammar of MinML values~>v extended with the new constructs.
  \end{question}

  \begin{question}{2.2}\points{5}%
    Complete the dynamic semantics for the new constructs. You must define
    a small-step semantics >{e |-> e'}. The evaluation of >{cons~rec} must
    be lazy, and the semantics must be deterministic (but you don't have to
    prove this).
  \end{question}

  \begin{question}{2.3}\extra
    Extend the definition of the C-machine >{s |-> s'} with the new
    constructs for streams.
  \end{question}


  \section{Type safety}
  You are free to make use of the following lemmas. You do not have to
  prove them.  (But if these lemmas don't
  hold for your static semantics from Section~1, you must go back and
  change it so that they do.)

  \begin{quote}
  \heading{Weakening}If >{G |- e : t} and >{x \notin dom@G}, then
    >{G, (x:t') |- e : t}.

  \heading{Value substitution}If >{\cdot |- v : t'} and >{(x:t'), G |- e : t}
    then >{G |- \{v/x\}e : t}.
  \end{quote}

  If you use any lemmas other than the ones above, you must state and prove them too.

  \begin{question}{3.1}\points{30}%
    State and prove the preservation and progress theorems for your new
    language. You can skip any cases for rules and constructs that haven't
    changed from the original MinML (but your proofs must be structured
    in such a way that the skipped cases work exactly the way they were
    done in lecture).

    Be sure to show all necessary steps in your proofs---the model solution
    for Assignment~1, available from the course web page, has more
    information on what ``necessary'' means.
  \end{question}

\end{document}
