\problemdata                                                             
        {Finding minimal element of list} % latex-friendly label for the prob.
        {Computational Processes, Structural Induction} % The topic(s) of the problem content.  
        {?} % Source (if known)                                          
        {S01 Tutorial 3, 1} % Usage (list ones you are aware of). 
        {Tina Wang, S02} % Last revision info (author, date).   
                                                                         
                                                                         
\begin{problem}           
\newcommand{\makelist}{\mathop{\mbox{makelist}}}
\newcommand{\head}{\mathop{\mbox{head}}}
\newcommand{\tail}{\mathop{\mbox{tail}}}
\newcommand{\findMin}{\mathop{\mbox{findMin}}}
Consider the following recursive definition of the
set~$\mathcal{L}$ of lists containing real numbers:
\begin{enumerate}
\item
The empty list, $nil$, is in $\mathcal{L}$.
\item
If $t \in \mathcal{L}$, then $\forall x \in \reals$,
$\makelist(x,t) \in \mathcal{L}$.
\end{enumerate}

Conceptually, $\makelist(x,t)$ makes a new list with $x$ as its first element,
and $t$ as the rest of the list.
Two helpful list functions are
$\head()$ and $\tail()$. We define $head()$ such that
$\head(nil) = nil$ and $\head(\makelist(x,t)) = x$.  Tail is defined
as $\tail(nil) = nil$ and $\tail(\makelist(x,t)) = t$.  

Construct a recursive algorithm in terms of these functions
that finds the minimum element of a non-empty
list in~$\mathcal{L}$ and prove that the algorithm is correct. (If
there are several minimal elements, the algorithm only needs to find
one of them.)

\solution{%
%  The algorithm uses the to operators $\head$ and
%  $\tail$. Given a list~$L$, $\head(L)$ returns the first element of the
%  list and $\tail(L)$~returns the list formed by removing the first
%  element of~$L$. The empty list is denoted by~$\emptyset$.
  \begin{trivlist} \parskip=0pt \parsep=0pt
  \item Algorithm $\findMin(Y)$.
  \item\qquad \textbf{if} $\tail(Y) = nil$ \textbf{then} return $\head(Y)$,
  \item\qquad \textbf{else} return $\min\{\head(Y), \findMin(\tail(Y))\}$.
  \end{trivlist}
  Note that we do not have to check for empty lists in this algorithm,
  as we only claim that the algorithm is correct on {\em non-empty} lists.
  In a real program, you would want such a check for robustness,
  but this is not a class in real-world defensive programming techniques.

  \begin{theorem*}
    The above algorithm terminates and returns the minimum element of
    its argument when its argument is a non-empty list in $\mathcal{L}$.
  \end{theorem*}

  \begin{proof}By structural induction on $\mathcal{L}$

  {\em Base Case:}
  If $Y$ is a list of the form $\makelist(x,nil)$,
  then $x$ is the minimum (and only) element of the list. In this
  case, our algorithm returns $\head(\makelist(x,nil))$ (which is $x$).
  So in this base case,
  the algorithm terminates, returning the minimum element of the
  non-empty list argument $Y$.

  {\em Inductive Step:}
  Assume the algorithm terminates, returning the minimum element
  for a list $t$ in $\mathcal{L}$.
  Also, assume that we follow the \textbf{else} branch of the code
  since the termination and correctness of the \textbf{if} branch
  are covered in the base case.

  The minimum of a list is the lesser of its first element and
  the minimum of the rest of the list. Since (by inductive assumption), our
  algorithm terminates correctly on $t$, our algorithm also terminates
  correctly on $\makelist(x,t)$ for all $x \in \reals$ since it
  returns the smaller of $x$ and $findMin(t)$.

  The base case and inductive step prove (by structural induction)
  that on any non-empty list $Y$ in $\mathcal{L}$, our algorithm terminates and
  returns the minimum element of $Y$.
  \end{proof}
  }
\end{problem}
                                 