\section{ADT Correctness\hfill\fbox{30 Points}}

In this question, we will consider two implementations of a
``function'' type, This is similar to the function type you used in
your first two assignments during type checking, except that we fix
the domain to be strings and the codomain integers, for the sake of
simplicity.

\begin{code}
signature FUNCTION =
sig
  type function
  val empty : function
  val add : function * (string * int)  -> function
  val lookup : function * string -> int option
end
\end{code}
The first implementation uses lists to represent functions:
\begin{code}
structure L :> FUNCTION =
struct
  type function = (string * int) list
  val empty = nil
  fun add (C, (x,e)) = (x,e)::C
  fun lookup (nil, x) = NONE
    | lookup ((h,e)::t, x) = if (x=h) then SOME(e) else lookup(t,x)
end
\end{code}
The second implementation uses SML functions to represent functions:
\begin{code}
structure F :> FUNCTION =
struct
  type function = string -> int option
  val empty = fn y => NONE
  fun add (C, (x,e)) = fn y => if (x=y) then SOME(e) else C(y)
  fun lookup(C, x) = C(x)
end
\end{code}

\clearpage
\subsection{Simulation relation\hfill\fbox{10 Points}}
We claim that these two implementations of functions are equivalent.
Fill in the definition of the simulation relation between
implementation values of type {\tt L.function} and type {\tt F.function}
started below.  (Note: There may be more than one simulation
relation that works.  If you wish, you may define the simulation
relation in a different way from the way we have suggested.)

If $s_1,\dots,s_n$ are strings and $f$ is a function from {\tt string}
to {\tt bool}, then
$$
[s_1,\dots,s_n]
\sim f\ \mbox{\bf iff}
$$
\vspace{1.5in}

\subsection{Proof of equivalence for add\hfill\fbox{10 Points}}
Give an informal proof that the {\tt add} operation preserves
the simulation relation
you just defined.  By informal, we mean that you do not have to justify
all the equivalence steps you make, so long as they are sensible.


\clearpage
\subsection{Why not be trivial?\hfill\fbox{5 Points}}
Sly Smartypants, a fellow student of yours in 15-312, wonders what's
wrong with simply defining the simulation relation to be true for
any pair of implementation values of types {\tt L.function} and
{\tt F.function}.  Good question: Why won't that work if you're trying
to prove that the {\tt L} and {\tt F} structures are equivalent?  (Limit your
answer to one or two sentences.)
\vspace{2in}

\subsection{When is triviality OK?\hfill\fbox{5 Points}}
What would it mean about an arbitrary ADT
if Sly's simulation relation could be
used to prove two implementations of that ADT equivalent?  (Limit your
answer to one or two sentences.)

\ifsoln
\clearpage
\subsection{Solution}

\begin{enumerate}
\item
$[s_1,\dots,s_n]
\sim f\ \mbox{\bf iff}
$
\begin{enumerate}
\item[1)] $f(s_i) = \mathcd{true}$ for every $i \in 1,\dots,n$.
\item[2)] $f(s) = \mathcd{false}$ otherwise.
\end{enumerate}
\item
Suppose $S=[s_1,\dots,s_n] \sim f$ and that $x$ is a string.
We will show that $\mathcd{L.add}\cdparens{S,x} \sim
\mathcd{F.add}\cdparens{f,x}$.  First, we have
$\mathcd{L.add}\cdparens{S,x} \cong [x,s_1,\dots,s_n]$
by inspecting the code.  Call this $S'$.
Then, we have $\mathcd{F.add}\cdparens{f,x}=
\mathcd{fn }y\mathcd{ => (}x\mathcd{=}y\mathcd{) orelse }f\mathcd{(}y\mathcd{)}$,
also by inspecting the code.
Call this $f'$.  $f'$ will return {\tt true} on input $y$ iff
$y$ is $x$ or $f$ returns {\tt true} on $y$.
Since $S\sim f$, we know that $f\mathcd{(}y\mathcd{)}$ will return
{\tt true} iff $y$ is any of the $s_i$.
Thus, $f'$ will return {\tt true} on $s$ iff $s$ is in the list $S'$,
and so $f'\sim S'$.
\item
It won't work because you won't be able to prove anything about
the correlation between the boolean values returned by the
two different implementations of the {\tt lookup} function.
\item
If equivalence between two implementations of an ADT could
be shown using Sly's simulation relation,
that would mean that none of the operations on the ADT returned
any values that were not abstract.
\end{enumerate}
\fi
