\documentclass{article}
\usepackage{latexsym}
%\usepackage{lcom}
%\usepackage{cdsty}
%\input{minml-defns}
\newcommand{\AMvsk}{\\[2ex]}
\newcommand{\AMlaz}[3]{\mbox{\textbf{lazy }} {(#1} : {#2)} \mbox{\textbf{
      is }} {#3}}
\newcommand{\AMfun}[3]{\mbox{\textbf{fun }} {#1} {#2} \mbox{\textbf{ is }}
 { #3}\mbox{ \textbf{end} }}
\newcommand{\AMcasest}[3]{\mbox{\textbf{strcase  }} {#1}\mbox{\textbf{ of }}
  {#2}\Rightarrow {#3}}
\newcommand{\AMts}{\tau \mbox{ stream}}
\newcommand{\AMcons}{Cons(e_h,e_t)} 



\begin{document}
\section{Streams\hfill\fbox{30 Points}}

In this question we investigate \emph{lazy} infinite lists or
\emph{streams}. Those are lists that that continually generate the
next element, without ever reaching the end of the list.  This view of
data structures as being in the process of creation conflicts with the
call-by-value evaluation strategy of {\textsf{MinML}}, since under the eager
approach all expressions are fully evaluated before they are used,
whereas we would like to evaluate them only as much as absolutely
necessary to allow the overall computation to proceed.  For example
in SML:
\begin{verbatim}
     datatype lazy 'a stream = Cons of 'a * 'a stream
\end{verbatim}
The keyword "lazy" indicates that values of type 'a stream are
suspended computations that, when evaluated, yield a value of the form
Cons (x, c), where x is a value of type 'a, and c is another value of
type 'a stream, i.e., another computation of such a value.

Since the description of values of this type we've just given is
clearly "circular", we must employ a recursive value binding to create
one.  Here's a definition of the infinite stream of 1's as a value of
type \texttt{int stream}:
\begin{verbatim}
     val rec lazy ones = Cons (1, ones)
\end{verbatim}

\texttt{ones} is bound to the computation that, when evaluated, yields
\texttt{Cons(1, ones)}, a stream whose head element is 1 and whose
tail is the very same computation again.  Thus if we evaluate the tail
of ones we will, once again, obtain the same value, and so on ad
infinitum.  Values of stream type are taken apart by pattern matching.
For example, we may evaluate the binding
\begin{verbatim}
     val Cons (h, t) = ones
\end{verbatim}

\smallskip

The aim of this question is to
endow {\textsf{MinML}} with this faculty, without changing the call-by-value
nature of function application. We add the following tokens to the
language:
\[
\begin{array}{rrcl}
\mathit{Types} & \tau &  ::= &\dots\mid\AMts\\
\mathit{Expressions}& e & ::= & \dots\mid
Cons(e_h,e_t)\mid\AMcasest{e_s}{Cons(h,t)}{e}\\
& & & \mid\AMlaz{s}{\AMts}{\AMcons}
\end{array}
\]
where $s$ is bound in $e_t$ but not in $e_h$.


For example, the streams of 1's
is defined as follows:
$$\AMlaz{ones}{int \ stream}{Cons(1,ones)}$$
Here's the code for taking the tail of a stream:
$$\AMfun{stail}{(s:int\ stream) : int}{(\AMcasest{s}{Cons(h,t)}{t})}$$



\subsection{First Part\hfill\fbox{5 Points}}
\begin{itemize}
\item Define the set of free variables for \textbf{lazy} and
  \textbf{strcase} and the set of values:
\vspace*{2in}

\item
Next define a function \texttt{take : int*int\ stream -> int list},
which builds a list containing the first $n$ elements of a stream. You
can assume SML syntax for ordinary lists and integers and that
\textbf{fun} accepts a pair of arguments:
\vspace*{2in}

\item
Trace the evaluation of the application of the latter function to
$\AMlaz{ones}{int \ stream}{Cons(1,ones)}$.
\vspace*{2in}
\end{itemize}
\subsection{Second Part\hfill\fbox{10 Points}}
 Give typing rules:
\vspace*{2in}

%$$\Gamma\vdash\AMcasest{s}{\AMcons}{e}:\tau$$ 
\subsection{Third Part\hfill\fbox{10 Points}} 

Give SOS evaluation rules:
\vspace*{3in}


\subsection{Last Part\hfill\fbox{5 Points}}
 Suppose we now want to introduce \emph{streams of
    streams}, say for example a stream consisting of a stream of 1's;
$$\AMlaz{ss}{(int\ stream) \ stream}{Cons({\AMlaz{ones}{int \
      stream}{Cons(1,ones)}}), ss)}$$ 
Let us define
$$\AMfun{shd}{(s:int\ stream) : int}{(\AMcasest{s}{Cons(h,t)}{h})}$$
and consider the evaluation of 
$$shd(shd(\AMlaz{ss}{(int\ stream) \ stream}{Cons({\AMlaz{ones}{int \
      stream}{Cons(1,ones)}}, ss)}))$$
which should return $1$, that is the head of the inner stream, where
we have used the name of the function as the identifier for its value.

Does this work? If so, trace the evaluation. Otherwise informally
sketch a change in the operational semantics that would allow this
computation.
\vspace*{3in}


\ifsoln

\clearpage
\subsection{Solution}
\begin{enumerate}
\item
\begin{itemize}
\item
\begin{eqnarray*}
FV(\AMlaz{s}{\AMts}{\AMcons})& = & FV(e_h)\cup (FV(e_t)\setminus\{s\})\\
FV(\AMcasest{e_s}{Cons(h,t)}{e})& =& FV(e_s)\cup (FV(e)\setminus\{h,t\})
\end{eqnarray*}

\item 
\[
\begin{array}{rrcl}
\mathit{Values}& v & ::= & \dots\mid Cons(v_h,e_t)
%\mid\AMlaz{s}{\tau\  stream}{Cons(v_h,e_t)}
\end{array}
\]
\item
\[
\begin{array}{l}
\mathbf{fun\ }((n,s):int*int\ stream) :  int\ list \ \mathbf{is} \ 
\\
\qquad\mathbf{IF\ } n=0\ \mathbf{THEN\ } nil\ \mathbf{ELSE} \\
\qquad\qquad\AMcasest{s}{Cons(x,s)}{x:: take( (n-1), s)}\\
\mathbf{end}
\end{array}
\]

\end{itemize}
\item
\[
\begin{array}{c}
\frac{\Gamma\vdash e_h : \tau\qquad\Gamma\vdash e_t : \AMts}{\Gamma\vdash Cons(e_h,e_t):\AMts}{Ty-Cons}\AMvsk
 \frac{\Gamma\vdash e_h : \tau\qquad\Gamma[s:\AMts]\vdash e_t : \AMts}{\Gamma\vdash
   \AMlaz{s}{\AMts}{Cons(e_h,e_t):\AMts}}{Ty-Lazy}\AMvsk
 \frac{\Gamma\vdash e_s : \AMts\qquad\Gamma[h:\tau,t:\AMts]\vdash
   e:\tau'}{ \Gamma\vdash\AMcasest{e_s}{Cons(h,t)}{e}:\tau' }{Ty-CaseStr}
\end{array}
\]
\item
\[
\begin{array}{c}
\frac{e_h\mapsto e'_h}{\AMcons\mapsto Cons(e'_h,e_t)}{Search-H}\AMvsk
\frac{e_h\mapsto e'_h}{\AMlaz{s}{\AMts}{\AMcons}\mapsto
  \AMlaz{s}{\AMts}{Cons(e'_h,e_t)}} {Search-L}\AMvsk
 \frac{e_s\mapsto
   e_s'}{\AMcasest{s}{Cons(h,t)}{e}\mapsto\AMcasest{s'}{Cons(h,t)}{e}}{Search-C}\AMvsk
\AMvsk
\frac{}{\AMlaz{s}{\AMts}{Cons(v,e_t)}\mapsto[\AMlaz{s}{\AMts}{Cons(v,e_t)}
  /s]Cons(v,e_t)}{Eval-L}\AMvsk
\frac{}{\AMcasest{Cons(v,s)}{Cons(h,t)}{e}\mapsto[v/h,s/t]e}{Eval-C}
\end{array}
\]
\item

The computation will loop under the search rule for
\textbf{lazy}, because the language is eager in the head of the
stream. We can make the latter lazy as well, by considering $\AMcons$ a
value, dropping the search rules but $Search-C$ and changing $v$ in
$e_h$ in the evaluation rules $Eval-L, Eval-C$.

\end{enumerate}
\fi

\end{document}