\documentclass[11pt, twoside]{article}

\usepackage{graphics}
\usepackage{psfig}

\input{macros-course}

%%% rjr -- I was trying to avoid these, by this is maddening...
\newcommand{\mathify}[1]{\ifmmode{#1}\else\mbox{$#1$}\fi}
\newcommand{\mquote}[1]{\mathify{\textrm{``$#1$''}}}
\newcommand{\mdash}{\mathify{\textrm{-}}}
%\newcommand{\set}[1]{\mathify{\{#1\}}}
\newcommand{\where}{{\ \scriptstyle{|} \ }}
\newcommand{\size}[1]{\mathify{\left| #1 \right|}}
\newcommand{\equivalent}{\mathify{\ \Longleftrightarrow \ }}
\newcommand{\ifandonlyif}{\equivalent}
%\newcommand{\implies}{\mathify{\ \Longrightarrow \ }}
%\newcommand{\etc}{ {\scriptstyle\ldots} }
%\newcommand{\union}{\cup}
%\newcommand{\intersect}{\cap}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Printing the page layout parameters

\printlayout

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\typein[\answer]{Include solutions? (y/n) }
\def\yes{y}
\ifx\answer\yes
  \typeout{}
  \typeout{Solutions *INCLUDED*.}
  \newcommand{\reading}[1]{}
  \newcommand{\omitsolution}[1]{ #1 }
  \newcommand{\omitnonsolution}[1]{}
  \usepackage[dark,first,bottom]{draftcopy}
  \draftcopyName{Solutions}{155}
%
  \newcommand{\handoutlabel}{sol5}
  \newcommand{\handouttitle}{Problem Set 5 Solutions}
  \newcommand{\handoutdate}{March 16, 2000}
  \newcommand{\collaboration}{}
  \newcommand{\titlebar}{%
    \handout{\handoutlabel}{\handouttitle}{\handoutdate}}
%
\else
  \typeout{}
  \typeout{Solutions *NOT INCLUDED*.}
  \newcommand{\reading}[1]{%
%    \mbox{}\\ %
    \hrule\mbox{} \\ %\bigskip %
    #1%
%    \mbox{} \\ %\bigskip %
    \hrule %
    %\vfill\mbox{}\newpage%
    }
  \newcommand{\omitsolution}[1]{}
  \newcommand{\omitnonsolution}[1]{#1}
%
  \newcommand{\handoutlabel}{ps5}
  \newcommand{\handouttitle}{Problem Set 5}
  \newcommand{\handoutdate}{March 7, 2000}
  \newcommand{\duedate}{March 14, 2000}
  \newcommand{\collaboration}{\collaborationnote}
  \newcommand{\titlebar}{%
    \handout{\handoutlabel}{\handouttitle}{\handoutdate}
    \centerline{{\bf Due  Date: \duedate.}}
    \vspace*{\baselineskip}}
%
\fi

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}


\titlebar

\reading{%
\mbox{} \\
\mbox{}\vspace*{-0.5\baselineskip}

\begin{description}\itemsep 0\baselineskip
\item[Self-study:] \mbox{} \\
Please review Rosen Section 2.6, on matrices.

Self-study problems: 3, 5, 11, 13, 15, 19, 23, 29, 30, 31

\item[Reading:] \mbox{} \\[-\baselineskip]
\vspace*{-0.5\baselineskip}
\begin{description}\itemsep 0\baselineskip
\item[Notes on Computational Processes:] \mbox{} \\ %
  Installment 3
\item[Rosen, \textit{Discrete Mathematics and Its Applications}:] \mbox{} \\ %
  Sequences and Summations: Section 1.7;
%  Generating Functions: Section 5.4;
%%%% Should that be included??
\item[6.042 Fall 97 Lecture notes (available from course page):] \mbox{} \\ %
  Lecture 8
\end{description}
%
%\begin{itemize}\itemsep 0\baselineskip
%\item Notes on Computational Processes, Installment 3.
%\item Rosen, \textit{Discrete Mathematics and Its Applications}: \mbox{} \\ %
%  Sequences and Summations: Section 1.7;
%  Generating Functions: Section 5.4;
%%%% Should that be included??
%\item 6.042 Fall 97 Lecture notes (available from course page):
%  Lecture 8
%\end{itemize}

\end{description}
}

\section*{Problems:}

\begin{problems}

%%%%%%%%%%%%%%%%%%%
%%% Problem 1

\problem 

Suppose you were about to enter college today and a college loan
officer offered you the following deal: \$25,000 at the start of each
year for four years to pay for your college tuition and an option of
choosing one of the following repayment plans:

\begin{description}\itemsep 0\baselineskip
\item[Plan A:] Wait four years, then repay \$$20,000$ at the start of
  each year for the next ten years.
\item[Plan B:] Wait five years, then repay \$$30,000$ at the start of
  each year for the next five years.
\end{description}

Suppose the annual interest rate is currently 7\% and does not change
in the future.  

\begin{itemize}\itemsep 0\baselineskip
\item[a)] Which repayment plan would you choose?

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 
  
  The use of the word `interest' above is slightly awkward. It refers to
the additional money you (or the loan officer) would make if your money
was just sitting in a bank. However, we can treat it just as we treat
inflation: $\$1$ today will be worth $\$1.07$ next year, and $\$1.07^2$ the
year after.

 Given this, set $r = \frac{1}{1.07}$. Then:
 
\begin{eqnarray*}
A & = & \sum_{y=0}^{9} 20000 \cdot r^{y+4}  \\
  & = & r^4 \cdot \sum_{y=0}^{9} 20000 \cdot r^y  \\
  & = & 20000r^4 \cdot \sum_{y=0}^{9} r^y \\
  & = & 20000r^4 \cdot \frac{1 - r^{10}}{1 - r} \\
  & = & \$114,666.69
\end{eqnarray*}

\begin{eqnarray*}
B & = & \sum_{y=0}^{4} 30000 \cdot r^{y+5}  \\
  & = & r^5 \cdot \sum_{y=0}^{4} 30000 \cdot r^y  \\
  & = & 30000r^5 \cdot \sum_{y=0}^{4} r^y \\
  & = & 30000r^5 \cdot \frac{1 - r^{5}}{1 - r} \\
  & = & \$93,840.63
\end{eqnarray*}

You should clearly take Plan B. You will be paying back much less in today's
dollars.

  \medskip

%\end{solution}
}

\item[b)] What is the loan officer's effective profit (in today's
  dollars) on the loan?

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

	The value of the money you are given is:
\begin{eqnarray*}
Loan & = & \sum_{y=0}^{3} 25000 \cdot r^{y}  \\
  & = & 25000 \cdot \sum_{y=0}^{3} r^y \\
  & = & 25000 \cdot \frac{1 - r^{4}}{1 - r} \\
  & = & \$90,607.90
\end{eqnarray*}

Therefore, the loan officer's profit is effectively $\$3,233$. (Or 
$\$24,059$ if we are not on the ball).

%\end{solution}
}

\end{itemize}

%%%%%%%%%%%%%%%%%%%
%%% Problem 2

\problem
Consider the following summation:
\[\sum_{k=2}^n {\frac{1}{k(k-1)}}\] 

\begin{problemparts}
\problempart
Find a closed form solution for this summation.

\hint Try using partial fractions to break $\frac{1}{k(k-1)}$
into a difference of two terms.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

It is easy to find that $\frac{1}{k(k-1)} = \frac{1}{k-1} - \frac{1}{k}$.
So we have:
 
\begin{eqnarray*}
\sum_{k=2}^n {\frac{1}{k(k-1)}} & = & 
\sum_{k=2}^n \left(\frac{1}{k-1} - \frac{1}{k} \right)  \\
 & = & \sum_{k=2}^n \frac{1}{k-1} - \sum_{k=2}^n\frac{1}{k}  \\
 & = & \frac{1}{1} + \frac{1}{2} + \ldots + \frac{1}{n-2} + \frac{1}{n-1} \;\; -\\
 &   & \left[ \frac{1}{2} + \frac{1}{3} + \ldots + \frac{1}{n-1} + \frac{1}{n} \right]
\end{eqnarray*}

So all that does not cancel out is $1 - \frac{1}{n}$.

%\end{solution}
}

\problempart Use induction to verify your closed form solution (i.e.,
prove that it is correct).

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

$P(n) := \left[ \sum_{k=2}^n {\frac{1}{k(k-1)}} = 1 - \frac{1}{n} \right] $

\emph{Base case:} $P(2)$ is true because the only term in the summation is
$\frac{1}{2(2-1)} = \frac{1}{2} = 1 - \frac{1}{2}$.

\emph{Inductive step:} Assuming $P(n)$, show $P(n+1)$.
\begin{eqnarray*}
\sum_{k=2}^{n+1} {\frac{1}{k(k-1)}} & = & 
\sum_{k=2}^{n} {\frac{1}{k(k-1)}} \; + \; \frac{1}{(n+1)(n)}  \\
 & = & 1 - \frac{1}{n} \; + \; \frac{1}{(n+1)(n)} 
 \;\;\;\;\;\;\;\;\;\;\;\;\;\;\textbf{IH}  \\
 & = & 1 - \frac{n+1}{(n+1)n} \; + \; \frac{1}{(n+1)(n)}  \\
 & = & 1 - \frac{n}{(n+1)n}  \\
 & = & 1 - \frac{1}{n+1}  \\
\end{eqnarray*}

 
%\end{solution}
}

\end{problemparts}


%%%%%%%%%%%%%%%%%%%
%%% Problem 3

\problem Find closed-form expressions for the following sums:

\mbox{}

\begin{problemparts}

\problempart
\vspace{-2\baselineskip}
\[
\sum_{k=0}^n \frac{8^k - 5^k}{9^k}
\]

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{eqnarray*}
\sum_{k=0}^n \frac{8^k - 5^k}{9^k} & = & 
\sum_{k=0}^n \left[ \frac{8^k}{9^k} - \frac{5^k}{9^k} \right]  \\
 & = & \sum_{k=0}^n \left[ \left(\frac{8}{9}\right)^k - \left(\frac{5}{9}\right)^k \right]  \\
 & = & \sum_{k=0}^n \left(\frac{8}{9}\right)^k - \sum_{k=0}^n \left(\frac{5}{9}\right)^k  \\
 & = & \frac{1 - \left(\frac{8}{9}\right)^{n+1}}{1 - \frac{8}{9}}  - 
       \frac{1 - \left(\frac{5}{9}\right)^{n+1}}{1 - \frac{5}{9}}  \\
 & = & \frac{1 + \frac{1}{3}\left(\frac{5}{9}\right)^{n+1} - \left(\frac{8}{9}\right)^{n+1}}{12}  \\
\end{eqnarray*}

\medskip

%\end{solution}
}


\problempart
\vspace{-2\baselineskip}
\[
\sum_{i=1}^n \sum_{j=0}^{\infty} i^{7/16} \cdot \left(1 - \frac{1}{4 i^{9/16}}\right)^j
\]

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

This sum is actually just a sum of a geometric series followed by the sum 
of an arithmetic series.

\begin{eqnarray*}
\sum_{i=1}^n \sum_{j=0}^{\infty} i^{7/16} \cdot \left(1 - \frac{1}{4 i^{9/16}}\right)^j
	& = &	\sum_{i=1}^n i^{7/16} \cdot \frac{1}{1 - \left(1 - \frac{1}{4 i^{9/16}}\right)} \\
	& = &	\sum_{i=1}^n 4i \\
	& = &	2 n (n+1)
\end{eqnarray*}

%\end{solution}
}

\end{problemparts}

%%%%%%%%%%%%%%%%%%%
%%% Problem 4

\problem

\textit{Note: This problem is only worth one point.  Give it some
  thought but don't exhaust yourself on it.}

Consider the sum of the following sequence:
\[1 - 1 + \frac{1}{2} - \frac{1}{2} + \frac{1}{3} - \frac{1}{3}
 + \frac{1}{4} - \frac{1}{4} + \frac{1}{5} - \frac{1}{5} + \ldots \]

To sum it, suppose we rearrange the terms and write it as:
\begin{eqnarray*}
 & (1 + \frac{1}{2} - 1) & +  \\
 & (\frac{1}{3} + \frac{1}{4} - \frac{1}{2}) & +  \\
 & (\frac{1}{5} + \frac{1}{6} - \frac{1}{3}) & +  \\
 & (\frac{1}{7} + \frac{1}{8} - \frac{1}{4}) & +  \\
 & \ldots & 
\end{eqnarray*}

which we can write as a summation as:
\[%
a = \sum_{n=1}^{\infty} \left( \frac{1}{2n-1} + \frac{1}{2n} - \frac{1}{n} \right) %
  = \sum_{n=1}^{\infty} \frac{1}{2n(2n-1)} %
\]

On the other hand, we arrange the original summation as
\begin{eqnarray*}
 & (1 - 1 - \frac{1}{2}) & +  \\
 & (\frac{1}{2} - \frac{1}{3} - \frac{1}{4}) & +  \\
 & (\frac{1}{3} - \frac{1}{5} - \frac{1}{6}) & +  \\
 & (\frac{1}{4} - \frac{1}{7} - \frac{1}{8}) & +  \\
 & \ldots &
\end{eqnarray*}
\[%
b = \sum_{n=1}^{\infty} \left( \frac{1}{n} - \frac{1}{2n-1} - \frac{1}{2n} \right) %
  = \sum_{n=1}^{\infty} \frac{-1}{2n(2n-1)} %
  = - a
\]

How is this possible?  Choose the correct response from the options
below. Be prepared to back up your answer.

%\begin{problemparts}
%\problempart
%I find the above somewhat disturbing, but I can't resolve it.
%\problempart
%Don't toy with me. Your petty tricks are no match for my superior mathematical skills.
%\problempart
%It's 4 am tuesday morning. I'm not even coherent enough to be disturbed.
%\end{problemparts}

\begin{itemize}
\item[\textbf{a)}] \ I find the above somewhat disturbing, but I can't
resolve it.
\item[\textbf{b)}] \ Don't toy with me. Your petty tricks are no match 
for my superior mathematical skills.
\item[\textbf{c)}] \ It's 4am Tuesday morning. I'm not even coherent enough
to be disturbed.
\end{itemize}

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

	Of course, this is a personal question. However, if you answered \textbf{c}, you
really should get started earlier -- for your own good.

	Students who answered \textbf{b} may have seen a hint it the two harmonic summations
(positive and negative) hiding within the original series.
The original summation is only \emph{conditionally} convergent. (This means that
if you sum the absolute value of the terms, 
$2 \cdot \sum_{n=1}^{\infty} \frac{1}{n}$,
the summation is not finite). With such summations, you cannot freely rearrange the 
terms. In fact, there is a theorem that says that any series that converges but does
not converge \emph{absolutely} can be rearranged to form any real number.

	It is not insightful to declare that $ a = 0 = -0$. While this is part of the
contradiction above, it is clearly not the answer. Every term in the first summation
is positive. Every term in the second summation is negative. Neither can be zero, as
a result. In fact, they are somewhere around $\pm log(2)$. Similarly, it is not
adequate to say that the sums diverge or are not well-defined. Both summations, as
well as the original zero-sum, really do converge on finite numbers. 

	Don't worry about the details here. However, you should take from this a warning
about being too loose with your math, much as you must avoid making flawed but convincing
proofs.

%\end{solution}
}


%%%%%%%%%%%%%%%%%%%
%%% Problem 5

\omitnonsolution{

\clearpage

}

\problem 
% Using a sequence to implement a set.

The following labeled state machine $\ms{DSet}$ models a ``dynamic set'' of
integers. (Remember that a set, unlike a multiset, can only contain
one element of any particular object).
The set starts out empty.

A client can modify or inspect the set by means of the following
operations:
\begin{itemize}\itemsep 0\baselineskip
\item $\mathbf{add}(x)$, \ which adds an integer $x$ to the set.
\item $\mathbf{remove}(x)$, \ which removes integer $x$ from the set.
\item $\mathbf{isin}(x)$, \ which tells if the element $x$ is in the set.
\end{itemize}

Formally, $\ms{DSet}$ can be defined as a collection of the following components: 

\begin{itemize}
\item 
$Q$: 
The states consist of the components: 
  \begin{itemize}
  \item $\ms{set}$, \ a set of integers 
  \item $\ms{reqtype} \in \set{\mquote{add}, \mquote{remove}, \mquote{isin} } \union \set{\ms{null}}$ 
  \item $\ms{element} \in \ints \union \set{ \ms{null} }$ 
  \item $\ms{retval} \in \set{\mquote{OK}, \ms{null} } \union \ms{Boolean} $
  \end{itemize}
  
\item 
$Q_0$:
Initially, $\ms{set} = \emptyset$, and all the other components are
$\ms{null}$. (Note that $\ms{null}$ is a special symbol, not the 
empty set $\emptyset$).

\item 
$L$:
  \begin{itemize}
  \item[] Input labels:
    \begin{itemize}
    \item[] $\mathbf{request\mdash add}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{request\mdash remove}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{request\mdash isin}(x)$, \ \ $x \in \ints$
    \end{itemize}

  \item[] Internal labels:
    \begin{itemize}
    \item[] $\mathbf{compute\mdash add}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{compute\mdash remove}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{compute\mdash isin}(x)$, \ \ $x \in \ints$
    \end{itemize}

  \item[] Output labels:
    \begin{itemize}
    \item[] $\mathbf{return}(\mquote{OK})$
    \item[] $\mathbf{return}(b)$, \ \ $b \in Boolean$
    \end{itemize}
  
  \end{itemize}

\item 
Transitions ($\delta$):
  \begin{itemize}
  \item[] $\mathbf{request\mdash add}(x)$ \\
if $\ms{reqtype} = \ms{null}$ then \\
  $\ms{\;\;\;\;reqtype} := \mquote{add}$ \\
  $\ms{\;\;\;\;element} := x$ 

  \item[] $\mathbf{request\mdash remove}(x)$ \\
if $\ms{reqtype} = \ms{null}$ then \\
  $\ms{\;\;\;\;reqtype} := \mquote{remove}$ \\
  $\ms{\;\;\;\;element} := x$ 

  \item[] $\mathbf{request\mdash isin}(x)$ \\
if $\ms{reqtype} = \ms{null}$ then \\ 
  $\ms{\;\;\;\;reqtype} := \mquote{isin}$ \\
  $\ms{\;\;\;\;element} := x$ 

  \item[] $\mathbf{compute\mdash add}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{add}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;set} := \ms{set} \union \set{x}$ \\
$\ms{\;\;\;\;retval} := \mquote{OK}$ 

  \item[] $\mathbf{compute\mdash remove}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{remove}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;set} := \ms{set} - \set{x}$ \\
$\ms{\;\;\;\;retval} := \mquote{OK}$ 

  \item[] $\mathbf{compute\mdash isin}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{isin}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
if $x \in \ms{set}$ then \\
$\ms{\;\;\;\;retval} := \ms{true}$ \\
else \\
$\ms{\;\;\;\;retval} := \ms{false}$

  \item[] $\mathbf{return}(\mquote{OK})$ \\
Can occur if $\ms{retval} = \mquote{OK}$ \\
%Effect: \\
$\ms{\;\;\;\;reqtype}, \ms{element}, \ms{retval} := \ms{null}$ 

  \item[] $\mathbf{return}(b)$, $b \in Boolean$ \\
Can occur if $\ms{retval} = b$ \\
%Effect: \\
$\ms{\;\;\;\;reqtype}, \ms{element}, \ms{retval} := \ms{null}$ 

  \end{itemize}

\end{itemize}
 
\begin{problemparts}

\problempart

Which of the following are valid traces of $\ms{DSet}$? For any
incorrect ones, indicate what is wrong.

%% add in candidates instead. !!!

\begin{enumerate}
\item Start with the sole element of $Q_0$.
        \begin{itemize}
        \item $\mathbf{request\mdash add}(7)$
        \item $\mathbf{return}(\mquote{OK})$
        \item $\mathbf{request\mdash isin}(7)$
        \item $\mathbf{return}(\ms{true})$
        \item $\mathbf{request\mdash remove}(7)$
        \item $\mathbf{return}(\mquote{OK})$
        \item $\mathbf{request\mdash remove}(7)$
        \item $\mathbf{return}(\mquote{OK})$
        \end{itemize}

\item Start with the sole element of $Q_0$.
        \begin{itemize}
        \item $\mathbf{request\mdash add}(7)$
        \item $\mathbf{return}(\mquote{OK})$
        \item $\mathbf{request\mdash remove}(4)$
        \item $\mathbf{return}(\ms{false})$
        \item $\mathbf{request\mdash add}(7)$
        \item $\mathbf{return}(\mquote{OK})$
        \end{itemize}

\item Start with the sole element of $Q_0$.
        \begin{itemize}
        \item $\mathbf{request\mdash add}(4)$
        \item $\mathbf{request\mdash add}(6)$
        \item $\mathbf{return}(\mquote{OK})$
        \item $\mathbf{request\mdash isin}(6)$
        \item $\mathbf{request\mdash isin}(4)$
        \item $\mathbf{return}(\ms{true})$
        \end{itemize}

\item Start with the sole element of $Q_0$.
        \begin{itemize}
        \item $\mathbf{request\mdash add}(3)$
        \item $\mathbf{request\mdash remove}(3)$
        \item $\mathbf{return}(\mquote{OK})$
        \item $\mathbf{request\mdash isin}(3)$
        \item $\mathbf{return}(\ms{false})$
        \item $\mathbf{request\mdash remove}(1)$
        \item $\mathbf{return}(\mquote{OK})$
        \end{itemize}

\end{enumerate}

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{enumerate}
\item valid
\item invalid -- remove computations always set the return value to \mquote{OK},
	whether or not the element was really removed.
\item invalid -- the second add request would have been ignored, so the check
	for 6 should return false.
\item invalid -- similarly, the first remove request would have been ignored, 
	since the add request is still `pending' ($reqtype$ is not $null$).
\end{enumerate}

Note that it is not enough to imagine one execution that would not produce
such a trace. A trace is possible if \emph{any} execution allowed by the 
rules of the transitions would produce that trace.
%\end{solution}
}

\problempart

\textbf{High-level implementation:}

One way to implement $\ms{DSet}$ is to represent the set by a finite
sequence of integers.  The $\mathbf{add}$ operation could append the new
element to the end of the sequence \emph{whether or not it already
appears in the sequence}.  The $\mathbf{isin}$ operation returns the
answer to whether or not any copy of the element is in the sequence.
The $\mathbf{remove}$ operation removes the element from the sequence at
every place that it occurs.

Define a state machine $\ms{Seq}$ corresponding to this
implementation.  In implementing the operations, you should not try to
represent individual search steps that try to locate an element in the
sequence.  Instead, let each operation perform its main computation in
one large-granularity step, which involves the entire sequence. Thus,
this description will still be rather abstract.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item 
$Q$: 
The states consist of the components: 
  \begin{itemize}
  \item $\ms{seq}$, \ a sequence (ordered) of integers 
  \item $\ms{reqtype} \in \set{\mquote{add}, \mquote{remove}, \mquote{isin} } \union \set{\ms{null}}$ 
  \item $\ms{element} \in \ints \union \set{ \ms{null} }$ 
  \item $\ms{retval} \in \set{\mquote{OK}, \ms{null} } \union \ms{Boolean} $
  \end{itemize}
  
\item 
$Q_0$:
Initially, $\ms{seq}$ has no elements, and all the other components are
$\ms{null}$.

\item 
$L$: identical to abstract case.

\item 
$\delta$: Input, output are identical to abstract case.
  \begin{itemize}
  \item[] $\mathbf{compute\mdash add}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{add}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq} := \ms{seq}$ with $x$ appended on the end \\
$\ms{\;\;\;\;retval} := \mquote{OK}$ 

  \item[] $\mathbf{compute\mdash remove}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{remove}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq} := \ms{seq}$ compressed to not include any elements equal to $x$ \\
$\ms{\;\;\;\;retval} := \mquote{OK}$ 

  \item[] $\mathbf{compute\mdash isin}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{isin}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
if $x \in \ms{seq}$ then \\
$\ms{\;\;\;\;retval} := \ms{true}$ \\
else \\
$\ms{\;\;\;\;retval} := \ms{false}$

  \end{itemize}

\end{itemize}

%\end{solution}
}


\problempart

Prove that your $\ms{Seq}$ state machine implements the $\ms{DSet}$
labeled state machine; that is, prove that any trace of $\ms{Seq}$ is
a trace of $\ms{DSet}$. Remember that a trace is a listing of only the
input and output labels during an execution -- the externally visible
behavior. You may use the Abstraction Theorem.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 


We want to show that any trace of $Seq$ is a trace of $DSet$. 
In other words, any execution $\alpha$ of $Seq$ has a corresponding
execution $\beta$ in $DSet$ that produces the same externally visible
(input and output) labels.
\[
trace(\alpha) = trace(\beta)
\]
We show this by induction on the length of $\alpha$ (the number of 
transitions in that execution). We must first strengthen our hypothesis
to include a relation between the states of $Seq$ and $DSet$ -- otherwise, 
we will not have enough to go on to do the induction. This relation is
the \emph{abstraction relation}. 

Use the relation that $reqtype$, $element$, and $retval$ are identical,
and $seq$ contains the same elements as $set$ (although they may be 
repeated in $seq$).

So, our proposition would be $P(n)$: For any execution $\alpha$ of $Seq$ 
of length $n$, there
is an execution $\beta$ of $DSet$ that has the same trace and ends with 
$reqtype$, $element$, and $retval$ in $DSet$ identical to those in $Seq$
and with the elements of $seq$ and $set$ being identical.

Given the Abstraction Theorem, we only have to show that these conditions
are preserved for any transition that $Seq$ can make.

The possible transitions of $Seq$ are:
  \begin{itemize}
  \item[] $\mathbf{request\mdash add}(x)$ \\
		Also do a $request\mdash add(x)$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
		(By the abstraction relation, we know that the $reqtype$ in
		one execution will be $null$ if and only if it is $null$ in the
		other).
  \item[] $\mathbf{request\mdash remove}(x)$ \\
		Also do a $request\mdash remove(x)$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \item[] $\mathbf{request\mdash isin}(x)$ \\
		Also do a $request\mdash isin(x)$. Nothing changes besides the
		identical alterations, and the labels generated are the same.

  \item[] $\mathbf{compute\mdash add}(x)$ \\
		Do a $compute\mdash add(x)$. While $seq$ may now have several
		copies of $x$, this is allowed by our abstraction relation.
		Otherwise, the conditions are maintained.
  \item[] $\mathbf{compute\mdash remove}(x)$ \\
		Do a $compute\mdash add(x)$. While $seq$ may have had several
		copies of $x$, all are removed by the $Seq$ transition.
  \item[] $\mathbf{compute\mdash isin}(x)$ \\
		Do a $compute\mdash isin(x)$. Will find the same result in
		both $seq$ and $set$, because the abstraction relation says
		that they have the same elements.

  \item[] $\mathbf{return}(\mquote{OK})$ \\
		Also do a $return(\mquote{OK})$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \item[] $\mathbf{return}(b)$, $b \in Boolean$ \\
		Also do a $return(b)$. Nothing changes besides the
		identical alterations, and the labels generated are the same.
  \end{itemize}

%\end{solution}
}

\problempart

\textbf{Low-level implementation:}

Give an implementation called $\ms{SeqLow}$ that relies on lower-level
operations for performing the searches and removals (operate at the
element-level).

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item 
$Q$: 
The states consist of the components: 
  \begin{itemize}
  \item $\ms{seq}$, \ a sequence (ordered) of integers $seq_0$ through $seq_n$
  \item $\ms{index} \in \nats$
  \item $\ms{offset} \in \nats$
  \item $\ms{maxindex} \in \nats$
  \item $\ms{reqtype} \in \set{\mquote{add}, \mquote{remove}, \mquote{isin} } \union \set{\ms{null}}$ 
  \item $\ms{element} \in \ints \union \set{ \ms{null} }$ 
  \item $\ms{retval} \in \set{\mquote{OK}, \ms{null} } \union \ms{Boolean} $
  \end{itemize}
  
\item 
$Q_0$:
Initially, $\ms{seq}$ has no elements, $index = 0$, $maxindex = 0$, $offset = 0$,
and all the other components are $\ms{null}$.

\item 
$L$: Input, output identical to abstract case.
  \begin{itemize}
  \item[] Internal labels:
    \begin{itemize}
    \item[] $\mathbf{compute\mdash add}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{compute\mdash remove}(x)$, \ \ $x \in \ints$
    \item[] $\mathbf{compute\mdash isin}(x)$, \ \ $x \in \ints$
    \end{itemize}
  \end{itemize}

\item 
$\delta$: Input, output are identical to abstract case.
  \begin{itemize}
  \item[] $\mathbf{compute\mdash add}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{add}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
$\ms{\;\;\;\;seq_{index}} := x$ \\
$\ms{\;\;\;\;maxindex} := maxindex + 1 $ \\
$\ms{\;\;\;\;retval} := \mquote{OK}$

  \item[] $\mathbf{compute\mdash remove}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{remove}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
if $index = maxindex$ then \\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;maxindex} := maxindex - offset$ \\
$\ms{\;\;\;\;retval} := \mquote{OK}$ \\
else if $seq_{index} = x$ then\\
$\ms{\;\;\;\;index} := index + 1$ \\
$\ms{\;\;\;\;offset} := offset + 1$ \\
else \\
$\ms{\;\;\;\;seq_{index - offset}} := seq_{index}$ \\
$\ms{\;\;\;\;index} := index + 1$ 

  \item[] $\mathbf{compute\mdash isin}(x)$ \\
Can occur if $\ms{reqtype} = \mquote{isin}$, $\ms{element} = x$, and
$\ms{retval} = \ms{null}$ \\
%Effect: \\
if $index = maxindex$ then \\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;retval} := \ms{false}$ \\
else if $seq_{index} = x$ then\\
$\ms{\;\;\;\;index} := 0$ \\
$\ms{\;\;\;\;retval} := \ms{true}$ \\
else \\
$\ms{\;\;\;\;index} := index + 1$

  \end{itemize}

\end{itemize}

%\end{solution}
}

\problempart

Give an informal argument that $\ms{SeqLow}$ implements $\ms{Seq}$.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

We must show that every sequence of $SeqLow$ is a sequence of $Seq$.
Informally, we can argue that for any execution $A$ of $SeqLow$ that 
has the same trace as an execution $B$ of $Seq$, every transition from
$A$ can be matched by some sequence of transitions from $B$. We can match
up the components of the two systems very closely. 

We take as an invariant that all like-named components in the two systems 
have the same values. $maxindex$ is one more than the largest index in the
sequence. $index$ holds the current place in the sequence that
we are examining. If $reqtype = \mquote{isin}$, then we know that there
are no elements equal to $element$ from $seq_{0}$ to $seq_{index-1}$.
If $reqtype = \mquote{remove}$, then we know that $offset$ is equal to
the number of elements that were equal to $element$ from $seq_{0}$ to 
$seq_{index-1}$, and also that all of those elements have been shifted
down to fill in. (It is actually rather difficult to express these 
constraints more formally).

Input and output transitions are exactly matched. 
  \begin{itemize}
  \item[] $\mathbf{compute\mdash add}(x)$ \\
  		Also do a $compute\mdash add(x)$. Will add the element to the
  		end in both cases.
  \item[] $\mathbf{compute\mdash remove}(x)$ \\
if $index = maxindex$ then \\
  		Also do a $compute\mdash remove(x)$. In both cases, all elements
  		that match $x$ are gone from the sequence, and the sequence is
  		that much shorter,
else if $seq_{index} = x$ then\\
		Do nothing. No observable changes; just stepping through details.
else \\
		Do nothing. No observable changes; just stepping through details.
		
  \item[] $\mathbf{compute\mdash isin}(x)$ \\
if $index = maxindex$ then \\
  		Also do a $compute\mdash isin(x)$. Will return the same value,
  		since we now know that $x$ is not equal to any $seq_{i}$ where
  		$i < maxindex$.
else if $seq_{index} = x$ then\\
  		Also do a $compute\mdash isin(x)$. Will return the same value,
  		since we know that $x$ is equal to some $seq_{i}$ (namely,
  		$i = index$).
else \\
		Do nothing. No observable changes; just stepping through details.
  \end{itemize}


%\end{solution}
}

\end{problemparts}


%%%%%%%%%%%%%%%%%%%
%%% Problem 6

\problem Consider an ``abstract object'' that maintains a dynamic
polynomial $\ms{poly}$.  This polynomial has variable $x$, and integer
coefficients.  Initially, the polynomial is just the $0$ polynomial
(no terms).  The polynomial supports operations:
\begin{itemize}
\item $\mathbf{add\mdash term}(c,e)$, which adds the term $c x^e$
  to the maintained polynomial.
\item $\mathbf{coeff}(e)$, which asks for the coefficient of the $x^e$
  term.
\end{itemize}

\begin{problemparts}

  \problempart Model this object by a labeled state machine $\ms{ADP}$.
  The state should keep track of the polynomial (a value that is
  simply a mathematical polynomial -- you don't have to think about
  how to represent it using lower-level mathematical objects like
  numbers, matrices, sequences, etc.)  The state will also need some
  bookkeeping information to keep track of operations in progress.
  The labels should include inputs reflecting the requests and outputs
  reflecting the responses.  Your machine should ignore requests that
  arrive while an operation is active.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{itemize}
\item $Q$: \\
 $ p \in \set{polynomials} $

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$\;\; \set{(0, null, null, null)} $

or, equivalently,

$\;\; p = 0$, $req = null$, $power = null$, $mult = null$

\item $L$:
    \begin{itemize}
    \item[] Input labels:
    	\begin{itemize}
    	\item[] $req\mdash add\mdash term(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $req\mdash coeff(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \item[] Output labels:
    	\begin{itemize}
    	\item[] $return(\mquote{OK})$
    	\item[] $return(c)$, \ \ $c \in \ints$
    	\end{itemize}
    \end{itemize}

\item $\delta$: \\
	Each is associated with (generates) the label of its namesake.
    \begin{enumerate}
    \item $req\mdash add\mdash term(c,e)$:  \\
    	Can occur anytime. \\
        if $req = null$ then \\
        $~\;\;\;\; req := \mquote{add}$ \\
        $~\;\;\;\; power := e$ \\
        $~\;\;\;\; mult := c$
    \item $req\mdash coeff(e)$:  \\
    	Can occur anytime. \\
        if $req = null$ then \\
        $~\;\;\;\; req := \mquote{find\mdash coeff}$ \\
        $~\;\;\;\; power := e$ \\
        $~\;\;\;\; mult := null$
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$. \\
        $~\;\;\;\; p := p + c \cdot x^e$ \\
        $~\;\;\;\; req := \mquote{OK}$
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$ and $power = e$. \\
        $~\;\;\;\; req := \textrm{coefficient of $x^e$ in $p$}$
    \item $return(\mquote{OK})$:  \\
    	Can occur if $req = \mquote{OK}$. \\
        $~\;\;\;\; req, power, mult := null$
    \item $return(c)$:  \\
    	Can occur if $req = c$. \\
        $~\;\;\;\; req, power, mult := null$
    \end{enumerate}

\end{itemize}


%\end{solution}
}

  \problempart List some (4--5) traces that are exhibited by your state
  machine $\ms{ADP}$.  Include at least one that involves a request arriving
  when it is not supposed to.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
%perhaps put explanations in on right?
req\mdash add\mdash term(1,1) & \\
return(\mquote{OK})  & \\
req\mdash add\mdash term(2,2) & \\
return(\mquote{OK})  & \\
req\mdash coeff(2)      & \\
return(2)  & \\
req\mdash add\mdash term(2,1) & \\
return(\mquote{OK})  & \\
req\mdash coeff(1)      & \\ 
return(3)  & \\
\end{array}
\]

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
req\mdash add\mdash term(1,1)  & \\
return(\mquote{OK})  & \\
req\mdash add\mdash term(2,2) & \\
req\mdash coeff(2)  & \\
return(\mquote{OK})  & \\
req\mdash coeff(2)  & \\
req\mdash add\mdash term(3,2)  & \\
return(2)  & \\
req\mdash coeff(2)  & \\
return(2)  & \\
\end{array}
\]

