ch09.tex

\chapter{Sorting}
\label{ch:sorting}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End:

The task of sorting records into a desired order
(alphabetical order, for example, or chronological order,
or numeric order by an identifying key)
is one of the most studied problems in computing.
Solutions abound,
and a good one can save an enormous amount of time.
A sorting operator that is twice as fast
as a slower operator when rearranging a few hundred records
will typically be many times faster than the slow operator
for thousands of records and thousands of times faster
when there are millions of records to be arranged.
Data archives with thousands or millions of records
are common, and that makes the sorting process important.\footnote{The
difference between using a fast sorting operator and a slow one
can be dramatic.
\index{sorting!bubble sort vs quicksort}\label{bubble-vs-quicksort-example}Some
years ago, one of the authors helped the US Forest Service
figure out why their central computing system
was bogged down.
The culprit turned out to be about two dozen lines
of code in their road design system.
Those lines defined a slow sorting method
known as bubble sort. Replacing it with a fast sorting
method known as quicksort cut the amount of computation
attributable to the road design system from over a hundred
hours a week on each of eight mainframe computers to a few hours
a week on one.}

This chapter will discuss two sorting operators that
deliver the same results but differ
greatly in the amount of time they take to do the job.
Since they deliver the same results,
they are equivalent operators in a mathematical sense,
but they are vastly different computationally.
We will discuss both the computational differences
and the \index{operators, equivalence of}
\index{equivalence!of operators}mathematical equivalence.

Deriving the resource requirements of an operator from
the equations that define it is
similar to deriving other properties.
Previously, we have been mostly concerned with meeting
expectations with regard to the form of the results
of an operation, not the time it takes to deliver those results.
Now we will discuss engineering choices that affect the usefulness of
software as the amount of data increases.
Engineering requires not only producing the expected
results but also dealing with scale in effective ways.

\section{Insertion-Sort}
\label{sec:insertion-sort}

To focus our attention on the essentials of
arranging records in order by a key, we will
assume that the entire content of a record
resides in its key.
In practice, there is usually a lot of information
in a record, not just an identifying key,
but the process of arranging the records
in order by key is the same, regardless
of what information is associated with each key.
To simplify the discussion,
we will use numbers for keys
and discuss operators that rearrange lists
of numbers into increasing order.
For example, if the operand of the sorting
operator were the list \textsf{[5 9 4 6 5 2]},
the operator would deliver the list \textsf{[2 4 5 5 6 9]},
which contains the same numbers, but arranged so
that the smallest one comes first, increasing up the
line to the largest at the end.

In practice, keys need not be numbers,
but they do need to be comparable
to determine an ordering (alphabetical, chronological, and so on).
If the keys aren't numbers,
then the numeric comparisons
($<$, $>$) in our discussion would be replaced by
other operators designed to compare
keys to see which one precedes the other
in the desired ordering.
The sorting method is the same, regardless
of how keys are compared.

Suppose someone has defined an operator that,
given a list of numbers that has
already been arranged into increasing order,
along with a new number to put in the list,
delivers a list with the new number inserted
in a place that preserves the ordering.
If we call the operator \textsf{insert}, then
the formula \textsf{(insert 8 [2 4 5 5 6 9])} would
deliver \textsf{[2 4 5 5 6 8 9]}.

What are some equations that we would expect
the \textsf{insert} operator to satisfy?
If the list were empty, then the operator
would deliver a list whose only element would
be the number
\index{equation, by name!\{ins0\}, \{ins1\}, \{ins2\}}\index{axiom, by name!\{ins0\}, \{ins1\}, \{ins2\}}to be inserted in the list.
\vspace{2mm}\\
%\begin{quote}
\hspace*{5mm}\textsf{(insert $x$ nil) $=$ (cons $x$ nil)} ~~~~ \{\emph{ins0}\}
\vspace{2mm}
%\end{quote}

If the number to be inserted is less than or equal to the
first number in the list, the operator could simply
insert the number at the beginning of the list.
\vspace{2mm}\\
%\begin{quote}
\hspace*{5mm}\textsf{(insert $x$ (cons $x_1$ $xs$)) $=$ (cons $x$ (cons $x_1$ $xs$))} if $x \le x_1$ ~~~~\{\emph{ins1}\}
\vspace{2mm}
%\end{quote}

If the number to be inserted is greater than the first number
in the list, we don't know where it will go in the list,
but we do know it won't come first.
The first number in the list will still be the first number
after the new one is inserted somewhere down the line.
If we trust the operator to put it in the right place,
we can make a new list starting with the same first number
and then  let the insertion operator put the new number
where it belongs among the numbers after the first one.
That leads to an inductive equation for the operator
\index{axiom, by name!\{ins0\}, \{ins1\}, \{ins2\}}\index{equation, by name!\{ins0\}, \{ins1\}, \{ins2\}}\textsf{insert}.
\vspace{2mm}\\
%\begin{quote}
\hspace*{5mm}\textsf{(insert $x$ (cons $x_1$ $xs$)) $=$ (cons $x_1$ (insert $x$ $xs$))} if $x > x_1$ ~~~~ \{\emph{ins2}\}
\vspace{2mm}
%\end{quote}

The equations \{\emph{ins0}\}, \{\emph{ins1}\}, and \{\emph{ins2}\}
are comprehensive, consistent, and computational,
so they define the operator \textsf{insert}
(three C's, figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}).
The following definition in ACL2 transliterates the three equations
but consolidates \{\emph{ins0}\} and \{\emph{ins1}\} into one equation
by observing that the right-hand sides of both equations
are the same formula: \textsf{(cons $x$ $s$)}, where $s$ is the second operand
on the left-hand side
(which is \textsf{nil} in equation \{\emph{ins0}\} and
\textsf{(cons $x_1$ $xs$)} in equation \{\emph{ins1}\}).

\label{defun:insert-isort}\index{axiom, by name!\{ins0\}, \{ins1\}, \{ins2\}}\index{equation, by name!\{ins0\}, \{ins1\}, \{ins2\}}
\index{operator, by name!insert (in order)}\seeonlyindex{insert, in order}{operator}
\index{sorting!insert (in order)}
\begin{code}
\begin{verbatim}
(defun insert (x xs) ; assume x1 <= x2 <= x3 ...
  (if (and (consp xs) (> x (first xs)))
      (cons (first xs) (insert x (rest xs))) ; {ins2}
      (cons x xs)))                          ; {ins1}
\end{verbatim}
\end{code}

Now suppose someone has defined a sorting operator called \textsf{isort}
(insertion-sort).
Empty lists and one-element lists already have their
elements in order, by default.
Therefore, the formula \textsf{(isort nil}) would deliver \textsf{nil}
and the formula \textsf{(isort (cons $x$ nil))} would deliver
\textsf{(cons $x$ nil)}.
That is, \textsf{(isort $xs$) $=$ $xs$} when $xs$ has one element or none.

\begin{center}
\label{eq:isrt0}\label{eq:isrt1}
\index{equation, by name!\{isrt0\}, \{isrt1\}, \{isrt2\}}\index{axiom, by name!\{ins0\}, \{ins1\}, \{ins2\}}
\begin{tabular}{ll}
\textsf{(isort nil) $=$ nil}                       & \{\emph{isrt0}\} \\
\textsf{(isort (cons $x$ nil)) $=$ (cons $x$ nil)} & \{\emph{isrt1}\} \\
\end{tabular}
\end{center}

If the list to be sorted has two or more elements,
it has the form \textsf{(cons $x_1$ (cons $x_2$ $xs$))}
(\{consp\} axiom, page \pageref{consp-axiom}).
If the \textsf{isort} operator works properly,
the formula \textsf{(isort (cons $x_2$ $xs$))} would be
a list made up of the number $x_2$ and all the numbers in the list $xs$
taken together and
arranged in increasing order.
Given that list, the \textsf{insert} operator can put the number $x_1$ in
the right place, producing a list made up of all the
numbers in the original list rearranged into increasing order.

\begin{center}
\label{eq:isrt2}
\begin{tabular}{ll}
\textsf{(isort(cons $x_1$ (cons $x_2$ $xs$))) $=$ (insert $x_1$ (isort(cons $x_2$ $xs$)))} & \{\emph{isrt2}\} \\
\end{tabular}
\end{center}

The equations \{\emph{isrt0}\}, \{\emph{isrt1}\}, and \{\emph{isrt2}\}
are comprehensive (the operand is either empty, has one element, or
has more than one element) and consistent (no overlapping cases).
They are computational because the operand of \textsf{isort}
on the right-hand side of the inductive equation
\{\emph{isrt2}\}, namely \textsf{(cons $x_2$ $xs$)},
has fewer elements than the operand on the left-hand side,
which is \textsf{(cons $x_1$ (cons $x_2$ $xs$))}.
Therefore, the operand on the right-hand side is
closer than the operand on the left-hand side to a list
of the form \textsf{(cons $x$ nil)}, which is
the operand on the left-hand side of the
noninductive equation \{\emph{isrt1}\}.
Therefore, the equations satisfy the three C's requirements %'
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}),
which means that they define the operator \textsf{isort}.
The three equations can be consolidated into two because
\{\emph{isrt0}\} and \{\emph{isrt1}\}
are both the same equation: \textsf{(isort $xs$)} $=$ $xs$,
where $xs$ is \textsf{nil} in equation \{\emph{isrt0}\}
and \textsf{(cons $x$ nil)} in equation \{\emph{isrt1}\}.

\label{defun:isort}\index{axiom, by name!\{isrt0\}, \{isrt1\}, \{isrt2\}}\index{equation, by name!\{isrt0\}, \{isrt1\}, \{isrt2\}}\index{operator, by name!isort (insertion-sort)}\seeonlyindex{isort}{operator}\index{insertion-sort}\index{sorting!insertion-sort (isort)}
\begin{code}
\begin{verbatim}
(defun isort (xs)
  (if (consp (rest xs)) ; xs has 2 or more elements?
      (insert (first xs) (isort (rest xs))) ; {isrt2}
      xs))              ; (len xs) <= 1     ; {isrt1}
\end{verbatim}
\end{code}

We expect the insertion-sort operator to preserve
the number of elements in its operand and to
neither add nor drop values from the list.
Theorems stating these properties would be
similar to the corresponding theorems for
the multiplex and demultiplex operators discussed
in chapter \ref{ch:mux-dmx}.
The theorem on preservation of values is
stated as a
\index{Boolean!equivalence ($\leftrightarrow$, iff)}\index{operator, by name!iff (Boolean equivalence)}\index{operator, logic!Boolean equivalence ($\leftrightarrow$, iff)}\index{equivalence!Boolean ($\leftrightarrow$, iff)}\index{iff (\emph{see also} operator)}Boolean
equivalence
and uses the \textsf{occurs-in }predicate
(box \ref{aside:mux-val-thm}, page \pageref{aside:mux-val-thm}) %(page \pageref{def:occurs-in})
for determining
whether or not a value occurs in a list
(box~\ref{aside:mux-val-thm}, page \pageref{aside:mux-val-thm}, and
exercise \ref{ex:mul-val-thm}, page \pageref{ex:mul-val-thm}).\footnote{Preservation
of length and values does not guarantee
that the operator delivers the correct result.
For example, the lists \textsf{[1 1 2]} and \textsf{[1 2 2]} have the
same length and the same values
but \textsf{(isort [1 1 2]) $\neq$ [1 2 2]}.
The sorted list must be a permutation of the original list.
The permutation property is not much harder
to prove than length and value preservation,
but it does require a definition of permutation
(exercise~\ref{ex:permp-isort}, page~\pageref{ex:permp-isort}).}

