% ----------------------------------------------------------------
% AMS-LaTeX Paper ************************************************
% **** -----------------------------------------------------------
\documentclass[10pt]{article}
\usepackage{graphicx}
\usepackage{program}
\usepackage{ifthen}

\setlength{\textheight}{8.75in}
\setlength{\textwidth}{6.5in}
\setlength{\oddsidemargin}{0in}
\setlength{\evensidemargin}{0in}
\setlength{\topmargin}{-0.75in}

\newtheorem{algorithm}{Algorithm}
\newtheorem{note}{Note}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}

\newcommand{\sign}{\mbox{sign}}
%\usepackage{graphics}
% ----------------------------------------------------------------
\vfuzz2pt % Don't report over-full v-boxes if over-edge is small
\hfuzz2pt % Don't report over-full h-boxes if over-edge is small
% THEOREMS -------------------------------------------------------

\input{flatex}

% ----------------------------------------------------------------
\begin{document}

\title{Deriving a very simple FLAME algorithm}

\author{
Robert van de Geijn
}%

\date{Draft \\
\today}
\maketitle
% ----------------------------------------------------------------

% ----------------------------------------------------------------

Given a vector of $ n $ numbers
\[
x = \left( \begin{array}{c}
  \chi_0 \\
  \chi_1 \\
  \chi_2 \\
  \vdots \\
  \chi_{n-1}
\end{array}
\right)
\]
the sum of those numbers is given by 
\[
\alpha = \sum_{i=0}^{n-1} \chi_i
\]

\begin{note}
We use lower case letters for vectors and lower case Greek letters for scalars.
\end{note}

\input{blank_ws}

Let us define the operation to be performed by
\[
\alpha \becomes \mbox{Sum}( x ). 
\]
We will derive an algorithm for computing $ \alpha $ by filling out the worksheet in Fig.~\ref{fig:ws}.

\begin{note}
Read this as ``$ \alpha $ becomes the sum of the elements of vector $ x $''.
\end{note}

\begin{note}
Notice that we carefully distinguish between ``$=$'' which indicates equality and ``$\becomes$'' which indicates assignment.
\end{note}

\begin{note}
Below, the step numbers refer to the numbers in the ``Steps'' column on the left in Fig.~\ref{fig:sum}.
\end{note}

\input{sum_ws}

\paragraph*{Step 1: Precondition and postcondition}

Letting $ \hat{\alpha} $ denote the original contents of
$ \alpha $,
the precondition (state of the variables at the beginning),
$ \PPre $,
for our algorithm will be 
$ \alpha = \hat{\alpha} $ while the postcondition, $ \PPost $, 
(state of the variables upon completion) is that
$ \alpha = \mbox{Sum}( x ) $.
This is indicated in Steps~1a and~1b in Fig.~\ref{fig:sum}.

\paragraph*{Step 2: Determining loop-invariants}

As part of the computation of $ \alpha $ it is logical
to sweep through $ x $ in a consistent manner, e.g. from top to bottom.
Our notation captures this by partitioning $ x $
like
\[
x 
\rightarrow 
\FlaTwoByOne
  { x_T }
  { x_B }
\]
where $ x_T $ and $ x_B $ represent the top and bottom part of the
vector.  

\begin{note}
Read $ x_T $ and $ x_B $ as ``x-Top'' and ``x-Bottom'', respectively.
\end{note}

\begin{note}
The idea is that each of the two parts of $ x $ at a given state of the
algorithm has been updated or used in some (typically different) fashion.
For example, we will see next that 
elements of $ x_T $ have already been summed into 
$ \alpha $ while elements of $ x_B $ have not.
\end{note}

Next, we take this partitioned vector $ x $ and substitute it into the 
postcondition to find that
\[
\alpha = \mbox{Sum}\left( 
\FlaTwoByOne
  { x_T }
  { x_B }
\right).
\]
Manipulating this we notice that
\[
\alpha = 
\mbox{Sum}( x_T ) + 
\mbox{Sum}( x_B ).
\]

\begin{note}
The above equality shows how $ \alpha $ can be computed from the two
separate parts of $ x $.
\end{note}

Notice that the loop-invariant, $ \PInv $, is a predicate that indicates the
state of the variables (in this case $ \alpha $) at the top of the 
{\em while} loop in Fig.~\ref{fig:sum}.  Notice that the loop computes
$ \alpha $ and thus at the top of the loop we would expect to have 
computed only some of the final result.
For example, at the top of the loop, we may indicate the contents of
$ \alpha $ as
\begin{equation}
\label{eqn:var1}
\PPre : \alpha = \mbox{Sum}( x_T ).
\end{equation}
This condition is now entered in the worksheet in Fig.~\ref{fig:sum} in 
four places:
\begin{enumerate}
\item
At the top of the loop-body.
\item
Before entering the loop.  
The idea is that the first time through the loop,
$\alpha $ contains exactly what it contained before entering the loop.  Thus, the loop-invariant must already be {\em true} there.
\item
At the bottom of the loop-body.
The idea is that no computation happens between the bottom of the
loop-body and the next time the top of the loop-body is reached.
\item
Upon completion of the loop.
\end{enumerate}

\paragraph*{Step 3: Loop-guard}