Start with $(0, null, null, null)$:

\[
\begin{array}{ll}
req\mdash add\mdash term(4,2) & \\
req\mdash add\mdash term(7,1)  & \\
return(\mquote{OK})  & \\
req\mdash coeff(3)  & \\
req\mdash coeff(2)  & \\
return(0)  & \\
req\mdash coeff(1)  & \\
return(0)  & \\
req\mdash coeff(2)  & \\
return(4)  & \\
\end{array}
\]

Of course, there are many more traces. The important thing about this
system is that requests will be dropped if there is still a pending
request that has not generated a $return$ -- the value of $req$ will
not be $null$ when they come in.

%\end{solution}
}

  \problempart Describe in words an implementation of your state
  machine $\ms{ADP}$.  The state of this implementation should involve
  lower-level mathematical objects like numbers, matrices, sequences,
  etc.

\omitsolution{
%\begin{solution}

% I do not really know what is adequate here!

  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] Keep an array $poly$ such that the $i$th entry holds the
coefficient of $x^i$ in $p$. The array size will have to grow as necessary,
or there will be a limit on the terms of the polynomial. 
$comp\mdash add\mdash term(c,e)$ will simply be $poly[e] := poly[e] + c$.
$comp\mdash coeff(e)$ will be $req := poly[e]$.