\label{defthm:isort-len}
\label{defthm:isort-val}
\index{theorem, by name!\{isort-len\}, \{isort-ord\}, \{isort-val\}}
\begin{code}
\begin{verbatim}
(defthm isort-len-thm
  (= (len (isort xs)) (len xs)))

(defthm isort-val-thm
  (iff (occurs-in e xs)
       (occurs-in e (isort xs))))
\end{verbatim}
\end{code}

We also expect the numbers in the list
that the \textsf{isort} operator
delivers to be in increasing order.
To state that property, we need a predicate
to distinguish between lists containing numbers in increasing order
and lists that have some numbers out of order.
A list with only one element or none is automatically in order.
A list with two or more elements is in order
if its first element doesn't exceed its second and if
all the elements after the first element are in order.
These observations lead to the following
ACL2 definition of a predicate \textsf{up},
which is true when its operand is a list
of numbers that is in increasing order and false otherwise:

%%%\hspace{1cm} (up(cons $x_1$ (cons $x2$ $xs$))) = ($x_1 \le x_2$) $\wedge$ (up(cons $x_2$ $xs$))
%%%\hfill \{\emph{up2}\}
\index{compare!numbers ($<$, $<=$, $=$, $>=$, $>$)}
\index{predicate!numeric order ($<$, $<=$, $=$, $>=$, $>$)}
\index{order!numeric ($<$, $<=$, $=$, $>=$, $>$)}
\index{operator!numeric order ($<$, $<=$, $=$, $>=$, $>$)}
\index{number!order ($<$, $<=$, $=$, $>=$, $>$)}
\seeonlyindex{less or equal ($<=$)}{predicate}
\label{defun:up}
\index{operator, by name!up (\emph{see} predicate)}
\index{predicate, by name!up (increasing order)}
\seeonlyindex{up (increasing order)}{predicate}
\begin{code}
\begin{verbatim}
(defun up (xs)     ; (up[x1 x2 x3 ...]): x1 <= x2 <= x3 ...
  (or (not (consp (rest xs)))          ; (len xs) <= 1
      (and (<= (first xs) (second xs)) ; x1 <= x2
           (up (rest xs)))))           ; x2 <= x3 <= x4 ...
\end{verbatim}
\end{code}

Our expectations about ordering in the list that the \textsf{isort} operator
delivers can be expressed formally in ACL2 in terms of the \textsf{up} predicate.
ACL2 succeeds without assistance in proving
all three properties: length preservation,
value preservation, and ordering.
The proof can induct on the length
of the list supplied as the operand of \textsf{isort}.

\label{defthm:isort-ord-thm}
\index{sorting!insertion-sort (isort)}\index{theorem!insertion-sort (isort)}
\index{theorem, by name!\{isort-len\}, \{isort-ord\}, \{isort-val\}}
\begin{code}
\begin{verbatim}
(defthm isort-ord-thm
  (up (isort xs)))
\end{verbatim}
\end{code}

Later, we will analyze the computational behavior of the \textsf{isort} operator
and will find that it is extremely slow for long lists.
The next section begins a discussion of a sorting operator
that is fast, even on long lists.

\begin{exercises}
\exer {Do a paper-and-pencil proof that the \textsf{isort} operator
preserves the values in its operand
(\textsf{isort-val-thm}, above).}%page \pageref{defthm:isort-val}).}

\exer {Do a paper-and-pencil proof that the \textsf{isort} operator
preserves the length of its operand
(\textsf{isort-len-thm}, page \pageref{defthm:isort-len}).
You may assume theorem \{\emph{insert-len}\}: \textsf{(len(insert $x$ $xs$)) $=$ $1$ $+$ (len xs)}.}

\exer {Do a paper-and-pencil proof that the \textsf{isort} operator
delivers a list arranged in increasing order
(\textsf{isort-ord-thm}, page \pageref{defthm:isort-ord-thm}).}

\exer {\label{ex:ct}%
Suppose \textsf{(ct $x$ $xs$)} delivers a count
equal to the number of times
the value $x$ occurs in the list $xs$.
\subexer {What value should the operator \textsf{ct} deliver if $xs$ has no elements?}
\subexer {State a theorem in ACL2 that expresses the
      number of occurrences of a value $x$ in the list \textsf{(cons $x$ $xs$)}
      in terms of the number of occurrences of $x$ in $xs$.}
\subexer {State a theorem in ACL2 that expresses the
      number of occurrences of a value $x$ in the list \textsf{(cons $y$ $xs$)}
      when $y$ is not equal to $x$.}
\subexer {Use the above observations to define the operator \textsf{ct}.}
}
\begin{code}
\begin{verbatim}
(defun ct (x xs) ; number of occurrences of x in xs
   ...)
\end{verbatim}
\end{code}

\exer {The \index{operator, by name!del (delete list element)}
\seeonlyindex{del (delete list element)}{operator}\textsf{del} operator
deletes an occurrence of $x$ in $xs$
if $x$ occurs in $xs$.
\label{defun:del}}
\begin{code}
\begin{verbatim}
(defun del (x xs)
   (if (not(consp xs))
       nil
       (if (equal x (first xs))
           (rest xs)
           (cons (first xs) (del x (rest xs))))))
\end{verbatim}
\end{code}
\begin{quote}
Define a theorem in ACL2 that
expresses the number of occurrences of $x$ in \textsf{(del $x$ $xs$)}
in terms of the number of occurrences of $x$ in $xs$.
Refer to the operator \textsf{ct} (exercise~\ref{ex:ct}).\\
\emph{Hint}: Be careful to take into account the possibility that
$x$ does not occur in $xs$.
\end{quote}

\exer {\label{ex:permp-isort}%
The predicate
\index{predicate, by name!permp (permutation)}\index{operator, by name!permp (\emph{see} predicate)}\seeonlyindex{permp}{predicate}\textsf{permp},
defined as follows, is true if its second operand
is a permutation of its first operand and false otherwise:\footnote{The
predicate \textsf{occurs-in} is defined in
box~\ref{aside:mux-val-thm} (page \pageref{aside:mux-val-thm}).}}
\label{defun:permp}
\begin{code}
\begin{verbatim}
(defun permp (xs ys)
   (if (not(consp xs))
       (not(consp ys))
       (and (occurs-in (first xs) ys)
            (permp (rest xs) (del (first xs) ys)))))
\end{verbatim}
\end{code}
\begin{quote}
Define a theorem in ACL2 stating that \textsf{(isort $xs$)} is a
permutation of $xs$, and
get ACL2 to prove the theorem.
Since the theorem will refer to the predicate \textsf{permp}
and \textsf{permp} refers to the operators \textsf{occurs-in} and \textsf{del},
ACL2 will need to admit definitions of those operators
to its logic before it can attempt to prove the theorem.
\end{quote}

\end{exercises}

\section{Order-Preserving Merge}
\label{sec:mrg}

The multiplex operator (\textsf{mux}, section \ref{sec:mux})
combines two lists into one in a perfect shuffle.
The merge operator is another way to combine lists.
It combines ordered lists
in a way that preserves order.
If both lists contain numbers arranged in increasing order,
the merge operator \textsf{mrg}
will combine the two lists
into one in which all of the elements from both lists
are arranged in increasing order.
Two of the equations for \textsf{mrg}
specify the results when one of the lists is empty.
The equations for \textsf{mrg} in those cases are the same as
the corresponding equations for the multiplex operator
(\{\emph{mux0x}\} and \{\emph{mux0y}\}, page \pageref{def:mux}).

\begin{center}\index{equation, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}\index{axiom, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}
\begin{tabular}{ll}
\textsf{(mrg nil $ys$) $=$ $ys$} & \{\emph{mg0}\} \\
\textsf{(mrg $xs$ nil) $=$ $xs$} & \{\emph{mg1}\} \\
\end{tabular}
\end{center}

When both lists are nonempty, the merged list will
start with either the first element of the first operand
or the first element of the second operand,
depending on which is smaller.
The remaining elements in the merged list come from
merging what's left of the list whose first element is smaller
with all of the elements in the other list.
That divides the nonempty case into two
subcases, one when the first operand starts with a smaller number
than the second operand
and the other when the second operand begins with the smaller number.

\begin{center}\index{equation, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}\index{axiom, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}
\begin{tabular}{ll}
\textsf{(mrg (cons $x$ $xs$) (cons $y$ $ys$)) $=$ (cons $x$ (mrg $xs$ (cons $y$ $ys$)))} if $x \le y$ & \{\emph{mgx}\} \\
\textsf{(mrg (cons $x$ $xs$) (cons $y$ $ys$)) $=$ (cons $y$ (mrg (cons $x$ $xs$) $ys$))} if $x > y$   & \{\emph{mgy}\} \\
\end{tabular}
\end{center}

The four equations, taken as a whole, are comprehensive
because either one list is empty or the other one is empty
or both lists are nonempty,
in which case the first element of one of them
is less than or equal to the first element of the other.
They are consistent because, as with the \textsf{mux} operator,
the only overlapping situation is when
both lists are empty, in which case equation \{\emph{mg0}\}
delivers the same result as equation \{\emph{mg1}\}.

Two of the equations (\{\emph{mgx}\} and \{\emph{mgy}\}) are inductive,
so we need to make sure they are computational.
In both equations, there are fewer elements in the operands
on the right-hand side than on the left-hand side.
That is, the total number of elements to be merged
on the right-hand side of the inductive equation \{\emph{mgx}\}
is less than the total on the left-hand side.
That makes the operands on the right-hand side closer to
a noninductive case than the operands on the left-hand side.
Therefore, the equations are computational.
That covers the three C's
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}),
so we can take the equations as axioms that define the \textsf{mrg} operator.

A formal definition in ACL2 can be constructed from
the equations \{\emph{mg0}\}, \{\emph{mg1}\}, \{\emph{mgx}\}, and \{\emph{mgy}\}.
However, ACL2 needs some help in finding an induction scheme
to prove that the equations lead to a terminating computation.
We reasoned that the merge equations are computational
because the total number of elements in the two operands
is smaller on the right-hand side of the inductive equations
than on the left-hand side.
The \textsf{declare} directive in the following ACL2 definition suggests
basing the proof by induction on this total,
and that suggestion is enough to get the mechanized logic on the right track.

\begin{code}\label{defun:mrg}\index{axiom, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}\index{equation, by name!\{mg0\}, \{mg1\}, \{mgx\}, \{mgy\}}\index{operator, by name!mrg (ordered merge)}\seeonlyindex{mrg (ordered merge)}{operator}\index{sorting!merge, ordered (mrg)}\index{merge, ordered (mrg)}\index{defun!induction hint}\index{definition!defun hint}\index{directive!induction hint}
\begin{verbatim}
(defun mrg (xs ys)
  (declare (xargs :measure (+ (len xs) (len ys)))); induction scheme
  (if (and (consp xs) (consp ys))
      (let* ((x (first xs)) (y (first ys)))
        (if (<= x y)
            (cons x (mrg (rest xs) ys))   ; {mgx}
            (cons y (mrg xs (rest ys))))) ; {mgy}
      (if (not (consp ys))
          xs     ; ys is empty            ; {mg0}
          ys)))  ; xs is empty            ; {mg1}