Notice that upon completion of the loop
\begin{itemize}
\item
The loop-invariant is {\em true}.
\item
The loop-guard $ G $ is {\em false}.
\item
The condition
\[
\left( 
   \alpha = \mbox{Sum}( x_T ) 
\right)
\wedge 
\neg G
\]
must imply that $ \alpha = \mbox{Sum}( x ) $.
\end{itemize}
Notice that {\em if} $ x_T $ is all of $ x $, then this is the case.
So, if we take $ G : n( x_T ) \neq n( x ) $ (read as: the length of 
$ x_T $ is not the same as the length of $ x $) then
$ \neg G $ means that $ n( x_T ) = n( x ) $ and therefore
\[
\left( \left( 
   \alpha = \mbox{Sum}( x_T ) 
\right)
\wedge 
\neg G
\right)
\Rightarrow
  \left( \alpha = \mbox{Sum}( x ) \right)
\]

This argument determines the required loop-guard $ G $ that appears in the
worksheet.

\paragraph*{Step 4: Initialization}

Next, we must find an initialization, $ S_I $, that has the following properties:

\begin{itemize}
\item
No computation is performed.
\item
The initialization changes the contents of $ \alpha $ so that the
loop-invariant is satisfied.
\end{itemize}

We note that if we partition
\[ 
x \rightarrow 
\FlaTwoByOne
 { x_T }
 { x_B }
\]
where $ x_T $ has {\em no} elements (and hence $ x_B $ is all of $ x $)
{\em and} 
we set $ \alpha $ equal to zero ($ \alpha \becomes 0 $), 
then we put the
variables $ x_T $, $ x_B $, and $ \alpha $ in a state where the loop-invariant is satisfied.
This initialization appears in Step 4 in Fig.~\ref{fig:sum}.

\paragraph*{Step 5: Progressing through the vector}

We now note that as part of the computation $ x_T $ starts by having
no elements, but must ultimately equal all of $ x $.
Thus, as part of the loop elements must be taken from $ x_B $ and 
added to $ x_T $.
This is denoted in Fig.~\ref{fig:sum} by the statements
\[
\FlaTwoByOne
 { x_T }
 { x_B }
\rightarrow
\FlaThreeByOneB
 {x_0}
 {\chi_1}
 {x_2}
\]
and  
\[
\FlaTwoByOne
 { x_T }
 { x_B }
\leftarrow
\FlaThreeByOneT
 {x_0}
 {\chi_1}
 {x_2}.
\]
This notation simply implies that the top element of $ x_B $, 
$ \chi_1 $, migrates from $ x_B $ to $ x_T $.

\paragraph*{Step 6: Determining the state after repartitioning}

The repartitioning in Step 5a does not change the contents of
$ \alpha $: it is really just an indexing operation.
We can thus ask ourselves the question of what the contents of
$ \alpha $ are in terms of the exposed parts of $ x $
($ x_0 $, $ \chi_1 $, and $ x_2 $).
We can derive this condition, $ \Qbefore $, via {\em textual substitution}:
The repartitioning in Step 5a means that
\[
\FlaTwoByOneNoPar
{ x_T = x_0 }
{ x_B = 
  \FlaTwoByOneSingleLine
     { \chi_1 }
     { x_2 }
}.
\]
If we substitute the quantities on the right of the equalities into
the loop-invariant we find that
\[
\alpha = \mbox{Sum}( x_T )
\]
implies that
\[
\alpha = \mbox{Sum}( x_0 )
\]
which is entered in Step 6 in Fig.~\ref{fig:sum}.

\paragraph*{Step 7: Determining the state after moving the double lines}

Next, we notice that the moving of the double lines in Step 5b
means that now 
\[
\FlaTwoByOneNoPar
{ x_T = 
  \FlaTwoByOneSingleLine
     { x_0 }
     { \chi_1 }
}
{ x_B = x_2 }.
\]
Since the loop-invariant must be true after this redefinition
of $ x_T $ and $ x_B $, 
we substitute the quantities on the right of the equalities into
the loop-invariant we find that now
\[
\alpha = \mbox{Sum}
\left(
  \FlaTwoByOne
    { x_0 }
    { \chi_1 }
\right)
\]
which implies that
\[
\alpha = \mbox{Sum}( x_0 ) + \chi_1.
\]
This is entered for $ \QAfter $ in Step 7 in Fig.~\ref{fig:sum}.

\paragraph*{Step 8}

Comparing the contents in Step 6 and Step 7 now tells us that
$ \alpha $ must be changed from equalling only $ \mbox{Sum}( x_0 ) $ to
equalling $ \mbox{Sum}( x_0 ) + \chi_1 $.
We conclude that it must be updated by adding $ \chi_1 $ 
(since it already equals $ \mbox{Sum}( x_0 ) $):
\[
\alpha \becomes \alpha + \chi
\]
which is entered for $ S_U $ in Fig.~\ref{fig:sum}.

\begin{quote}
\em
{\bf Exercise 1.}
Derive an algorithm for computing $ \alpha \becomes \mbox{Sum}( x ) $
by picking the loop-invariant as
\[
\alpha = \mbox{Sum}( x_B )
\]
\end{quote}

\end{document}