\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{code}
\title{Computer Science 131, Fall 2000\\
       Assignment 3: Formal Semantics}
\date{Out:  Wednesday, February 7\\[5pt]
      \textbf{Due: Wednesday, February 14, 11:00am}}
\author{}

\renewcommand{\tt}{\mathcd{tt}}
\newcommand{\ff}{\mathcd{ff}}

\newcommand{\eplus}[2]{#1 \mathcd{+} #2}
\newcommand{\etimes}[2]{#1 \mathcd{*} #2}
\newcommand{\ele}[2]{#1 \mathcd{<=} #2}
\newcommand{\eif}[3]{\mathcd{if}\ #1\ \mathcd{then}\ #2\ \mathcd{else}\ #3}
\newcommand{\elet}[3]{\mathcd{let}\ #1\ \mathcd{be}\ #2\ \mathcd{in}\ #3}
\newcommand{\eapply}[2]{#1\,#2}
\newcommand{\efix}[3]{\mathcd{fix}\ #1(#2)\ \mathcd{in}\ #3}

\newcommand{\subst}[3]{#3[#1{\to}#2]}
   
\newcommand{\estep}[2]{#1 \to #2}


\newcommand{\cassign}[2]{#1\ \mathcd{:=}\ #2}
\newcommand{\cseq}[2]{#1 \mathcd{;}\ #2}
\newcommand{\cif}[3]{\mathcd{if}\ #1\ \mathcd{then}\  
                            #2\ \mathcd{else}\ #3}
\newcommand{\cwhile}[2]{\mathcd{while}\ #1\ \mathcd{do}\ #2}
\newcommand{\cskip}{\mathcd{skip}}

\newcommand{\cstep}[4]{\langle #1,#2\rangle\to\langle #3,#4\rangle}
\newcommand{\cstop}[3]{\langle #1,#2\rangle\to #3}
\newcommand{\eeval}[3]{\langle #1,#2\rangle\Downarrow #3}

\newcommand{\wfe}[3]{#1 \vdash #2 : #3}
\newcommand{\G}{\Gamma}

\newcommand{\infrule}[2]{
  \begin{equation}
    \frac{\begin{array}{c}
              #1
          \end{array}}
         {\begin{array}{c}
              #2
          \end{array}}
  \end{equation}}



\begin{document}
\maketitle 

This assignment involves no programming.  Your written answers must be
given directly to the professor in class (or put under his office
door, 1253 Olin).  Typewritten solutions (e.g., using \LaTeX\  or
Framemaker) are strongly preferred.  You may submit handwritten work
only if it is clearly legible; \emph{the graders have been instructed
  to mark as wrong any work they have trouble reading}.

If you submit a solution after the Wednesday morning deadline, be sure to
mark it with the date and time of the handin so that the graders can 
count late days.

\section{Mini-ML (50\%)}

\begin{enumerate}
\item\textbf{Dynamic Semantics}

Show all of the state transitions required to evaluate the given
programs to value.  For each step, cite the number of the rule or
rules needed to justify that step; the rules are shown in Appendix~A.
You may use ``\cd{...}'' to
avoid recopying chunks of code that do not change from one step to
another, as long as your intent is completely clear.


\begin{enumerate}
\item 
Be careful with your substitutions!
  \begin{code}
    let x be 3 in
      let f be (fix g(y) is x+y) in
        let x be 4 in
          f(x)           
  \end{code}
\item 
  \begin{code}
    let fact be 
           fix g(y) is if y$\le$0 then 1 else y*g(y+(~1)))
    in
        fact 2
  \end{code}
\end{enumerate}

\goodbreak

\item \textbf{Static Semantics}

  The inference rules defining the mini-ML type system are shown
  in Appendix~B.  Since the pieces of code used in this
  problem have no free variables, we can unambiguously talk about the
  type(s) of these expressions; if it helps, however, you can assume
  that the typing environment $\G$ is initially empty.  
  You need not give the typing proofs for the
  first four parts.
  \begin{enumerate}
  \item What is the type of \cd{fix f(x) is x+1} ?  
  \item What types can the expression \cd{fix f(x) is x} be shown
        to have? 
  \item What types can the expression \cd{fix f(x) is f(x+1)} be shown
        to have?
  \item What types can the expression \cd{fix f(x) is f(x)} be shown
        to have?
  \item The following code evaluates to the value 3 according to the
    dynamic semantics.
    \begin{code}
      let id be (fix f(x) is x) in
          if f(true) then f(3) else f(4)
    \end{code}
    Can this be shown to have type \cd{int} 
    in the type system defined by the inference rules?  How or why not?
  \end{enumerate}

\end{enumerate}

\section{SIL: A Simple Imperative Language (50\%)}

For this problem, you will be given a formal definition of execution
for a very simple subset of a language like C.

The language is divided into \emph{expressions}, which evaluate to a
value as before, and \emph{commands} which update variables and handle
control flow.  The only command that may not be self-explanatory is the
$\cskip$ command, which has no effect when executed.  This is abstract
syntax for the empty or null command usually represented the
absence of a command, as when the C programmer writes
\cd{for (i=0; i<10; i++) ;}\ .

\[
\begin{array}{lrl}
\mbox{Values} & v ::= &n\ |\ \tt\ |\ \ff\\[5pt]
\mbox{Expressions} &e ::= &v\ |\ x\ |\ \eplus{e}{e}\ |\ \ele{e}{e}\\[5pt]
\mbox{Commands} & c ::= &\cskip\\
               &|&\cassign{x}{e}\\
               &|&\cseq{c}{c}\\
               &|&\cif{e}{c}{c}\\
               &|&\cwhile{e}{c}\\
\end{array}
\]

\begin{enumerate}
\item \textbf{Evaluation}
  
  Evaluation in this language is more complex than for mini-ML,
  because the state of the abstract machine must include the current
  values of each variable.  (This was avoided in the case of mini-ML
  by substituting away variables as soon as their values were
  determined.  This only worked because the values of a variable can
  never change.)  We do this by using what will be called a
  \emph{memory} or a \emph{store}.  An arbitrary memory will be
  denoted $M$.

Memories are simply lookup tables that associate values with variable
names.  For example, a table stating that the variable \cd{x} has
value \cd{5}, \cd{y} has value $\tt$, and \cd{z} has value $\ff$ can
be written as $(\mathcd{x}{=}\mathcd{5}, \mathcd{y}{=}\tt, \mathcd{z}{=}\ff)$.
The empty memory will be written $\emptyset$.


We don't care exactly how this lookup table is implemented; it doesn't
matter as long as we can insert and lookup variables.  (Memories are
treated as an abstract data type.)  If $M$ is a memory than we will
write $M(\mathcd{x})$ to denote the value which $M$ associates with
the variable \cd{x}.  Also, we write $M,\mathcd{x}{=}v$ to denote the 
memory that results by extening $M$ with the information that
\cd{x} is now associated the value $v$.

We can now describe the program states in the dynamic sematics: a
state is either a pair containing the command to be executed and the
current memory, or else is just a memory.  The final states are those
containing just the memory.

The rules for the dynamic semantics are shown in Appendix C.  One
complication is that we must also define the evaluation of
expressions, and the evaluation of an expression like \cd{x+1} depends
on the current memory (because you must know the current value of
\cd{x}).  The first four rules define a relation $\eeval{e}{M}{v}$, to
be read ``the expression $e$ in the memory $M$ evaluates to the value
$v$''.  This is what was called in class a ``big-step'' semantics for
expressions, because the relation is directly between the initial
expression and its final value.  Convince yourself, for example, that
$\eeval{\mathcd{x}+1}{\mathcd{x}=\mathcd{5}}{\mathcd{6}}$.  [We could
have used a small-step semantics as in mini-ML for defining expressions;
the big step semantics happens to be slightly more convenient here.]

The remaining rules define the (small-step) state transitions for commands.  For example, we have
\[
\begin{array}{rll}
&\langle \mathcd{(n := 3; if n<=5 then n:=5 else skip)}, \emptyset \rangle\\
\to&\langle \mathcd{(if n<=5 then n:=5 else skip)}, (\mathcd{n}{=}\mathcd{3}) \rangle &\mbox{(by Rules 38, 37, 32)}\\
\to&\langle \mathcd{n:=5},(\mathcd{n}{=}\mathcd{3}) \rangle
  &\mbox{(by Rules 40, 35, 33, 32)}\\
\to&(\mathcd{n}=\mathcd{5})&\mbox{(by Rules 37, 32)}\\
\end{array}
\]

Show the steps (and cite the rules justifying each step) to
completely evaluate
  \[
   \langle \mathcd{x := 0; while x<=0 do (skip; x := x+1)}, \emptyset\rangle.
  \]

\item \textbf{Concurrency}


\newcommand{\cconc}[2]{#1 \| #2}

Suppose we want to extend the language to allow multitasking, so that
evaluation can work on more than one command at once.  One way to do this
is to add a new command form $\cconc{c_1}{c_2}$, with evaluation rules
as follows:

\infrule{\cstep{c_1}{M}{c'_1}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{\cseq{c'_1}{c_2}}{M'}}

\infrule{\cstep{c_2}{M}{c'_2}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{\cseq{c_1}{c'_2}}{M'}}

\infrule{\cstop{c_1}{M}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{c_2}{M'}}

\infrule{\cstop{c_2}{M}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{c_1}{M'}}

This extention makes evaluation of commands non-deterministic; a
single state may step to several possible states.  What final states
can the following command end up in?  Briefly justify your answer.

\[
\langle\mathcd{(x:=0; x:=x+1) $\|$ (x:=3; x:=x+5)}, \emptyset\rangle
\]

\item \textbf{loop-while-repeat}

\newcommand{\lwr}[3]{\mathcd{loop}\ #1\ \mathcd{while}\ #2:\ #3\ \mathcd{repeat}}

Suppose we wanted to replace the \cd{do}-\cd{while} loop in the SIL
language with a new sort of looping construct that allows the exit test to
occur anywhere within the loop:

\[
\begin{array}{rl}
c ::= &...\\
    |&\lwr{c}{e}{c}\\
\end{array}
\]
The idea is that code like
\begin{code}
  loop 
    $c_1$ 
  while $e$  
    $c_2$ 
  repeat
\end{code}
will start by executing the command $c_1$. If $e$ then evaluates to $\ff$ the entire loop terminates.  If the expression evaluates to $\tt$, then command $c_2$ is executed and the loop starts over
again (executing $c_1$, followed by another loop test, etc.).

One nice property of this construct is that it is strictly more
general than the separate ``while'' and ``do'' loops found in
languages like C or Java.  Recall that in the concrete syntax that a
programmer would use, it is common to express the nop-command $\cskip$
with the ``empty'' command.  Then by letting $c_1$ be the empty
command we get the readable code
\begin{code}
  loop while $e$
    $c_2$
  repeat
\end{code}
which has the same behavior as the SIL command \cd{while $e$ do $c_2$}
and the C command \cd{while ($e$) $c_2$}.  Conversely, by
letting $c_2$ be the empty command we get the readable code
\begin{code}
  loop
     $c_1$
  while $e$ repeat
\end{code}
which has the behavior of the C command \cd{do $c_1$ while ($e$)}.  It
is also occasionally convenient to have the case where $c_1$ and $c_2$
are both empty.

Show some inference rule or rules which define evaluation of this
\cd{loop}-\cd{while}-\cd{repeat} construct, matching the informal
description given above.  (There are several possible formulations.)

\end{enumerate}

\clearpage
\appendix

\section{Dynamic Semantics for Mini-ML}

\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\eplus{e_1}{e_2}}{\eplus{e'_1}{e_2}}}

\infrule
   {\estep{e_2}{e'_2}}
   {\estep{\eplus{v_1}{e_2}}{\eplus{v_1}{e'_2}}}

\infrule
   {}
   {\estep{\eplus{n_1}{n_2}}{n_1{+}n_2}}

\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\etimes{e_1}{e_2}}{\etimes{e'_1}{e_2}}}

\infrule
   {\estep{e_2}{e'_2}}
   {\estep{\etimes{v_1}{e_2}}{\etimes{v_1}{e'_2}}}

\infrule
   {}
   {\estep{\etimes{n_1}{n_2}}{n_1n_2}}

\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\ele{e_1}{e_2}}{\ele{e'_1}{e_2}}}

\infrule
   {\estep{e_2}{e'_2}}
   {\estep{\ele{v_1}{e_2}}{\ele{v_1}{e'_2}}}

\infrule
   {}
   {\estep{\ele{n_1}{n_2}}{n_1\le n_2}}

\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\eif{e_1}{e_2}{e_3}}{\eif{e'_1}{e_2}{e_3}}}

\infrule
   {}
   {\estep{\eif{\tt}{e_2}{e_3}}{e_2}}

\infrule
   {}
   {\estep{\eif{\ff}{e_2}{e_3}}{e_3}}


\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\elet{x}{e_1}{e_2}}{\elet{x}{e'_1}{e_2}}}

\infrule
   {}
   {\estep{\elet{x}{v_1}{e_2}}{\subst{x}{v_1}{e_2}}}


\infrule
   {\estep{e_1}{e'_1}}
   {\estep{\eapply{e_1}{e_2}}{\eapply{e'_1}{e_2}}}

\infrule
   {\estep{e_2}{e'_2}}
   {\estep{\eapply{v_1}{e_2}}{\eapply{v_1}{e'_2}}}

\infrule
   {\estep{e_2}{e'_2}}
   {\estep{\eapply{(\efix{f}{x}{e})}{v}}{\subst{f}{(\efix{f}{x}{e})}{(\subst{x}{v}{e})}}}


\clearpage
\section{Static Semantics for Mini-ML}

\infrule{}
        {\wfe{\G}{n}{\mathcd{int}}}

\infrule{}
        {\wfe{\G}{\tt}{\mathcd{bool}}}

\infrule{}
        {\wfe{\G}{\ff}{\mathcd{bool}}}

\infrule{\wfe{\G}{e_1}{\mathcd{int}}
         \qquad
         \wfe{\G}{e_2}{\mathcd{int}}}
        {\wfe{\G}{\eplus{e_1}{e_2}}{\mathcd{int}}}

\infrule{\wfe{\G}{e_1}{\mathcd{int}}
         \qquad
         \wfe{\G}{e_2}{\mathcd{int}}}
        {\wfe{\G}{\etimes{e_1}{e_2}}{\mathcd{int}}}

\infrule{\wfe{\G}{e_1}{\mathcd{int}}
         \qquad
         \wfe{\G}{e_2}{\mathcd{int}}}
        {\wfe{\G}{\ele{e_1}{e_2}}{\mathcd{bool}}}

\infrule{\wfe{\G}{e_1}{\mathcd{bool}}
         \qquad
         \wfe{\G}{e_2}{t}
         \qquad
         \wfe{\G}{e_3}{t}}
        {\wfe{\G}{\eif{e_1}{e_2}{e_3}}{t}}

\infrule{}
        {\wfe{\G}{x}{\G(x)}}

\infrule{\wfe{\G}{e_1}{t_1}
         \qquad
         \wfe{\G,x{:}t_1}{e_2}{t_2}}
        {\wfe{\G}{\elet{x}{e_1}{e_2}}{t_2}}

\infrule{\wfe{\G,f{:}t_1{\to}t_2,x{:}t_1}{e}{t_2}}
        {\wfe{\G}{\efix{f}{x}{e}}{t_1{\to}t_2}}

\clearpage
\section{Dynamic Semantics for SIL}

\infrule{}
        {\eeval{v}{M}{v}}

\infrule{}
        {\eeval{x}{M}{M(x)}}

\infrule{\eeval{e_1}{M}{n_1}\qquad\eeval{e_2}{M}{n_2}}
        {\eeval{\eplus{e_1}{e_2}}{M}{n_1{+}n_2}}

\infrule{\eeval{e_1}{M}{n_1}\qquad\eeval{e_2}{M}{n_2}}
        {\eeval{\ele{e_1}{e_2}}{M}{n_1{\le}n_2}}

\infrule{}
        {\cstop{\cskip}{M}{M}}

\infrule{\eeval{e}{M}{v}}
        {\cstop{\cassign{x}{e}}{M}{(M,x{=}v)}}

\infrule{\cstep{c_1}{M}{c'_1}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{\cseq{c'_1}{c_2}}{M'}}

\infrule{\cstop{c_1}{M}{M'}}
        {\cstep{(\cseq{c_1}{c_2})}{M}{c_2}{M'}}

\infrule{\eeval{e}{M}{\tt}}
        {\cstep{\cif{e}{c_1}{c_2}}{M}{c_1}{M}}

\infrule{\eeval{e}{M}{\ff}}
        {\cstep{\cif{e}{c_1}{c_2}}{M}{c_2}{M}}

\infrule{\eeval{e}{M}{\tt}}
        {\cstep{\cwhile{e}{c}}{M}{(\cseq{c}{\cwhile{e}{c}})}{M}}

\infrule{\eeval{e}{M}{\ff}}
        {\cstop{\cwhile{e}{c}}{M}{M}}

\end{document}