\end{verbatim}
\end{code}

The \textsf{mrg} operator preserves the total length of its operands,
and it neither adds nor drops any of the values in those operands.
The equations specifying these properties are like those of the
corresponding properties of the \textsf{mux} operator, namely,
the mux-length theorem (page \pageref{mux-length-thm}) and the
mux-val theorem (page \pageref{thm:mux-val}).\footnote{As
with the theorems about
\textsf{mux}, \textsf{dmx}, and \textsf{isort}, length and value preservation
do not guarantee that \textsf{mrg} delivers a correct result.
The result must be a permutation
of the elements of the lists to be merged,
which is a more restrictive property than
preservation of length and values
(see exercise~\ref{ex:permp-isort}, page~\pageref{ex:permp-isort}).}

The \textsf{mrg} operator also preserves order.
If the numbers in both operands are in increasing order,
the numbers in the list it delivers are in increasing order.
A formal statement of this property can employ the same order predicate
(\textsf{up}, page \pageref{defun:up}) that was used to specify a
similar property of the \textsf{isort} operator.
However, in the case of the \textsf{mrg} operator,
the property is guaranteed only under the condition
that both operands are already in order,
so the property is stated as an implication.
\label{defthm:mrg-ord}\index{theorem, by name!\{mrg-length\}, \{mrg-ord\}, \{mrg-val\}}
\index{theorem!merge, ordered}
\begin{code}
\begin{verbatim}
(defthm mrg-ord-thm
  (implies (and (up xs) (up ys))
           (up (mrg xs ys))))
\end{verbatim}
\end{code}

ACL2 can verify this property without assistance.
The induction scheme for proving that
the \textsf{mrg} operator terminates,
namely, induction on the total number of elements in the operands,
also works in the proof of the merge order theorem.
A paper-and-pencil proof could follow the same strategy.

\begin{exercises}
\exer {\label{ex:mrg-length-thm}%
\index{theorem, by name!\{mrg-length\}, \{mrg-ord\}, \{mrg-val\}}Using the mux-length theorem (page \pageref{mux-length-thm})
as a model, make a formal ACL2 statement of the mrg-length theorem.}

\exer {Do a paper-and-pencil proof of the mrg-length theorem
of exercise \ref{ex:mrg-length-thm}.}

\exer {\label{ex:mrg-ord-thm}%
Do a paper-and-pencil proof of \textsf{mrg-ord-thm} (see \textsf{defthm}, above).}%(page \pageref{defthm:mrg-ord}).}

\exer {\label{ex:mrg-val-thm}%
\index{theorem, by name!\{mrg-length\}, \{mrg-ord\}, \{mrg-val\}}Using the mux-val theorem (page \pageref{thm:mux-val})
as a model, make a formal ACL2 statement of the mrg-val theorem.}

\exer {Do a paper-and-pencil proof of the mrg-val theorem of exercise \ref{ex:mrg-val-thm}.}
\end{exercises}

\section{Merge-Sort}
\label{sec:msort}

We can use the \textsf{mrg} operator (page \pageref{defun:mrg}),
together with the demultiplexer (\textsf{dmx}, page \pageref{dmx-defun}),
to define a sorting operator \textsf{msort} (merge-sort) that is fast for long lists.
The \textsf{msort} operator uses \textsf{dmx} to split the list into two parts,
sorts each part inductively into increasing order, and finally
uses the \textsf{mrg} operator to combine the sorted parts into one list.

If the operand of \textsf{msort} has only one element or none,
it is already in increasing order,
so the equations in that case,
like those for \textsf{isort} (page \pageref{eq:isrt0}),
are not inductive.
If the operand of \textsf{msort} has two or more elements,
the defining equation is inductive and
involves two sorting operations,
one for each of the two lists delivered by applying
\textsf{dmx} to the operand.

\begin{center}
\label{eq:msrt1}\index{axiom, by name!\{msrt0\}, \{msrt1\}, \{msrt2\}}\index{equation, by name!\{msrt0\}, \{msrt1\}, \{msrt2\}}
\label{eq:msrt0}
\label{eq:msrt2}
\begin{tabular}{ll}
\textsf{(msort nil) $=$ nil}                        & \{\emph{msrt0}\} \\
\textsf{(msort (cons $x$ nil)) $=$ (cons $x$ nil)} & \{\emph{msrt1}\} \\
\textsf{(msort (cons $x_1$ (cons $x_2$ xs))) $=$ (mrg (msort odds) (msort evns))} & \{\emph{msrt2}\} \\
 ~~~~ where  & \\
 ~~~~ \textsf{[odds, evns] $=$ (dmx (cons $x_1$ (cons $x_2$ xs)))} & \\
\end{tabular}
\end{center}

The inductive equation will be computational only if
both of the lists that \textsf{dmx} delivers are strictly
shorter than the operand of \textsf{msort}.
We expect this to be true because half
of the elements go into each list
(\textsf{dmx} length theorems, page \pageref{thm:dmx-length-first-second}).
The following formal definition expresses the \textsf{msort}
equations (\{\emph{msrt0}\}, \{\emph{msrt1}\}, \{\emph{msrt2}\}) in ACL2
but consolidates the equations for lists with one element or none in the
manner of the ACL2 definition of \textsf{isort} (page \pageref{defun:isort}):

\label{defun:msort}\label{eq:msrt1}\index{axiom, by name!\{msrt0\}, \{msrt1\}, \{msrt2\}}\index{equation, by name!\{msrt0\}, \{msrt1\}, \{msrt2\}}
\index{operator, by name!msort (merge-sort)}\index{defun!lemma hint}\index{defun!induction hint}\index{directive!induction hint}\index{directive!lemma hint}\seeonlyindex{msort (merge-sort)}{operator}\index{merge-sort}\index{sorting!merge-sort (msort)}
\begin{code}
\begin{verbatim}
(defun msort (xs)
  (declare (xargs
            :measure (len xs)
            :hints (("Goal"
                    :use ((:instance dmx-shortens-list-thm))))))
  (if (consp (rest xs))      ; 2 or more elements?
      (let* ((splt (dmx xs))
             (odds (first splt))
             (evns (second splt)))
        (mrg (msort odds) (msort evns))) ; {msrt2}
      xs))             ; (len xs) <= 1   ; {msrt1}
\end{verbatim}
\end{code}

The definition of \textsf{msort} includes
a \textsf{declare} directive
to help ACL2 verify that \textsf{msort} terminates.
The directive suggests basing the induction on the length of the operand.
To apply this inductive measure successfully,
ACL2 needs a hint suggesting the use of a lemma\footnote{Since
the theorem about the lengths of the lists
delivered by \textsf{dmx} is cited in the proof of another theorem
(namely, the theorem stating that \textsf{msort} terminates),
we refer to it as a \index{lemma}lemma.
The lemma could be derived from length theorems about \textsf{dmx}
proven in section \ref{sec:dmx} (page \pageref{thm:dmx-length-first-second}),
but a weaker form of those theorems turns out to be just what
ACL2 needs for its proof that \textsf{msort} terminates.}
stating that the \textsf{dmx} operator splits its
operand into two lists, both of which are strictly shorter than its operand.
ACL2 proves the lemma without assistance,
and it then admits (with the help of the \textsf{declare} directive)
the definition of \textsf{msort} to its mechanized logic.

\label{defthm:dmx-shortens-list}
\index{theorem, by name!\{dmx-shortens-list\}}
\begin{code}
\begin{verbatim}
(defthm dmx-shortens-list-thm ; lemma helps ACL2 admit def of msort
  (implies (consp (rest xs))  ; can't shorten 0- or 1-element lists
           (let* ((odds (first  (dmx xs)))
                  (evns (second (dmx xs))))
              (and (< (len odds) (len xs))
                   (< (len evns) (len xs))))))
\end{verbatim}
\end{code}
%'

Like \textsf{isort}, the \textsf{msort} operator puts the elements of its operand
in increasing order and preserves length and values.
The following statements of these properties, like those for \textsf{isort},
use the predicates \textsf{up} (page \pageref{defun:up})
and \textsf{occurs-in} (page \pageref{def:occurs-in}).\footnote{The
theorem statements employ the ACL2 operator \textsf{iff}, which is
\index{Boolean!equivalence ($\leftrightarrow$, iff)}\index{operator, by name!iff (Boolean equivalence)}\index{operator, logic!Boolean equivalence ($\leftrightarrow$, iff)}\index{iff (\emph{see also} operator)}\index{equivalence!Boolean ($\leftrightarrow$, iff)}Boolean equivalence
(box~\ref{aside:boolean-equivlance}, page \pageref{aside:boolean-equivlance}).}
Like \textsf{isort}, \textsf{(msort $xs$)} delivers a permutation of $xs$
(exercise~\ref{ex:permp-isort}, page \pageref{ex:permp-isort}),
but the proof is trickier for \textsf{msort}.
It might make a good project for ambitious readers.
ACL2 verifies the \textsf{msort} ordering property without help,
but it needs some lemmas stating the base case and the inductive case for
the proof of the length property.
ACL2 fails on the value property, so
we will settle for a paper-and-pencil proof of that one
(exercise \ref{msort-val-thm-pencil}, page \pageref{msort-val-thm-pencil}).
Figure~\ref{fig:msort-thms} (page \pageref{fig:msort-thms})
states the \textsf{msort} theorems and lemmas in ACL2.

\begin{figure}
\begin{code}
\begin{verbatim}
(defthm msort-order-thm
  (up (msort xs)))
(defthm msort-len-lemma-base-case
  (implies (not (consp (rest xs)))
           (= (len (msort xs)) (len xs))))
(defthm msort-len-lemma-inductive-case
  (= (len (msort (cons x xs)))
     (1+ (len (msort xs)))))
(defthm msort-len-thm
  (= (len (msort xs))
     (len xs)))
(defthm msort-val-thm
  (iff (occurs-in e xs)
       (occurs-in e (msort xs))))
\end{verbatim}
\end{code}
\label{defthm:msort-len}\label{defthm:msort-val}\index{sorting!msort theorems}\index{theorem!merge-sort (msort)}\index{theorem, by name!\{msort-len\}, \{msort-ord\}, \{msort-val\}}
\caption{Theorems and lemmas about merge-sort.}
\label{fig:msort-thms}
\label{defthm:msort-ord}
\end{figure}

\begin{exercises}
\exer {Do a paper-and-pencil proof that, under certain conditions, the \textsf{dmx} operator
delivers lists that are shorter than its operand
(\textsf{dmx-shortens-list-thm}, above).} % page \pageref{defthm:dmx-shortens-list}).

\exer {Do a paper-and-pencil proof that the \textsf{msort} operator
delivers a list that is in increasing order
(\textsf{msort-order-thm}, above).
You may cite \textsf{mrg-ord-thm}
(exercise \ref{ex:mrg-ord-thm}, page \pageref{ex:mrg-ord-thm}).}%page \pageref{defthm:msort-ord}).}