\item[Using Ordered Pairs: ] Keep a set $terms$ of ordered pairs $(i, c)$ 
mapping the $i$th entry to the coefficient of $x^i$ in $p$.
$comp\mdash add\mdash term(c,e)$ will be more complex, unless we just add
the pair and sum all pairs with like first components on lookup. We will 
have to search through for an existing pair with a matching first component.
This will require more internal state. $comp\mdash coeff(e)$ will be a
similar search for the right pair, returning $0$ if none is found.

\end{description}

%\end{solution}
}

  \problempart Formalize your implementation as a labeled state
  machine $\ms{Imp}$.  It should have the same external labels as your
  labeled state machine $\ms{ADP}$.

\omitsolution{
%\begin{solution}
  
  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] Assume that we ignore the bounds of the array.

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
For all (many) $i \in \nats$,  \\
$~\;\;\; poly[i] \in \ints $

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$poly[i] = 0 \textrm{for all $i$}$, $req = null$, $power = null$, $mult = null$

\item $L$: Same as before.

\item $\delta$: Same as before for input and output. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$. \\
        $~\;\;\;\; poly[e] := poly[e] + c$ \\
        $~\;\;\;\; req := \mquote{OK}$
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$ and $power = e$. \\
        $~\;\;\;\; req := poly[e]$
    \end{itemize}
