\documentclass[10pt]{article} 
\usepackage{amsmath}
\usepackage{611}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% CS611: Please fill in these macros as appropriate:
\newcommand{\homework}{3}      %%% Replace ? by homework number
\newcommand{\due}{October 19, 2001}    %%% Replace ??/??/?? by MM/DD/YY format
                               %%% due date
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ml}[1]{\texttt{#1}}
\newcommand{\mlarr}{-\symbol{62}} % only works properly in tt fonts

\begin{document}
\hwheader

\section*{What to turn in}

Turn in the written parts of the assignment during class on the due date. 
For the programming part, you should mail your version of the file
\T{translate.ml} to \texttt{nystrom@cs.cornell.edu} by 5{\sc pm}
on that day. The short problems (4,5) will not be worth as much as
the others.

\begin{enumerate}

\item "Substitution Lemma"

We define the small step parallel reduction
semantics for lambda expressions as follows:
\[
\infer{x \pstepsto x}{}
\]
\medskip
\[
\infer{t_1~t_2 \pstepsto t_3~t_4}{t_1 \pstepsto t_3 & t_2 \pstepsto t_4}
\]
\medskip
\[
\infer{\lambda~x~t_1 \pstepsto \lambda~x~t_2}{t_1 \pstepsto t_2}
\]
\medskip
\[
\infer{(\lambda~x~t_1)~t_2 \pstepsto t_3~\{t_4/x\}}{t_1 \pstepsto t_3 & t_2 \pstepsto t_4}
\]
Prove that $(t_1 \pstepsto t_2)~ \wedge~( t_3 \pstepsto t_4) \Rightarrow
t_1\{t_3/x\} \pstepsto t_2\{t_4/x\}$.

\item "Evaluation Contexts"

We extend the call-by-value $\lambda$ calculus with a primitive
exception mechanism as follows:
\begin{align*}
e &::= ~x~|~\lambda~x~e~|~e_1~e_2~|~"raise"~|~"try"~e_1~"handle"~e_2
\end{align*}

The expression {\bf raise}, encountered in either the operand or operator
position of an application, raises an exception and terminates the current
evaluation of the expression. The exception will be bubbled up until a
{\bf try} expression is reached. If $e_1$ in the {\bf try} expression 
raises an exception, we will start to evaluate $e_2$ in the exception
handler in the next step. 

{\bf raise} is not a value in this language. For example,
$"try"~((\lambda~x~1)~"raise")~"handle"~2$ evaluates to $2$ instead
of $1$, because $((\lambda~x~1)~"raise")$ evaluates to $"raise"$
instead of $1$.

Evaluation contexts $C$ for this language can be defined as:
\begin{align*}
v &::= ~\lambda~x~e\\ 
C &::= ~[~]~|~C~e~|~v~C~|~"try"~C~"handle"~e\\
\end{align*}

A redex $r_a$ for this evaluation context can have the following forms:
$$r_a ::= (\lambda~x~e)~v~|~"try"~D~"handle"~e~|~"try"~v~"handle"~e$$
Here, $D$ is an expression that contains an ``exposed'' {\bf raise}:
a {\bf raise}
that is not hidden in an $\lambda$ abstraction or a {\bf try} expression.
The formal definition of $D$ is:
$$D ::= ~"raise"~|~D~e~|~v~D$$

Given these definitions, the possible reductions are as follows:

\[
(\lambda~x~e)~v \stepsone_a e~\{v/x\}
\]
\[
"try"~D~"handle"~e~ \stepsone_a e
\]
\[
"try"~v~"handle"~e~ \stepsone_a v
\]

And we have the usual rule for reductions in an appropriate context:
\[
\infer{C[e] \stepsone_a C[e']}{e\stepsone_a e'}
\]
\begin{enumerate}
\item "Context Lemma"

Show that $\forall e, \mbox{if e is a closed term, then }(e = v) \vee (e = D) \vee (\exists~\mbox{unique}~C,~\mbox{unique}~r_a,~\mbox{such that}~ C[r_a] = e)$, 
where we define $C[t]$ as
\[
[~][t] = t \qquad (C~e)[t] = C[t]~e \qquad (v~C)[t] = v~C[t] \qquad 
("try"~C~"handle"~e)[t] = "try"~C[t]~"handle"~e   
\]

In English, show that for each closed term $e$ in this language, it is either a
value, of the form $D$, or that there is only one way to write down its
evaluation context.  This means that any expression $e$ can be evaluated
deterministically until we get a value $v$ or a term of the form $D$
(which must raise an exception).

\item "Equivalence of Evaluation Contexts"

There is another way to define evaluation contexts for this language. We
can remove $D$ and add more possible redexes $r_b$ as follows:
\begin{align*}
v &::= ~\lambda~x~e\\ 
C &::= ~[~]~|~C~e~|~v~C~|~"try"~C~"handle"~e\\
r_b &::= (\lambda~x~e)~v~|~"try"~"raise"~"handle"~e~|~"try"~v~"handle"~e~|~"raise"~e~|~v~"raise"
\end{align*}

The reductions for a redex $r_b$ are these:
$$(\lambda~x~e)~v \stepsone_b e~\{v/x\}$$
$$"try"~"raise"~"handle"~e~ \stepsone_b e$$
$$"try"~v~"handle"~e~ \stepsone_b v$$
$$"raise"~e \stepsone_b "raise"$$
$$v~"raise" \stepsone_b "raise"$$

Problem: show that all evaluations in the original semantics are also
permitted in the more verbose semantics:
$e \stepsone_a e' \Rightarrow e \stepsone_b^* e'$.
\end{enumerate}

\item "Iterators"

Consider a binary tree defined by the Java class "Tree":
\begin{verbatim}
class Tree {
    Tree left;
    Key here;
    Tree right;
}
\end{verbatim}

We'd like to define an iterator that returns the elements in the tree 
in pre-order.  The iterator might be used like this:
\begin{verbatim}
TreeIter i = new TreeIter(tree);
for (Key k = i.next(); k != null; k = i.next()) {
    // do something with k
}
\end{verbatim}
It's actually quite awkward to implement "TreeIter". We must explicitly save
the state of the iteration in a stack between calls to {\tt next()}.  For
instance,
\begin{verbatim}
class TreeIter {
  Stack stack;
 
  TreeIter(Tree t) {
    stack = new Stack();
    stack.push(t);
  }
 
  Key next() {
    while (! stack.empty()) {
      Tree t = (Tree) stack.pop();
 
      if (t.left == null && t.right == null) {
        return t.key;
      }
 
      if (t.right != null) stack.push(t.right);
      stack.push(new Tree(null, t.key, null));
      if (t.left != null) stack.push(t.left);
    }
 
    return null;
  }
}
\end{verbatim}

Writing Java iterators for more complex data structures is even more
difficult to get right. By contrast,
the language CLU (c. 1977)
has a powerful iterator construct that allows iterators to
be expressed more elegantly.  The iterator construct adds
two expression forms: $"for"~x~"in"~e_i~"do"~e_b$ and $"yield"~e$.
The idea is that a "for" expression evaluates the ``iterator'' $e_i$.
If a $"yield"~e_v$ expression is encountered during the evaluation of $e_i$,
the body of $e_b$ is evaluated in an environment where $x$ is bound
to the result of the evaluation of $e_v$.  After evaluating $e_b$,
control is transferred back into $e_i$ at the point of the "yield"
and evaluation continues as though the "yield" had resulted in $e_b$.
A "yield" expression not in the scope of any "for" expression should
raise a runtime error.  Note that the variable $x$ is bound in $e_b$ but not
in $e_i$.

If Java had CLU-style iterators, the binary tree iterator above could be
written simply:
\begin{verbatim}
elements() yields Key {
    for k in left.elements() do { yield k };
    yield key;
    for k in right.elements() do { yield k }
}
\end{verbatim}
And it could be used conveniently too:
\begin{verbatim}
for k in tree.elements() do {
    // do something with k
}
\end{verbatim}

Consider a version of "uF" augmented with "for" and "yield" expressions:
\begin{align*}
e & ::= n \mid x \mid "\#t" \mid "\#f" \mid "\#u" \\
 & \mid \lambda x~e \mid e_0~e_1 \mid "let"~x=e_0~"in"~e_1 \\
 & \mid "if"~e_0~"then"~e_1~"else"~e_2 \\
 & \mid "for"~x~"in"~e_i~"do"~e_b \mid "yield"~e \\
\end{align*}

\begin{enumerate}
\item
Extend the contextual operational semantics for uF to include
"for" and "yield" expressions.
\item
Give a translation of this language into standard "uF" in
continuation-passing style.
\end{enumerate}

\item "Continuity"

Consider the function
\[
\nm{minall} : (\omega_\bot\rightarrow \omega_\bot)\rightarrow\omega_\bot
= \lambda f:\omega_\bot\rightarrow \omega_\bot~.~\min_{y\in \omega} f(y)
\]
In this definition,
$\omega$ denotes the whole numbers (0, 1, 2, \ldots), and
the function $\min$ gives the smallest number
in all of the $f(y)$, or $\bot$ if $f(y)=\bot$ for some integer $y$.
Show that this function is monotonic but not continuous.

\item "Dynamic vs. Static Scope"

Consider the following uF program. What value does it have under
dynamic scope? Under the standard block-structured static scope?
Explain briefly (don't show the whole evaluation).
\newcommand\la{\ensuremath{\lambda}}
\begin{code}
~let f = \la{}n\la{}g1\la{}g2 (
~  let x = n+10 in
~   let g = (\la{}z x) in
~    if n==0 then (g \#u) + (g1 \#u) + (g2 \#u)
~               else (f (n-1) g g1)
~) in
~  (f 2 \#u \#u)
\end{code}

\item "Implementation"

Call-by-name evaluation often results in redundant computation.
For instance,
\begin{center}
\begin{minipage}{0pt}
  \begin{tabbing}
      "let" \= $x = 3 + 2~"in"$ \\
            \> "let" \= $y = x + 1~"in"$ \\
            \>       \> $y + y$
  \end{tabbing}
\end{minipage}
\end{center}
In this example, substituting $3+2$ for $x$ in the body of the "let" will cause
$3+2$ to be computed twice.  With call-by-value semantics $x$ and $y$ are
computed only once, but a computation may diverge (although not in this
example) even if the result of the computation is not used.  Since call-by-name
is inefficient, most lazy functional languages such as Haskell or Miranda
implement \emph{call-by-need}.  Call-by-need evaluation has the observational
behavior of call-by-name (assuming expressions have no side effects) but requires no more substitution steps than
call-by-value evaluation.  Call-by-need is often implemented by overwriting an
argument to an application with its value the first time it is evaluated, thus
avoiding the need to subsequent re-evaluation.  In the above program, the first
evaluation of $y$ will evaluate $x + 1$ and result in the value $6$.
Subsequent demands for the computation $x+1$ will immediately return $6$.

In this problem, you will write a translator from a call-by-need Scheme-like
language into a call-by-value language.

The implementation files for this question are found in the file
\T{need.tar.gz}, which is available from the course web page.  The
archive contains an implementation of a interpreter for the call-by-need
source language (described below) as well as an interpreter for the
call-by-value target language.  You can run the interpreters and your
translation using the \T{need} command.

The syntax for the full source language is given by: 
\[
\begin{array}{rcl}
\mathit{op} & ::= & \T{+} \mid \T{*} \mid \T{and} \mid \T{or} \\
\mathit{binop} & ::= & \T{-} \mid \T{=} \mid \T{\lt} \\
\mathit{unop} & ::= & \T{zero?} \mid \T{left} \mid \T{right} \\
\mathit{refop} & ::= & (\T{ref}~e) \mid (\T{!}~e) \mid (\T{:=}~e_1~e_2) \mid (\T{seq}~e_1~e_2~\ldots~e_n) \\
e & :: = & x \mid n \mid \T{true} \mid \T{false} \mid
	(\mathit{op}~e_1~e_2~\ldots~e_n) \mid
	(\mathit{binop}~e_1~e_2) \mid
	(\mathit{unop}~e) \mid
	\mathit{refop} \mid
	(\T{if}~e_0~e_1~e_2) \\
& & \mid \T{(fn (}x_1\ldots x_n \T{)}\; e\T{)}
  \mid \T{(}e_1~e_2~\ldots e_n\T{)} 
  \mid \T{(let ((}v_1\ e_1\T{)} \ldots\T{(}v_n\ e_n\T{))}\ e\T{)}
  \mid <e_1,e_2>
\end{array}
\]

\noindent In this syntax definition, $x$ stands for variable
identifiers, $n$ ranges over the integers and $A_1 \ldots A_n$
stands for one or more occurrences of syntactic objects of the form
$A$. Lambda abstractions with any number of arguments $x_1, \ldots,
x_n$ are written \T{(fn ($x_1 \ldots x_n$) $e$)}.  Both user-defined
functions and primitive operations are applied to their arguments using
prefix notation, just as in the simple lambda calculus.  Thus \T{(+ 3
4)} evaluates to \T{7}, and \T{((fn (x) (x)) 37)} evaluates to \T{37}

Arithmetic and boolean operators first evaluate their arguments and then
perform the operation.  Subtraction (\T{-}) and the relational operators (\T{=}
and \T{\lt}) expect exactly two integer arguments, while \T{+}, \T{*}, \T{and},
and \T{or} expects at least two, but possibly more, arguments.  The unary
operators expect one argument.

The operator \T{zero?} expects one argument and returns \T{\#t} if it is
an integer expression that evaluates to 0 and \T{\#f} if it is any other
value.

The \T{let} expression binds variables to expressions $e_i$ that may
be used in the body $e$.  The binding of $v_i$ is available in $e_j$
when $j\gt i$, as in the Scheme \T{let*} expression.

Pairs are enclosed in angle brackets (e.g., $<e_1, e_2>$). Pairs
are lazy, so <(+ 3 4),5> does not immediately evaluate to <7,5>, and
<$\Omega$,$\Omega$> is not a divergent program. The
\T{left} and \T{right} operators return the left and right components of a
pair, respectively, forcing the evaluation of those components.

After compiling the interpreter using \T{make} or \T{make.bat} you should be
able to load and run programs using the command \T{need}.  For
this assignment, you will need to modify only the file \T{translate.ml}.
Indeed, this is the only file you should modify.

To simplify the AST somewhat, we desugar multi-argument functions
into unary functions and we multi-argument primitive operations
into binary operations, arriving at a core source language:
\[
\begin{array}{rcl}
\mathit{binop} & ::= & \T{+} \mid \T{*} \mid \T{-} \mid \T{=} \mid \T{\lt} \\
\mathit{unop} & ::= & \T{zero?} \mid \T{left} \mid \T{right} \\
\mathit{refop} & ::= & (\T{ref}~e) \mid (\T{!}~e) \mid (\T{:=}~e_1~e_2) \mid (\T{seq}~e_1~e_2) \\
e & :: = & x \mid n \mid \T{true} \mid \T{false} \mid
	(\mathit{binop}~e_1~e_2) \mid
	(\mathit{unop}~e) \mid
	\mathit{refop} \mid
	(\T{if}~e_0~e_1~e_2) \\
& & \mid \T{(fn (}x \T{)}\; e\T{)}
  \mid \T{(}e_1~e_2\T{)} 
  \mid \T{(let ((}v_1\ e_1\T{))}\ e\T{)} 
 \mid <e_1,e_2>
\end{array}
\]
The core source language is just
the full source language without multi-argument functions and
applications, without most boolean operations, and without list operations.
Note that \T{let} only defines one parameter.

Our target language has the same syntax except that \emph{refop}
expressions are not permitted.  Expressions in the target language are
also evaluated call-by-value rather than call-by-name.

You should write a translator from the core source language to the target
language.  A few cases for the translator we wrote are filled in in the source
files for this problem, but you are free to do this translation any way you
wish (as long as it requires modifying only \T{translate.ml}).  To help you to
determine whether your translation is correct, we have provided both a
call-by-need interpreter and a call-by-value interpreter.  Both interpreters
are invoked by running \T{need} from the command line.

There are many possible ways to do the translation, but one way
we suggest is to do it in two phases. In the first phase, translate
the call-by-need language to call-by-value, but do not eliminate \emph{refop}
expressions.  In the second stage, translate the call-by-value language
with refs to a call-by-value language without refs.  The first phase
of the translation should be performed by the \T{Translate.to\_call\_by\_value}
function.  The second phase of the translation should be performed by
the \T{Translate.remove\_refs} function.  If you implement both phases
of the translation at once, both phases should be performed in
\T{Translate.to\_call\_by\_value} and \T{remove\_refs} should just be the
identity function.

\begin{enumerate}

\item Write a program in the source language that evaluates to a different
result in call-by-value, call-by-need, and call-by-name.  Submit your program
by email with your version of \T{translate.ml}. You'll get extra credit
if your program exposes bugs in other students' translations.

\item Implement \T{Translate.to\_call\_by\_value} in \T{translate.ml}.  This
function should translate a call-by-need input program into a call-by-value
program that produces the same result.  The most straightforward way to
perform this translation is to use refs as described above, but you are not
required to do so.

\item Implement \T{Translate.remove\_refs} in \T{translate.ml}.  This function
should remove all "Ref", "Deref", "Assign", and "Seq" nodes from the AST.  If
your \T{to\_call\_by\_value} translation already removed these nodes,
\T{remove\_refs} should be the identity function.

\end{enumerate}
\end{enumerate}
\end{document}