\exer {\label{msort-val-thm-pencil}%
Do a paper-and-pencil proof that the \textsf{msort} operator
preserves the values in its operand
(\textsf{msort-val-thm}, page \pageref{defthm:msort-val}).
You may cite the mrg-val theorem
(exercise \ref{ex:mrg-val-thm}, page \pageref{ex:mrg-val-thm}).}

\exer {Do a paper-and-pencil proof that the \textsf{msort} operator
preserves the length of its operand
(\textsf{msort-len-thm}, page \pageref{defthm:msort-len}).
You may cite the merge-length theorem
(exercise \ref{ex:mrg-length-thm}, page \pageref{ex:mrg-length-thm}).}

\exer {Do a paper-and-pencil proof that the \textsf{msort} operator
delivers a permutation of its operand (see exercise~\ref{ex:permp-isort}, page \pageref{ex:permp-isort}).
\emph{Caveat}: This is a project, not an exercise.}
\end{exercises}

\section{Analysis of Sorting Algorithms}
\label{sec:sort-analysis}

\seeonlyindex{algorithm analysis}{computation steps}\seeonlyindex{time of computation}{computation steps}In
this section, we discuss a
\index{computation steps!ACL2}computation model for ACL2
that gives us a way to count the number of computation steps required
to compute the value denoted by a formula.
We use the equations defining
the \textsf{msort} operator to derive inductive equations
for the number of computation steps that \textsf{msort} requires to rearrange lists
into increasing order.
Then, we assert a formula for the number of computation steps required
by \textsf{msort} and prove, by mathematical induction,
that the formula is correct.
\index{sorting!msort vs isort}
It turns out that the number of steps in the computation
\textsf{(msort [$x_1$, $x_2$, $\dots$ $x_n$])}
is proportional to $n~log(n)$.

We do the same for \textsf{isort}.
The number of steps in the \textsf{isort} computation varies widely,
depending on the order of the values in the operand,
so we estimate the average over randomized lists.
That average turns out to be proportional
to the square of the number of elements in the operand.
Finally, we compare the computation steps required by
the two operators, \textsf{msort} and \textsf{isort}, and find that
\textsf{msort} is much faster for long lists.

\subsection{Counting Computation Steps}
\label{subsec:counting-computation-steps}

A definition of an operator in ACL2
is a collection of equations that
reduces invocations of the operator
to computations of the result.
Predicates determine
which equations to select from the definition.
Both the formula that computes the result and
the predicate formulas that control
its selection invoke other operators.
In the case of an inductive equation,
the selected formula may invoke the operator
defined by the definition.
The computation eventually boils down to a sequence of basic,
\index{computation steps!counting}\index{computation steps!ACL2}one-step operations.
Analyzing the number of steps required to compute a result
amounts to counting the number of steps in that sequence.

A detailed analysis would allow a different
computation time for each basic operator.
That is, a model for detailed analysis could associate
several computation steps with one basic operator
and associate only a few steps with another operator.
There would also be a scale establishing a relationship between
computation steps and \index{computation time}computation time.

Our analysis will provide a less refined picture than such
a model because we will assume that each basic operator
delivers its result in just one computation step.
In the worst case, this would throw comparisons between
the number of steps in different computations off
by the ratio between the time required by the slowest basic
operator and the fastest. That is, comparisons
based on our crude model
will be off by a small factor,
but they will provide a
rough estimate of the ratio between the computation speed of
one operator and another.

\begin{figure}\index{computation steps!one-step operators}\index{computation steps!ACL2}\index{computation steps!counting}
\begin{center}
\begin{spacing}{0.9}
\begin{tabular}{ll}
Insertion: \textsf{(cons $x$ $xs$)}                                       & \\
Extraction: \textsf{(first $xs$)}, \textsf{(rest $xs$)}                            & \emph{operators that add one step}           \\
Arithmetic: \textsf{($+$ $x$ $y$)}, \textsf{($-$ $x$ $y$)}, \textsf{($*$ $x$ $y$)}, \dots   & ~~\emph{to a computation}                    \\
Boolean: \textsf{(and $x$ $y$)}, \textsf{(or $x$ $y$)}, \textsf{(not $x$)}, \dots       & ~~~~\emph{(after computing needed operands)} \\
Comparison: \textsf{(< $x$ $y$)}, \textsf{(<= $x$ $y$)}, \textsf{(= $x$ $y$)}, \dots  & \\
Cons predicate: \textsf{(consp $xs$)}                                     & \\
Selection: \textsf{(if $p$ $x$ $y$)}                                      & \emph{computes} $p$\emph{, then} $x$ \emph{or} $y$\emph{, but not both}
\end{tabular}
\end{spacing}
\end{center}
\vspace{-4mm}
\caption{Basic one-step operators.}
\label{fig:basic-one-step-ops}
\end{figure}

Figure~\ref{fig:basic-one-step-ops} %(page \pageref{fig:basic-one-step-ops})
specifies the basic, one-step operators of
the computation model.
Each basic operator in a formula contributes one step
to the computation, so
counting the number of steps in a computation is straightforward
if the definitions of the operators it invokes refer only
to the operators listed in the figure.
For example, analyzing the formula for constructing
the list \textsf{[1 2 3 4]} reveals a four-step computation.\vspace{2mm}\\
\hspace*{1cm}\textsf{[1 2 3 4]} denotes \textsf{(cons 1 (cons 2 (cons 3 (cons 4 nil))))}\\
\hspace*{1cm}Four Steps: \textsf{(cons 4 nil)}, \textsf{(cons 3 [4])}, \textsf{(cons 2 [3 4])}, \textsf{(cons 1 [2 3 4])}\vspace{2mm}

\begin{figure}
\begin{center}
\begin{tabular}{lcl}
\hline
\hspace*{5mm}\emph{formula}                         &\emph{steps}&~~~\emph{step 1, step 2, \dots}\\ \hline
\textsf{(cons 1 (cons 2 (cons 3 (cons 4 nil))))}    &     4      &\textsf{(cons 4 nil)}, \textsf{(cons 3 \dots)},\\
                                                    &            &~~~\textsf{cons}, \textsf{cons}\\
\textsf{(second [1 2 3])}                           &     2      &\textsf{(rest [1 2 3])}, \textsf{(first [2 3])}\\
\textsf{(if ($>$ 7 3) ($+$ 3 ($*$ 5 4)) ($+$ 2 2))} &     4      &\textsf{($>$ 7 3)}, \textsf{(if T $\Box$ $\Box$)}, \textsf{($*$ 5 4)},\\
                                                    &            &~~~\textsf{($+$ 3 20)}\\
\textsf{(if ($<$ 7 3) ($+$ 3 ($*$ 5 4)) ($+$ 2 2))} &     3      &\textsf{($<$ 7 3)}, \textsf{(if nil $\Box$ $\Box$)}, \textsf{($+$ 2 2)}\\
\end{tabular}
\end{center}
\caption{Computation steps in formulas with basic operators.}
\label{fig:basic-op-formulas}
\end{figure}

Figure~\ref{fig:basic-op-formulas} %(page \pageref{fig:basic-op-formulas})
displays a similar analysis on some formulas
composed of basic operations. The same kind of
analysis applies when the formulas invoke defined operators
rather than intrinsic ones like
\textsf{cons}, \textsf{first}, and \textsf{rest}.
For example, the operator \textsf{F-from-C}, defined
as follows, converts a temperature from degrees Celsius to
degrees Fahrenheit. It multiplies the temperature by the ratio \textsf{180/100}
(to adjust from Celsius degrees to the
more refined scale of Fahrenheit degrees), then adds 32
(to adjust the freezing point from zero to 32).\footnote{Ratios
in ACL2 are designated
by two integers separated by a slash.
The notation represents the number itself, not a computation:
\textsf{1/2} represents one-half, just as \textsf{2} represents two.
No computation is involved.}
That makes two basic operations in all, so the formula
\textsf{(F-from-C $100$)} represents a two-step computation.

\index{Fahrenheit vs Celsius}\index{Celsius vs Fahrenheit}\index{operator, by name!F-from-C}\seeonlyindex{F-from-C}{operator}
\begin{code}
\begin{verbatim}
(defun F-from-C (C)
  (+ (* 180/100 C) 32))
\end{verbatim}
\end{code}

The formula \textsf{(list (F-from-C $0$) (F-from-C $100$))}
makes a list in Fahrenheit degrees of two important
points on the temperature scale:
the freezing point of water ($0$ $^\circ$C) and the boiling point ($100$ $^\circ$C).
To count the number of steps in this computation,
we need to write the formula in terms of basic operations.
The operator \textsf{list} is shorthand for a sequence of nested
\textsf{cons} operations to build a list,
so in terms of basic operations, the formula is
\textsf{(cons (F-from-C $0$) (cons (F-from-C $100$) nil))}.
The total step-count comes to six: two for each \textsf{F-from-C} invocation
and one for each \textsf{cons}.

Another example:
the operator \textsf{swap2}, defined as follows, interchanges the
first two elements of a list if the list has at least two elements.
If not, it leaves the list as is.

\begin{code}\index{operator, by name!swap2}\seeonlyindex{swap2}{operator}
\begin{verbatim}
(defun swap2 (xs)
  (if (consp (rest xs))
      (cons (second xs) (cons (first xs)) (rest (rest xs)))
      xs))
\end{verbatim}
\end{code}

It refers to the operator that extracts the second element from a list,
which is shorthand for using the basic operator \textsf{rest} to drop the
first element, then the operator \textsf{first} to extract the first element
of what remains.
\label{steps-in-second-op}\index{computation steps!counting}\index{computation steps!ACL2}So,
the formula \textsf{(second $xs$)} would add two steps
to the computation. The number of steps in the computation \textsf{(swap2 $xs$)}
depends on how many elements $xs$ has. If $xs$ has two or more elements,
then \textsf{(swap2 $xs$)} takes ten steps:
\textsf{if}, \textsf{consp}, \textsf{rest}, \textsf{cons},
two steps for \textsf{second},
\textsf{cons} again, \textsf{first}, and \textsf{rest} again, twice.
If $xs$ has fewer than two elements, then \textsf{(swap2 $xs$)} takes three steps:
\textsf{if}, \textsf{consp}, and \textsf{rest}.

\begin{exercises}

\exer {Count the number of steps in \textsf{($-$ (F-from-C $100$) (F-from-C $0$))}.}

\exer {\label{ex:swap2-count}%
Count the number of steps in \textsf{(swap2 (list 1 2 3))}.\\
\emph{Note}: \textsf{(list 1 2 3)} is shorthand for nested \textsf{cons} operations
(figure~\ref{fig:list-nested-cons}, page \pageref{fig:list-nested-cons}).}

\exer {Count the number of steps in \textsf{(swap2 (list 1))}.}

\exer {Count the number of steps in
\textsf{(list (third $xs$) (second $xs$) (first $xs$))},
where the formula \textsf{(third $xs$)} is shorthand for
\textsf{(first (rest (rest $xs$)))}.}

\exer {Define an operator \textsf{C-from-F} that converts degrees Fahrenheit
to degrees Celsius, and count the number of operations
required to compute \textsf{(C-from-F (F-from-C $20$))}.}