\end{itemize}


\item[Using Unique Ordered Pairs: ]

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
A linked list $terms$ of the form $(i, m, next)$
with $i \in \nats$, $m \in \ints$, $next \in terms \union \set{null}$.

$firstterm \in terms$

$curterm \in terms \union \set{null}$

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$firstterm = (0, 0, null)$, $curterm = firstterm$,  $terms = \set{firstterm}$,
$req = null$, $power = null$, $mult = null$

\item $L$: Same as before for input and output labels.
    \begin{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash sum\mdash next(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash sum \mdash default(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash next(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash default(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \end{itemize}

\item $\delta$:  Input, output transitions same as before. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm \neq null$, $curterm.i = e$ \\    	
        $~\;\;\;\; curterm.m := curterm.m + c$ \\
        $~\;\;\;\; req := \mquote{OK}$ \\
        $~\;\;\;\; curterm := firstterm$
    \item $comp\mdash sum \mdash next(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm \neq null$, $curterm.i \neq e$ \\    	
        $~\;\;\;\; curterm := curterm.next $ 
    \item $comp\mdash sum \mdash default(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, $power = e$,
    	$curterm = null$ \\
        $~\;\;\;\; firstterm := (e, c, firstterm) $ \\
        $~\;\;\;\; req := \mquote{OK} $ \\
        $~\;\;\;\; curterm := firstterm$

    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, $curterm.i = e$ \\
        $~\;\;\;\; req := curterm.m$ \\
        $~\;\;\;\; curterm := firstterm$
    \item $comp\mdash coeff \mdash next(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, $curterm.i \neq e$ \\    	
        $~\;\;\;\; curterm := curterm.next $ 
    \item $comp\mdash coeff \mdash default(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm = null$ \\    	
        $~\;\;\;\; req := 0$ \\
        $~\;\;\;\; curterm := firstterm$

%    \item $return(\mquote{OK})$:  \\
%    	Can occur if $req = \mquote{OK}$. \\
%        $~\;\;\;\; req, power, mult := null$ 
%    \item $return(c)$:  \\
%    	Can occur if $req = c$. \\
%        $~\;\;\;\; req, power, mult := null$
    \end{itemize}
\end{itemize}

Note that we implicitly added a new term to $terms$ every time we
expanded the linked list.

\item[Using Multiple Ordered Pairs: ]

We need the following modifications to the abstract machine:
\begin{itemize}
\item $Q$: \\
A linked list $terms$ of the form $(i, m, next)$
with $i \in \nats$, $m \in \ints$, $next \in terms \union \set{null}$.

$firstterm \in terms$

$curterm \in terms \union \set{null}$

$total \in \ints$

$ req \in \set{\mquote{add\mdash term}, \mquote{find\mdash coeff}, null}
	\union \set{\mquote{OK}} \union \ints $

$ power \in \nats \union \set{null}  $

$ mult \in \ints \union \set{null}  $

\item $Q_0$: \\
A set with only one element:

$firstterm = (0, 0, null)$, $curterm = firstterm$,  $terms = \set{firstterm}$,
$total = 0$,
$req = null$, $power = null$, $mult = null$

\item $L$: Same as before for input and output labels.
    \begin{itemize}
    \item[] Internal labels:
    	\begin{itemize}
    	\item[] $comp\mdash sum(c,e)$, \ \ $c \in \ints, e \in \nats$
    	\item[] $comp\mdash coeff(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash next(e)$, \ \ $e \in \nats$
    	\item[] $comp\mdash coeff \mdash end(e)$, \ \ $e \in \nats$
    	\end{itemize}
    \end{itemize}

\item $\delta$:  Input, output transitions same as before. 
    \begin{itemize}
    \item $comp\mdash sum(c,e)$:  \\
    	Can occur if $req = \mquote{add\mdash term}$, $mult = c$, and $power = e$ \\
        $~\;\;\;\; firstterm := (e, c, curterm)$ \\
        $~\;\;\;\; req := \mquote{OK}$ 
    \item $comp\mdash coeff(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, and $curterm.i = e$ \\
        $~\;\;\;\; total := total + curterm.m$ \\
        $~\;\;\;\; curterm := curterm.next $
    \item $comp\mdash coeff \mdash next(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	$curterm \neq null$, and $curterm.i \neq e$ \\
        $~\;\;\;\; curterm := curterm.next $
    \item $comp\mdash coeff \mdash end(e)$:  \\
    	Can occur if $req = \mquote{find\mdash coeff}$, $power = e$,
    	and $curterm = null$ \\
        $~\;\;\;\; req := total$ \\
        $~\;\;\;\; curterm := firstterm$ \\
        $~\;\;\;\; total := 0$
%    \item $return(\mquote{OK})$:  \\
%    	Can occur if $req = \mquote{OK}$. \\
%        $~\;\;\;\; req, power, mult := null$
%    \item $return(c)$:  \\
%    	Can occur if $req = c$. \\
%        $~\;\;\;\; req, power, mult := null$
    \end{itemize}
\end{itemize}

\end{description}

%\end{solution}
}

  \problempart Argue that your implementation $\ms{Imp}$ is correct,
  in the sense that every trace of $\ms{Imp}$ is also a trace of
  $\ms{ADP}$.

\omitsolution{
%\begin{solution}

  \medskip
  \textbf{Solution:} 

\begin{description}
\item[Using Arrays: ] This is the easiest.

	The abstraction function is obvious: All corresponding elements
have the same values and for every term $cx^i$ in $p$, $poly[i] = c$.
Only the to differing transitions are nontrivial to examine.
(Otherwise, the executions are identical and the abstraction function
is clearly preserved). However, even $comp\mdash sum$ and 
$comp\mdash coeff$ are easily accounted for: if an execution of
$Imp$ is extended by either, extend an execution of $ADP$ with the
same trace using the same transition. $comp\mdash sum$ preserves the
abstraction function by performing matching arithmetic.
$comp\mdash coeff$ preserves the abstraction function because $p$
and $poly$ are in correspondence and will set $req$ to the same value.

\item[Using Unique Pairs: ] Somewhat tricky to do formally.

	The abstraction function is: elements of the same name have the 
same values; every non-zero term in $p$ has exactly one corresponding
triplet in $terms$, and every zero-coefficient term in $p$ either has
no corresponding triplet or has a triplet with a second component of
$0$.

We need other elements of an invariant:
In $Imp$, $firstterm$ begins a linked list that reaches all terms in $terms$;
there are no terms with $i = mult$ `between' $firstterm$ and
$curterm$; no two terms have the same $i$ component; if $req$ is not
\mquote{find\mdash coeff} or \mquote{add\mdash term} 
then $curterm = firstterm$.

Input and output transitions have a simple identity correspondence.
Roughly, if the last transition of the partial execution of $Imp$ is:
\begin{itemize}
   	\item[] $\mathbf{comp\mdash sum(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. Both set $req$ to
   		\mquote{OK}; the assignments keep the polynomial structures 
   		aligned. (We use the fact that the IH tells us that no other 
   		element of $terms$ represents the same exponent here). Although
   		$req$ is changed, $curterm$ is set to $firstterm$. Nothing
   		else is changed.
   	\item[] $\mathbf{comp\mdash sum\mdash next(c,e)}$ \\
   		do nothing. No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash sum \mdash default(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. If there are no
   		terms after $curterm$, and no terms with $i = mult$ between
   		$firstterm$ and $curterm$, then there must be no terms at all
   		with $i = mult$. So adding in the new term did not violate
   		uniqueness. The new $firstterm$ is connected to all of the
   		elements of $terms$ because the old $firstterm$ was.
   	\item[] $\mathbf{comp\mdash coeff(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. Must be the correct
   		coefficient because $p$ and $terms$ are in correspondence and
   		no two terms have the same $i$ component.
   	\item[] $\mathbf{comp\mdash coeff \mdash next(e)}$ \\
		do nothing.  No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash coeff \mdash default(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. If there are no
   		terms after $curterm$, and no terms with $i = mult$ between
   		$firstterm$ and $curterm$, then there must be no terms at all
   		with $i = mult$. By the correspondence between $p$ and $terms$,
   		the coefficient must be $0$ in both $ADP$ and $Imp$.
\end{itemize}

Although the steps are not filled in, the above is a basic reasoning
that traces of $Imp$ can be matched by traces of $ADP$.

\item[Using Multiple Pairs: ] Slightly trickier to do formally.

	The abstraction function is: elements of the same name have the 
same values; every term in $p$ has a coefficient equal to the sum of
$m$ in all triplets $(i, m, next)$ in $terms$ with $i$ equal to that
coefficient.

We need other elements of an invariant:
In $Imp$, $firstterm$ begins a linked list that reaches all terms in $terms$;
$total$ is the sum of $m$ in all triplets $(i, m, next)$ between 
$firstterm$ and $curterm$; if $req$ is not
\mquote{find\mdash coeff} then $curterm = firstterm$.

Input and output transitions have a simple identity correspondence.
Roughly, if the last transition of the partial execution of $Imp$ is:
\begin{itemize}
   	\item[] $\mathbf{comp\mdash sum(c,e)}$ \\
   		perform a $comp\mdash sum(c,e)$ transition. Both set $req$ to
   		\mquote{OK}. The assignments keep the polynomial structures 
   		aligned by adding in the new coefficient.
   		The new $firstterm$ is connected to all of the
   		elements of $terms$ because the old $firstterm$ was.
   		Nothing else is changed.
   	\item[] $\mathbf{comp\mdash coeff(e)}$ \\
		do nothing. $total$ is appropriately increased, since $curterm$
		is advanced beyond the term that is contributing.
   	\item[] $\mathbf{comp\mdash coeff \mdash next(e)}$ \\
		do nothing.  No data is changed, and the invariant holds over
   		the change in $curterm$ because $i \neq mult$ for the old
   		$curterm$.
   	\item[] $\mathbf{comp\mdash coeff \mdash end(e)}$ \\
   		perform a $comp\mdash coeff(e)$ transition. If there are no
   		terms after $curterm$, then all terms with $i = mult$ are between
   		$firstterm$ and $curterm$. Thus, $total$ must be the proper
   		coefficient of term $e$. Since $p$ and $terms$ are in correspondence,
   		$Imp$ and $ADP$ will update $req$ to the same value.
\end{itemize}

\end{description}
	
%\end{solution}
}

\end{problemparts}


%%%%%%%%%%%%%%%%%%%
%%% Problem 7

\problem Attached to this problem set are some students' solutions
from a previous problem set.  Mark up these solutions, indicating
things that are incorrect or unclear, and if possible show how the
solution can be made completely correct and clear.  Please refer to
the 6.042 course webpage for more readable versions of the students'
solutions.

\omitnonsolution{

\clearpage
\problempart Problem Set 4, Problem 1

\centerline{\resizebox{\textwidth}{!}{\includegraphics{figures/ps5student2.ps}}}

\clearpage%
\problempart Problem Set 4, Problem 2

\centerline{\resizebox{\textwidth}{!}{\includegraphics{figures/ps5student1.ps}}}

}

\end{problems}

\end{document}