\exer {What is \textsf{(C-from-F (F-from-C $x$))}?
What is \textsf{(F-from-C (C-from-F $x$))}?}

\exer {Define a theorem about \textsf{(C-from-F (F-from-C $x$))}
and get ACL2 to prove it. \\
\emph{Note}: The complicated formula must be on the left-hand side of the
equation.\footnote{Constraints on the order of operands
in equations have to do with strategic considerations
in the ACL2 theorem-proving engine that are
beyond the scope of the treatment here. If you want to track
down those ideas, read about rewrite rules in the ACL2 documentation.}\\
\emph{Note}: The predicate \textsf{ACL2-numberp} is true
if its operand is a number and false otherwise.
The theorem must constrain the domain to numbers
(use \textsf{ACL2-numberp} and \textsf{implies}).}

\end{exercises}

\subsection{Computation Steps in Demultiplex}
\label{subsec:dmx-steps}

The demultiplex operator, \textsf{dmx} (page \pageref{dmx-defun}),
parcels out the elements of a list
into two separate lists, with every other element going into one list
and the remaining elements going into the other list.
We repeat its definition here for convenience in counting steps.

\begin{code}\label{defun:dmx-copy}\index{axiom, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}\index{equation, by name!\{dmx0\}, \{dmx1\}, \{dmx2\}}\index{operator, by name!dmx (demultiplexer)}
\begin{verbatim}
(defun dmx (xys)
  (if (consp (rest xys))    ; 2 or more elements?
      (let* ((x (first xys))
             (y (second xys))
             (xsys (dmx (rest (rest xys))))
             (xs (first xsys))
             (ys (second xsys)))
        (list (cons x xs) (cons y ys)))      ; {dmx2}
      (list xys nil)))  ; 1 element or none  ; (dmx1}
\end{verbatim}
\end{code}

From the inductive equations for \textsf{dmx},
we will derive corresponding equations for counting computation steps.
Let $D_n$ stand for the number of steps required
to compute \textsf{(dmx $xs$)} when $xs$ has $n$ elements.
If $n$ is zero or one, \textsf{(consp (rest $xs$))} is false,
so \textsf{dmx} selects the third operand of the \textsf{if}
operator as the result.
The computation takes five steps: one step each for selection (\textsf{if}),
\textsf{consp}, and \textsf{rest},
plus two steps for \textsf{(list $xys$ nil)}
because it is shorthand for \textsf{(cons $xys$ (cons nil nil))}.
Therefore, $D_0 = D_1 = 5$.

If $xs$ has two or more elements (that is, $n+2$ elements
for some natural number $n$),
the computation will require $D_{n+2}$ steps.
From the definition of \textsf{dmx}, we see that the computation
has several parts:
selection (\textsf{if}), one step;
\textsf{consp}, one step;
extraction (\textsf{first}), one step;
a two-step extraction (\textsf{second}), two steps;
extraction (\textsf{rest}) twice, two steps;
computation of \textsf{(dmx (rest (rest $xs$)))},
$D_n$ steps because \textsf{(rest (rest $xs$))} has $n$ elements;
another extraction (\textsf{first}), one step;
another two-step extraction (\textsf{second}), two steps;
a double \index{cons}\textsf{cons}
(the operator \textsf{list} with two operands), two steps;
and two insertions (\textsf{cons}), two steps.
Altogether, that comes to $D_n + 14$ steps.
Putting the two cases together,
we come up with the following recurrence equations:\footnote{Inductive
equations in the numeric domain are called
\emph{recurrence equations}.}\\[-6mm]
\begin{center}\label{def:recurrence-equations}\index{axiom, by name!\{d1\}, \{d2\} (steps in dmx)}\index{equation, by name!\{d1\}, \{d2\} (steps in dmx)}\index{recurrence equations!dmx}\index{computation steps!dmx operation}\index{operator, by name!dmx (demultiplexer)}
\begin{tabular}{ll}
  $D_0 = D_1 = 5$      & \{d1\} \\
  $D_{n+2} = D_n + 14$ & \{d2\} \\
\end{tabular}
\end{center}

\index{recurrence equations!solving}
Sometimes it's possible to guess a closed-form formula
for the numbers in a sequence defined by recurrence equations
and then prove by induction that the formula is
correct.\footnote{A
\label{footnote:closed-form}\index{formula!closed form}\index{closed-form formula}closed-form formula
for $D_n$ is a formula
that doesn't refer to $D_m$ for any $m$.}
For equations \{d1\} and \{d2\},
$D_{n} = 14(\lfloor n/2\rfloor + 1) + 5$ is the right guess.\footnote{We
will use floor brackets $\lfloor x\rfloor$ and ceiling brackets $\lceil x\rceil$
(box~\ref{floor-ceiling-ops-brackets}, page \pageref{floor-ceiling-ops-brackets})
extensively in this chapter.}
Figure~\ref{fig:dmx-computation-time} %(page \pageref{fig:dmx-computation-time})
proves this conjecture using strong induction
(figure~\ref{strong-induction-rule}, page \pageref{strong-induction-rule}).

\begin{figure}
%\begin{quote}
Theorem \{dmx computation steps\}: \\
~~~~ $D_n \equiv$ \emph{number of computation steps in} \textsf{(dmx [$x_1$ $x_2$ $\dots$ $x_n$])} $= 14\lfloor n/2\rfloor + 5$\\
\emph{proof} \vspace{1mm}\\
%\end{quote}
%\begin{quote}
\emph{Base case} $(n=0$) \\
\begin{tabular}{lll}
$D_{0}$&$= 5$                        & \{d1\} \\
       &$= 14\lfloor 0/2\rfloor + 5$ & \{$\lfloor 0/2\rfloor=0$\} \\
\end{tabular}
\vspace{1mm}\\
\emph{Inductive case for} $n=1$\\
\begin{tabular}{lll}
$D_{1}$&$= 5$                        & \{d1\} \\
       &$= 14\lfloor 1/2\rfloor + 5$ & \{$\lfloor 1/2\rfloor=0$\} \\
\end{tabular}
\vspace{1mm}\\
\emph{Inductive case for} $n+2 \geq 2$\\
\begin{tabular}{lll}
$D_{n+2}$ &$= D_n + 14$                      & \{d2\} \\
          &$= 14\lfloor n/2\rfloor + 5 + 14$ & \{\emph{induction hypothesis}\} \\
          &$= 14(\lfloor n/2\rfloor + 1) + 5$& \{\emph{algebra}\} \\
          &$= 14\lfloor n/2 + 1\rfloor + 5$  & \{$\lfloor x\rfloor + 1 = \lfloor x+1\rfloor$\} \\
          &$= 14\lfloor(n+2)/2\rfloor + 5$   & \{\emph{algebra}\} \\
\end{tabular}
%\end{quote}
\index{computation steps!dmx operation}
\vspace{1mm}
\caption{Computation steps in demultiplex.}
\label{fig:dmx-computation-time}\index{theorem, by name!\{dmx computation steps\}}
\end{figure}

\begin{exercises}

\exer {\label{ex:recurrence-len}%
Derive recurrence equations for the number of steps in the computation of \textsf{(len $xs$)}
from the axioms for the \textsf{len} operator (figure~\ref{fig:len-axioms}, page \pageref{fig:len-axioms}).
Assume that selecting between the two axioms is a two-step computation
(one step to determine whether or not $xs$ has any elements
and one step to use that determination to select the appropriate axiom).}

\exer {Use the recurrence equations from exercise \ref{ex:recurrence-len} to
guess a formula for the number of steps
in the computation of \textsf{(len $xs$)}.
Prove that the formula is correct.}

\exer {\label{ex:recurrence-append}%
Derive recurrence equations for the
number of steps in the computation of \textsf{(append $xs$ $ys$)}
from the definition of \textsf{append} in
figure~\ref{fig:append-defun} (page \pageref{fig:append-defun}).}

\exer {Use the recurrence equations from exercise \ref{ex:recurrence-append} to
guess a formula for the number of steps in the
computation of \textsf{(append $xs$ $ys$)}.
Prove that the formula is correct.}

\end{exercises}

\subsection{Computation Steps in Merge}
\label{subsec:mrg-steps}

Our next goal is to estimate the number of steps in
the computation of \textsf{(mrg $xs$ $ys$)} (page \pageref{defun:mrg}).
We will not try to count the exact number of steps in the computation,
but we will look for an upper bound.
\index{computation steps!mrg (merge) operation}Our analysis
will ensure that the number of steps does not exceed an
amount that we can compute from the number of elements in the operands.

We begin by defining $M_{j,k}$ to be the maximum number of steps required to merge a list
of $j$ elements with a list of $k$ elements.\footnote{There are an infinite number
of such lists, and the maximum of an infinite set of numbers is problematic.
However, the merge computation depends only
on the ordering of the numbers in the operands,
not on their specific values.
There are a finite number of permutations of the elements of a list,
so the set of combinations to be considered in computing the maximum is finite.
A similar caveat applies to most of our proofs.
We have defined properties, including step-counting formulas,
in terms of the number of list elements
without considering the values of those elements.
Properties of the form P($n$) $\equiv$ $(\dots$ [$x_1$ $x_2$ \dots $x_n$] $\dots)$
more properly would take the form
P($n$) $\equiv$ $\forall x_1.\forall x_2\dots\forall x_n.(\dots$ [$x_1$ $x_2$ \dots $x_n$] $\dots)$.
However, even though property definitions have glossed over this issue,
the proofs themselves have been independent of the values, $x_k$.
That is, the proofs are correct and rigorous but with certain details omitted.
Fortunately, proofs carried out by an engine of
mechanized logic such as ACL2 take the details into account.}
We also define $A_n$ to be the maximum number of steps required to merge two lists
with a combined total of $n$ elements.\\
\hspace*{1cm}$M_{j,k} \equiv$ \emph{maximum steps in computation of} \textsf{(mrg [$x_1$ $x_2$ \dots $x_j$] [$y_1$ $y_2$ \dots $y_k$])} \\
\hspace*{1cm}$A_n \equiv$ maximum\{$M_{j,k} \mid j + k = n$\}

\index{computation steps!mrg (merge) operation}We will
prove $\forall n.(A_n \leq 10(n+1))$ by induction.
For the base case, $A_0 = M_{0,0}$ because the only pair of natural
numbers $j$ and $k$ with $j + k = 0$ is $j = k = 0$.
So, $A_0$ is the number of steps in the computation of \textsf{(mrg $xs$ $ys$)}
when \textsf{(consp $xs$)} and \textsf{(consp $ys$)} are false.
Let's look at the definition of \textsf{mrg} and count those steps.\footnote{We
repeat the definition of \textsf{mrg} here to make counting operations more convenient.
The previous definition (page \pageref{defun:mrg})
declared an induction scheme to help ACL2
admit the definition into its mechanized logic.
We have omitted the declaration here because we are analyzing
the computation without the assistance of ACL2.}
In this case, the computation consists of seven or fewer one-step operations
(\textsf{if}, \textsf{and}, \textsf{consp} twice,
\textsf{if} again, \textsf{not}, and \textsf{consp} again).\footnote{Actually,
it's six steps. The operator \textsf{and} does not compute its second operand
if its first operand is false.}
Therefore, $A_0 \leq 7 < 10\cdot(0 + 1)$, which proves the base case.

Now, consider the inductive case:
$\forall n.((A_n \leq 10(n+1)) \rightarrow (A_{n+1} \leq 10((n+1) + 1)))$.
The induction hypothesis is $A_n \leq 10(n + 1)$.
$A_{n+1}$ is a maximum of a set of numbers $M_{j,k}$, where $j + k = n+1$
and $M_{j,k}$ represents the maximum number of steps in the computation of
\textsf{(mrg [$x_1$ $x_2$ \dots $x_j$] [$y_1$ $y_2$ \dots $y_k$])}.

\label{defun:mrg-copy}
\begin{code}
\begin{verbatim}
(defun mrg (xs ys)
  (if (and (consp xs) (consp ys))
      (let* ((x (first xs)) (y (first ys)))
        (if (<= x y)
            (cons x (mrg (rest xs) ys))   ; mgx
            (cons y (mrg xs (rest ys))))) ; mgy
      (if (not (consp ys))
          xs     ; ys is empty            ; mg0
          ys)))  ; xs is empty            ; mg1
\end{verbatim}
\end{code}

If one of the operands is empty, there are, as in the base case,
at most seven steps in the computation.
If neither operand is empty, there are eight one-step operations
(\textsf{if}, \textsf{and}, \textsf{consp} twice,
\textsf{first} twice, \textsf{if} again, and the comparison $x \leq y$)
that culminate in the selection of
one of two inductive formulas: \textsf{(cons $x$ (mrg (rest $xs$) $ys$))}
or \textsf{(cons $y$ (mrg $xs$ (rest $ys$)))}.
Both of these formulas have two one-step operations (\textsf{cons} and \textsf{rest})
for a total, counting the eight previous steps, of ten one-step operations.
There is also an inductive invocation to account for:
\textsf{(mrg (rest $xs$) $ys$)} or \textsf{(mrg $xs$ (rest $ys$))}.

The total number of elements in the operands
of the inductive invocation of \textsf{mrg}
is $n$ because there are $n+1$ elements in the two lists $xs$ and $ys$,
taken together, and in the inductive invocation the operator \textsf{rest} has
dropped an element from one of the lists.
That is, there are a total of $n$ elements in the operands
in the invocation \textsf{(mrg (rest $xs$) $ys$)},
and the same is true of \textsf{(mrg $xs$ (rest $ys$))}.
Therefore, by the definition of $A_n$,
the number of steps in the computation of the inductive invocation,
no matter which one of them is selected, cannot exceed $A_n$.
\index{recurrence equations!mrg (merge) operation}
We conclude that $A_{n+1} \leq A_n + 10$
($A_n$ steps for the inductive invocation
plus ten one-step operations).
\index{computation steps!mrg (merge) operation}
By the induction hypothesis, $A_n \leq 10(n+1)$.
Therefore, $A_{n+1} \leq 10(n+1) + 10$.
Factoring out the 10 algebraically,
we find that $A_{n+1} \leq 10((n+1) + 1)$.
That completes the proof of the inductive case,
and we conclude by induction that $\forall n.(A_n \leq 10(n+1))$.
\label{thm:mrg-computation-time}\label{thm:mrg-steps}\index{computation steps!mrg (merge) operation}
%%% could not make \begin{theorem} work here
%%% in the following theorem, \emph works backwards for some reason unknown to me -- rlp
%%%\begin{theorem}[\{dmx computation steps\}] \\
\begin{center}\index{theorem, by name!\{mrg computation steps\}}
\begin{tabular}{l}
Theorem \{mrg computation steps\}:\\
$($\textsf{(len $xs$)}$+$\textsf{(len $ys$)} $= n$) $\rightarrow$ $($\emph{steps to compute} \textsf{(mrg $xs$ $ys$)} $\equiv A_n \leq 10(n+1))$\\
\end{tabular}
\end{center}
%\end{theorem}

\begin{exercises}

\exer{The double index
of $M_{j,k}$ made the proof a little tricky.
Another approach would have been to use the principle of double induction
(figure~\ref{double-induction-rule}, page \pageref{double-induction-rule}),
which reframes mathematical induction for double-index predicates.
Suppose that $P$ is a predicate whose universe of discourse is pairs of natural numbers.
That is, for each pair of natural numbers $m$ and $n$,
$P(m,n)$ selects a proposition in the predicate.
Use the predicate $P$ to define another predicate $Q$
that has the natural numbers as its universe of discourse and
that has the following properties:\\
\hspace*{3mm}a. $Q(0)$ is the base case for double induction on $P$.\\
\hspace*{3mm}b. $(\forall n.(Q(n) \rightarrow Q(n+1)))$ is the inductive case
for double induction on $P$.\\
\emph{Note}: This exercise is difficult and not particularly instructive.
The point is that double
induction can be reduced to ordinary mathematical induction.}

\end{exercises}

\begin{figure}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{l}{Prove  $(\forall m.P(m,0)) \wedge (\forall n.P(0,n))$                                 \hfill \emph{base case}}\\
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - &\\
\multicolumn{2}{l}{Prove $(\forall m.(\forall n.((P(m+1, n) \wedge P(n, m+1)) \rightarrow P(m+1,n+1))))$ \hfill \emph{inductive case}}\\
--------------------------------------------------------------------------------------\{dbl ind\}  &\\
Infer $(\forall m.(\forall n.P(m,n)))$                                                &\\
\end{tabular}
\end{center}
\index{induction!double}
\caption{Double induction: a rule of inference.}
\label{double-induction-rule}
\end{figure}

\subsection{Computation Steps in Merge-Sort}
\label{subsec:msort-steps}

We have been working towards an upper bound on the number of steps
needed to arrange the elements of a list into increasing order
using the \textsf{msort} operator
(pages \pageref{defun:msort} and \pageref{defun:msort-copy}).\footnote{As
with the definition of \textsf{mrg}, we repeat the definition of \textsf{msort}
to facilitate counting steps, but we omit the hints
provided in the previous definition to help ACL2 prove termination.}

\index{sorting!merge-sort (msort)}
\begin{code}
\begin{verbatim}

(defun msort (xs)
  (if (consp (rest xs))      ; 2 or more elements?
      (let* ((splt (dmx xs))
             (odds (first splt))
             (evns (second splt)))
        (mrg (msort odds) (msort evns))) ; {msrt2}
      xs))               ; (len xs) <= 1 ; {msrt1}
\end{verbatim}
\end{code}
\label{defun:msort-copy}

Let $S_n$ stand for the number of steps in the computation
\textsf{(msort [$x_1$ $x_2$ \dots $x_n$])}.
If $n$ is zero or one, \textsf{msort} selects a noninductive
formula, and this requires three one-step operations:
\textsf{if}, \textsf{consp}, and \textsf{rest}.
If $n$ is two or bigger, it's more complicated.
Figure~\ref{msort-recurrences} (page \pageref{msort-recurrences})
derives the recurrences from the definition of \textsf{msort}.

The crucial steps are the two inductive invocations of \textsf{msort}.
The operand in the first invocation is a list delivered as the first component in
a demultiplexed list of $n$ elements.
(It is called \textsf{odds} in the \textsf{let$*$} formula.)
According to theorem \{dmx-len-first\} (page \pageref{thm:dmx-length-first-second}),
\textsf{odds} is a list containing $\lceil  n/2\rceil$ elements.
So, by the definition of \emph{S},
there are $S_{\lceil n/2\rceil}$ steps in the computation of \textsf{(msort odds)}.
Similarly, theorem  \{dmx-len-second\} (page \pageref{thm:dmx-length-first-second})
says that the second component of the demultiplexed list (\textsf{evns})
has $\lfloor n/2\rfloor$ elements, which means that there are
$S_{\lfloor n/2\rfloor}$ steps in the computation of \textsf{(msort evns)}.

The \textsf{(dmx $xs$)} computation takes $14\lfloor  n/2\rfloor + 5$ steps
(theorem \{dmx computation steps\},
figure~\ref{fig:dmx-computation-time},
page \pageref{fig:dmx-computation-time}).
The \textsf{mrg} computation takes at most $A_n = 10(n+1)$ steps
(theorem \{mrg computation steps\}, page \pageref{thm:mrg-steps}).
There are six additional steps
in \textsf{(msort $xs$)} when $xs$ has two or more elements,
all of which are basic operations:
one step each for \textsf{if}, \textsf{consp}, \textsf{rest}, and \textsf{first},
plus two steps for \textsf{second}.
Adding all this up
(two \textsf{msorts}, \textsf{dmx}, \textsf{mrg}, and the six basic steps),
we find \index{recurrence equations!merge-sort (msort)}that
$S_n \leq S_{\lceil  n/2\rceil} + S_{\lfloor  n/2\rfloor} +
          (14\lfloor n/2\rfloor + 5) + 10(n+1) + 6$.

Figure~\ref{msort-recurrences} (page \pageref{msort-recurrences})
summarizes this recurrence analysis.
The recurrences are upper bounds rather than equations because
our analysis of the \textsf{mrg} operator put an upper bound on
the number of steps in the computation, not an exact count.
The simplified formula $7n + 5$
is a bit larger than $14\lfloor n/2\rfloor + 5$
when $n$ is odd, but we're deriving an upper bound
anyway, so the inequality still holds.
A final algebraic simplification,
$(14\lfloor n/2\rfloor + 5) + 10(n+1) + 6 \leq (7n + 5) + 10(n+1) + 6 = 17n + 21$,
leads to inequality \{s2\}.

\begin{figure}
\begin{center}
\begin{spacing}{0.9}
\begin{tabular}{lrl}
  \emph{operator} & \emph{steps}$\leq$ & \emph{step-counts for} $n \geq 2$\\
  \hline
   \textsf{if}     & 1 & figure \ref{fig:basic-one-step-ops}, page \pageref{fig:basic-one-step-ops}  \\
   \textsf{consp}  & 1 & figure \ref{fig:basic-one-step-ops}  \\
   \textsf{rest}   & 1 & figure \ref{fig:basic-one-step-ops} \\
   \textsf{dmx}    & $14\lfloor n/2\rfloor + 5$ & \{dmx computation steps\}, $n$ elements, page \pageref{fig:dmx-computation-time}\\
   \textsf{first}  & 1 & figure \ref{fig:basic-one-step-ops} \\
   \textsf{second} & 2 & figure \ref{fig:basic-op-formulas}, page \pageref{fig:basic-op-formulas} \\
   \textsf{mrg}    & $10(n+1)$ & \{mrg computation steps\}, $n$ elements, page \pageref{thm:mrg-computation-time}\\
   \textsf{msort}  & $S_{\lceil  n/2 \rceil}$  & \{dmx-len-first\}, page \pageref{thm:dmx-length-first-second} \\
   \textsf{msort}  & $S_{\lfloor n/2 \rfloor}$ & \{dmx-len-second\}, page \pageref{thm:dmx-length-first-second} \vspace{5pt} \\
   \hline
	\multicolumn{3}{c}{$total = 1+1+1+(14\lfloor n/2\rfloor+5)+1+2+10(n+1)+S_{\lceil n/2\rceil}+S_{\lfloor n/2\rfloor}$} \vspace{1pt} \\
   \hline
\end{tabular}
\end{spacing}
~\vspace{2mm}\\
\begin{tabular}{ll}
   $S_n \equiv$ \emph{steps to compute} \textsf{(msort [$x_1$ $x_2$ \dots $x_n$])} \\
   $S_0 = S_1 = 3$ & \{s1\}\\
   $S_{n} \leq S_{\lceil n/2 \rceil} + S_{\lfloor n/2 \rfloor} + 17n + 21$, if $n \geq 2$ & \{s2\}\\
\end{tabular}
\end{center}
\caption{Recurrence inequalities for merge-sort computation steps.}
\label{msort-recurrences}\index{recurrence equations!merge-sort (msort)}\index{axiom, by name!\{s1\}, \{s2\} (steps in msort)}\index{equation, by name!\{s1\}, \{s2\} (steps in msort)}\index{S recurrence (steps in msort)}
\end{figure}

Now, we are going to guess a closed-form formula
(see footnote, page \pageref{footnote:closed-form})
for an upper bound on $S_n$
and then use strong induction
(figure~\ref{strong-induction-rule}, page \pageref{strong-induction-rule})
to prove that the formula is correct.
The right-hand side of the recurrence inequality \{s2\} expresses
an upper bound on $S_n$ in terms of $S_{n/2}$.
People experienced in solving recurrences take this as an
indication of $n~log(n)$ growth for $S_n$.
Accordingly, we can expect to be able to find a multiplier $\alpha$ such that
$\forall n.(S_{n+2} \leq \alpha \cdot (n+2)~log_2(n+2))$.\footnote{The
formula $\alpha\cdot n~log_2(n)$ cannot be an upper bound for $S_n$
when $n$ is zero or one because $n~log_2(n) = 0$ when $n$ is zero or one,
and we know
(figure~\ref{msort-recurrences}) %, page \pageref{msort-recurrences})
that $S_0 = S_1 = 3$, which is more than zero.}
Finding a multiplier that works is mostly a matter of
fiddling around with the recurrences to get some intuition
about the numbers they produce.
Here's the multiplier we came up with:
$\alpha = 42$.
Figure~\ref{thm:msort-nlogn} (page \pageref{thm:msort-nlogn})
proves that
$\forall n.(S_{n+2} \leq 42(n+2)~log_2(n+2))$
by strong induction.\footnote{A
smaller multiplier can be found, but
we're not too concerned with the size of the multiplier,
especially since we don't have a scale for the amount of time
a computation step takes in our model.
It's the order of growth, the $n~log_2(n)$ part, that interests us.
The coincidence that 42 works may amuse \index{Adams, Douglas}Douglas Adams fans.}

\begin{figure}
Theorem \{msort $n~log(n)$\}: $\forall n.(S_{n+2} \leq 42(n+2)~log_2(n+2))$ \\
\begin{tabular}{l}
\emph{Proof by strong induction} \\
\emph{Base Case} $(n = 0)$\\
\end{tabular}
\\
\begin{tabular}{lll}
$S_{0+2}$ & $\leq S_{\lceil(0+2)/2\rceil} + S_{\lfloor(0+2)/2\rfloor} + 17(0+2) + 21$ & \{s2\}           \\
          & $= S_1 + S_1 + 55$                                                        & \{\emph{algebra}\}\\
          & $= 3 + 3 + 55$                                                            & \{s1\}           \\
          & $< 42(0+2)~log_2(0+2)$                                                    & \{\emph{arithmetic}, $log_2(0+2)=1$\}\\
\end{tabular}
\vspace{1mm}\\
\begin{tabular}{l}
\emph{Inductive Case for} $1 \leq n \leq 18$ \\
~~~Use recurrences (figure~\ref{msort-recurrences}, page \pageref{msort-recurrences}) to calculate $S_{n+2}$, $n=1, 2, \dots 18$.\\
~~~Observe that $S_{n+2} \leq 42 (n+2)~log_2(n+2)$, $n=1, 2, \dots 18$. \\
\end{tabular}
\vspace{1mm}\\
\begin{tabular}{l}
\emph{Inductive Case for} $n \geq 19$ \emph{(using} $m \equiv n+2$ \emph{to save space)}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \\
\end{tabular}
\\
\begin{tabular}{llll}
$S_{n+2}$ & $=$    & $S_m$                                                           & \{\emph{definition} $m \equiv n+2$\} \\
          & $\leq$ & $S_{\lceil m/2\rceil} + S_{\lfloor m/2\rfloor} + 17m+21$        & \{s2\} \\
          & $\leq$ & $42\lceil m/2\rceil~log_2\lceil m/2\rceil ~ +$                  & \{\emph{induction hypothesis, twice}\\
          &        & $42\lfloor m/2\rfloor~log_2\lfloor m/2\rfloor + 17m+21$         & ~~ \emph{(}$\lceil m/2\rceil < m$, $\lfloor m/2\rfloor < m$\emph{)}\} \\
          & $\leq$ & $42\lceil m/2\rceil~log_2\lceil m/2\rceil~+~$                   & \\
          &        & $42\lfloor m/2\rfloor~log_2\lceil m/2\rceil + 17m+21$           & \{$\lfloor x\rfloor \leq \lceil x\rceil \rightarrow$ $log_2\lfloor x\rfloor \leq log_2\lceil x\rceil$\}\\
          & $=$    & $42(\lceil m/2\rceil + \lfloor m/2\rfloor)log_2\lceil m/2\rceil +$ \\
          &        & $17m + 21$ & \{\emph{algebra (factor out} $42~log_2\lceil m/2\rceil$\emph{)}\} \\
          & $=$    & $42m~log_2\lceil m/2\rceil + 17m + 21$                          & \{$\lceil m/2\rceil + \lfloor m/2\rfloor\ = m$\}\\
          & $\leq$ & $42m~log_2((m+1)/2)        + 17m + 21$                          & \{$log_2\lceil m/2\rceil \leq log_2((m+1)/2)$\} \\
          & $\leq$ & $42m~log_2((m+1)/2)        + 17m + m$                           & \{$m = n+2 \geq 19+2 = 21$\} \\
          & $\leq$ & $42m~log_2((m+1)/2)        + 18m$                               & \{$17m + m = 18m$\} \\
          & $=$    & $42m(log_2((m+1)/2)        + (18/42))$                          & \{\emph{algebra (factor out} $42m$\emph{)}\} \\
          & $=$    & $42m(log_2(m+1) $ \\
          &        & $\qquad\qquad - log_2(2) + (18/42))$                            & \{$log_2(x/y) = log_2(x) - log_2(y)$\} \\
          & $=$    & $42m(log_2(m+1) - 1 + (18/42))$                                 & \{$log_2(2) = 1$\} \\
          & $<$    & $42m(log_2(m+1) + log_2(m/(m+1)))$                              & \{$m \geq 3 \rightarrow log_2\frac{m}{m+1} > -1 + \frac{18}{42}$\} \\
          & $=$    & $42m~log_2((m+1)\cdot m/(m+1))$                                 & \{$log_2(x) + log_2(y) = log_2(xy)$\} \\
          & $=$    & $42m~log_2(m)$                                                  & \{\emph{algebra}\} \\
          & $=$    & $42(n+2)~log_2(n+2)$                                            & \{\emph{definition} $m \equiv n+2$\} \\
\end{tabular}
\index{computation steps!merge-sort (msort)}
\caption{Bound on steps in merge-sort computation.}
\label{thm:msort-nlogn}\index{theorem, by name!\{msort $n~log(n)$\}}
\end{figure}

\begin{exercises}

\exer {\label{defun:Srecur}%
Use the recurrences in figure~\ref{msort-recurrences} %(page \pageref{msort-recurrences})
to define an operator \textsf{S} in ACL2 with \textsf{(S $n$)} $= S_n$.}

\exer {\label{defun:log2}%
For any nonzero positive number $x$, $\lfloor log_2(x)\rfloor$
is the biggest integer $n$ such that $2^n \leq x$.
Define an operator \textsf{log2} in ACL2 that computes $\lfloor log_2(x)\rfloor$
for $x \geq 1$.}

\exer {If $S_{n+2} \leq 42(n+2)\lfloor log_2(n+2)\rfloor$, then
$S_{n+2} \leq 42(n+2) log_2(n+2)$.
Use the operators from exercises \ref{defun:Srecur} and \ref{defun:log2}
to compare $S_{n+2}$ with $42(n+2)\lfloor log_2(n+2)\rfloor$
for each natural number $n$ between $1$ and $18$. Explain any anomalies.
\emph{Hint}: $log_2(3)$ > 3/2.}

\end{exercises}

\subsection{Computation Steps in Insertion-Sort}
\label{subsec:isort-steps}

We want to compare the performance of
the \textsf{msort} operator (merge-sort)
with that of the \textsf{isort} operator (insertion-sort).
The difference can be dramatic
(see footnote, page \pageref{bubble-vs-quicksort-example}).
The \textsf{isort} operator almost always
takes much more time than \textsf{msort}
to arrange a list of numbers,
and the difference grows rapidly with the number of elements in the list.

However, the number of steps in the computation \textsf{(isort $xs$)}
varies widely depending on the arrangement of the numbers in the operand $xs$.
For a few arrangements,
\textsf{(isort $xs$)} is faster than \textsf{(msort $xs$)},
and when $xs$ is a short list, \textsf{isort} can be faster for any list.
In fact, high-speed, general purpose software for sorting
usually combines a method similar to insertion-sort
with a method comparable to merge-sort.
This hybrid strategy treats
the list to be sorted as a collection of short lists
(usually up to about eight elements),
applies an \textsf{isort}-like operator to the short lists,
and then combines them
using an \textsf{msort}-like operator.

The number of computation steps required by the
\index{insertion-sort}\textsf{isort} operator
varies widely, but
an estimate of the average number of computation steps that
\textsf{isort} requires for randomly arranged lists
is useful for comparison purposes.
We repeat the definition of \textsf{isort}
(figure~\ref{defun:insert-isort}) %, page \pageref{defun:insert-isort})
for convenience in the analysis.

\begin{figure}
\begin{code}
\begin{verbatim}
(defun insert (x xs) ; assume x1 <= x2 <= x3 ...
  (if (and (consp xs) (> x (first xs)))
      (cons (first xs) (insert x (rest xs))); {ins2}
      (cons x xs)))                         ; {ins1}
(defun isort (xs)
  (if (consp (rest xs)) ; xs has 2 or more elements?
      (insert (first xs) (isort (rest xs))) ; {isrt2}
      xs))              ; (len xs) <= 1     ; {isrt1}
\end{verbatim}
\end{code}
\index{operator, by name!insert (in order)}\index{equation, by name!\{ins0\}, \{ins1\}, \{ins2\}}\index{operator, by name!isort (insertion-sort)}\index{equation, by name!\{isrt0\}, \{isrt1\}, \{isrt2\}}\index{compare!numbers ($<$, $<=$, $=$, $>=$, $>$)}\index{predicate!numeric order ($<$, $<=$, $=$, $>=$, $>$)}\index{order!numeric ($<$, $<=$, $=$, $>=$, $>$)}\index{operator!numeric order ($<$, $<=$, $=$, $>=$, $>$)}\index{number!order ($<$, $<=$, $=$, $>=$, $>$)}\seeonlyindex{greater than ($>$)}{predicate}\index{sorting!insert (in order)}\index{insertion-sort (isort)}
\caption{Formal definition of \textsf{isort}.}
\label{defun:insert-isort}\label{defun:isort-copy}
\end{figure}

The computation of \textsf{(insert $x$ nil)}
takes four steps
(\textsf{if}, \textsf{and}, \textsf{consp},
\textsf{cons}).\footnote{The operator \textsf{and}
does not compute its second operand if its first operand
is false.}
In the computation \textsf{(insert $x$ [$x_1$ $x_2$ \dots $x_{n+1}$])},
the \textsf{insert} operator assumes that
$x_1 \leq x_2 \leq \dots x_{n+1}$.
In the worst case, $x > x_{n+1}$ and the \textsf{insert} computation
will deliver the list [$x_1$ $x_2$ \dots $x_{n+1}$ $x$].
A careful analysis shows that this worst case insertion takes
$8(n+1)+4$ steps (exercise~\ref{ex:insert-steps}, page \pageref{ex:insert-steps}).

It seems reasonable to expect that, on average,
for random data, $x$ will get inserted about
half way down the list $xs$.
That means it would take, on average, about
half as many steps to compute \textsf{(insert $x$ $xs$)}
as it takes in the worst case,
which is when $x$ exceeds all the numbers
in $xs$, putting $x$ at the end of the
list that \textsf{(insert $x$ $xs$)} delivers.
Proving the assertion about the average
requires understanding the nature of random
data and probabilistic effects, so we are not going
to pursue a proof, but we will assume that it's true.
With that assumption and $8(n+1)+4$
computation steps for worst case insertion,
the average number of steps
for \textsf{(insert $x$ [$x_1$ $x_2$ \dots $x_{n+1}$])} would be
$G_{n+1} = (8(n+1)+4)/2 = 4(n+1)+2 = 4n+6$.

What does this mean for \textsf{(isort $xs$)}?
From the definition of \textsf{isort},
we see that when \textsf{(len $xs$)} is zero or one,
\textsf{isort} performs three one-step operations
(\textsf{if}, \textsf{consp}, \textsf{rest}).
When $xs$ has $n+2$ elements (that is, two or more elements),
there are five one-step operations
(\textsf{if}, \textsf{consp},
\textsf{rest}, \textsf{first}, \textsf{rest} again)
plus an \textsf{insert} operation
with a second operand that has $n+1$ elements,
which takes $G_{n+1} = (4n+6)$ computation steps, on average.
Finally, there remains the inductive invocation of \textsf{isort}
with an operand that has $n+1$ elements.
This analysis yields the recurrence equations
in figure~\ref{fig:isort-steps} (page \pageref{fig:isort-steps})
for the average number of steps in the computation
\textsf{(isort [$x_1$ $x_2$ \dots $x_{n}$])}, which we denote by $I_n$.

We could guess a closed-form formula for $I_n$ and prove it by induction,
but instead let's carry out an analysis that applies
the recurrence equations for $I_n$ in stages.
Figure~\ref{fig:isort-steps} (page \pageref{fig:isort-steps})
displays the recurrence equations and presents the analysis,
using equation \{i2\} to build a formula for $I_{n+2}$ step by step.
First, replace $I_{n+2}$ by the right-hand side of equation \{i2\}.
Then, if $(n+1)\geq 2$, replace $I_{n+1}$ by the right-hand side of \{i2\} again
and continue using equation \{i2\} in this way until
the formula comes down to $(I_1 + \dots)$.
At that point, replace $I_1$ by $3$, citing equation \{i1\}.

Then, some algebraic reorganization reveals a factor
of $(1 + 2 + 3 + \dots n)$ in one of the terms in the sum.
This is the well-known
triangular number:\footnote{The formula for the triangular number
might win a contest for most popular example of proof by mathematical induction
in a poll of discrete math textbooks. It's either that or the
geometric progression (exercise~\ref{ex:geometric-progression}, page \pageref{ex:geometric-progression}).
Proving the triangular number formula is exercise~\ref{ex:triangular-number} (page \pageref{ex:triangular-number}).}
$(1 + 2 + 3 + \dots n) = n(n+1)/2$.
In the end, with a little more algebraic reorganization,
we find that \textsf{(isort [$x_1$ $x_2$ \dots $x_{n+2}$])} requires,
on average,
$I_{n+2} = (2n+11)(n+1) + 3$ computation steps.
Another way to say this is
$I_{n} = (2n+7)(n-1) + 3$ for $n\geq 2$.

\begin{figure}
\begin{center}
\begin{spacing}{0.9}
\begin{tabular}{ll}
\emph{Recurrence Equations for} $I_n$ &\\
\hline
$I_0 = I_1 = 3$                                      & \{i1\} \\
$I_{n+2} = I_{n+1} + (4n+6) + 5 = I_{n+1} + 4n + 11$ & \{i2\} \\
\end{tabular}
\end{spacing}
\vspace{2mm}
\begin{spacing}{0.9}
\addtolength{\tabcolsep}{-3pt}
\begin{tabular}{rll}
    & \emph{Closed-Form Formula for} $I_n$ & \\
\hline
    & $I_{n+2}$ & \\
$=$ & $I_{n+1} + (4n+11)$ & \{i2\} $I_{n+2}$\\
$=$ & $I_{n} + (4(n-1)+11) + (4n+11)$ & \{i2\} $I_{n+1}$ \\
    & \vdots & \\
$=$ & $I_{3} + (4\cdot 2 + 11) + (4\cdot 3 + 11) + \dots (4n+11)$                   & \{i2\} $I_{4}$ \\
$=$ & $I_{2} + (4\cdot 1 + 11) + (4\cdot 2 + 11) + (4\cdot 3 + 11) + \dots (4n+11)$ & \{i2\} $I_{3}$ \\
$=$ & $I_{1} + (4\cdot 0 + 11)$~$+$                                                 & \{i2\} $I_{2}$ \\
    & \phantom{$I_{2} + $} ~$(4\cdot 1 + 11) + (4\cdot 2 + 11) + (4\cdot 3 + 11) + \dots (4n+11)$ & \\
$=$ & $3 + (4\cdot 0 + 11)$~$+$                                                     & \{i1\}\\
    & \phantom{$I_{2} + $} $(4\cdot 1 + 11) + (4\cdot 2 + 11) + (4\cdot 3 + 11) + \dots (4n+11)$ & \\
$=$ & $3 + 11 + 4\cdot(1 + 2 + + 3 + \dots n) + 11n$                                & \{\emph{algebra}\} \\
$=$ & $3 + 11 + 4\cdot(n(n+1)/2) + 11n$                                             & \{\emph{triangular number}\} \\
$=$ & $(2n+11)(n+1) + 3$                                                            & \{\emph{algebra}\} \vspace{2mm}\\
    & $I_n = (2(n-2)+11)(n-2+1) + 3 = (2n+7)(n-1)+3$                                & if $n\geq 2$\\
\end{tabular}\addtolength{\tabcolsep}{3pt}
\end{spacing}
\end{center}
\vspace{-2mm}  %FRAGILE FRAGILE FRAGILE
\caption{$I_n$ = average number of steps to compute \textsf{(isort $x$ [$x_1$ $x_2$ \dots $x_{n}$])}.}
\label{fig:isort-steps}\index{computation steps!insertion-sort (isort)}\index{recurrence equations!isort (insertion-sort)}\index{I (isort recurrence)}\index{sorting!insertion-sort (isort)}
\end{figure}

Theorem \{msort $n~log(n)$\}
(figure~\ref{thm:msort-nlogn}, page \pageref{thm:msort-nlogn}) provides
an upper bound\footnote{It
turns out that this upper bound is close to the average
for merge-sort on randomized lists.}
on the number of steps $S_n$ in the computation
\textsf{(msort [$x_1$ $x_2$ \dots $x_{n+2}$])}:
$S_{n} \leq 42n~log_2(n)$ when $n =$ (len $xs$) $\geq 2$.
To compare the time it takes to sort a
list of numbers using \textsf{isort} versus \textsf{msort},
we can compute a lower bound on the ratio between
the number of computation steps that insertion-sort requires
versus merge-sort:
$I_n/S_n \geq (2n+7)(n-1)/(42n~log_2(n))$ when $n \geq 2$.
(We dropped $+3$ from the numerator, but the ratio is a lower bound anyway,
so it's still a lower bound.)
This ratio gets big fast with increases in $n$, the number of elements
in the list to be sorted.

\index{sorting!msort vs isort}\index{computation steps!msort vs isort}The
break-even point occurs at about a hundred elements.
For 1,000 elements, the ratio is about five.
That is, \textsf{msort}, as we have defined it (page \pageref{defun:msort-copy}),
is about five times faster
than \textsf{isort} (page \pageref{defun:insert-isort})
for a list with 1,000 elements.
For 10,000 elements, \textsf{msort} is about 40 times faster.
For 100,000 elements, 300 times faster,
and for 1,000,000 elements, about 2,000 times faster.
These estimates are on the conservative side
because we made no attempt to get a tight
upper bound on the number of computation steps for \textsf{msort},
and we have not paid close attention to computational details
in the definitions of \textsf{isort} and  \textsf{msort}.
Serious software for sorting is loaded with performance tweaks,
and that can make the ratios more extreme in practice.

Beyond a comparison of the performance of merge-sort
versus insertion-sort, the main thing to take away from this discussion
is that inductive definitions provide a straightforward way to
\index{recurrence equations!deriving}
derive recurrence equations for the number of steps that the defined operator
takes to carry out a computation.
If a solution to the recurrences can be found,
whether by guessing or by using one of a host of solution methods
that are beyond the scope of the treatment here,
then there is a good chance that an
\index{recurrence equations!solving}inductive proof
can verify that the solution is correct.
In this way, defining operators with inductive equations
facilitates analyzing the number of computational
steps the operators require to perform an operation.

\begin{exercises}

\exer {\label{ex:insert-recurrence}%
Derive, from the definition of
\textsf{insert} (page \pageref{defun:insert-isort}),
recurrence equations for the number of steps
in the computation \textsf{(insert $x$ [$x_1$ $x_2$ \dots $x_{n+1}$])}
if $x_1 \leq x_2 \leq \dots x_{n+1} < x$.}

\exer {\label{ex:insert-steps}%
Using the recurrences from exercise \ref{ex:insert-recurrence},
prove that the number of steps in the computation of
\textsf{(insert $x$ [$x_1$ $x_2$ \dots $x_{n+1}$])}
is $8(n+1)+6$ or less if $x_1 \leq x_2 \leq \dots x_{n+1} < x$.}

\exer {The multiplier $42$ in our bound on $S_n$ gets sloppier as $n$ increases.
Find  $\beta < 42$ that works for lists with
over 100 elements:
$S_{n} \leq \beta\cdot n~log_2(n)$ if $n > 100$.}

\exer {\label{ex:triangular-number}%
Use induction to prove the formula for the triangular number.\\
\hspace*{1cm}$(1 + 2 + 3 + \dots n) = n(n+1)/2$\\
You may be the billionth person to prove it. Knock yourself out.}
\end{exercises}