\documentclass{article}
\usepackage{axiom}
\begin{document}
\title{Provisos: A Programming Extension for \\
Conditional Computational Algebra}
\author{Timothy Daly}
\maketitle
\begin{abstract}
Provisos are a method of representing conditional information during a 
computation. This paper motivates the need for provisos and examines
the changes necessary to a computer algebra system to add a proviso
mechanism. In particular, we consider transparency and post-facto
extensions as mechansims for extending classes in an object oriented
system. We consider the classes of proviso information to maintain
during a computation. We consider the computation of the proviso
information and how the proviso information affects the results
obtained. Finally we raise and examine the topic of an algebra of
provisos. 
\end{abstract}
\eject
\tableofcontents
\eject
\section{Introduction}
\subsection{What is the motivation?}
If we examine the mathematics literature there are many instances of
formulas where we find the information about the formula structured:
\begin{verbatim}
Given these assumptions
then we have the formula
provided these restrictions
\end{verbatim}
\noindent
The "given" portion of the equation is usually embedded as text in the
paragraph preceeding the formula. This information includes many
assumptions that restrict the domain of interest, such as:
\begin{verbatim}
assume x is real ...
\end{verbatim}
\noindent
The formula portion states the conclusion the author wishes to draw.

The "provided" portion of the statement contains certain restrictions
that limit the applicability of the formula or constrain the truth of
the answer. These generally are of the form:
\begin{verbatim}
x = 0
\end{verbatim}
\noindent
if the restriction can be stated as a formula or they are written in
paragraph form if there is no notational conventions for writing the
restrictions. As a particular example we have:
\begin{verbatim}
Given x is real then
the integral of 1/x is abs(log(x))
provided x != 0
\end{verbatim}
\noindent
We will refer to this example as "the integration example" throughout
this paper..

Most computer algebra systems (hereafter CAS) attack this problem by
simply ignoring it. This is somewhat reasonable for single
computations where it leaves open the potential for misleading the
user but still giving reasonable answers. The problem arises when the
results are used in further computations. If, in further computations,
the domain of interest includes places where the assumptions or
restrictions make the formula invalid the results can be completely
wrong.

So we would like to build a system that carries this auxillary
information with a computation and modifes the results based on this
information. We call the auxillary information a {\bf proviso}. The
class of all such things is called the Proviso domain.

In this paper we will examine other approaches to the problem and then
present the approach we have taken.
\section{What is the problem?}
\begin{list}{}
\item global info reasoning across scopes/levels?
\item (depth issue) 
\item cross-branch information?
\item (breadth issue) 
\item fundamental issues
\end{list}
\subsection{Representation}
How provisos are represented affects the ability to reason with the 
information

Prior systems have implemented the representation as a global table of
facts. We feel that proviso information can occur at many levels in a
computation and that this information should be scoped relative to its
point of application. Thus, each object in the system should carry its
own proviso information.
\subsection{Control}
A single computation can generate multiple answers. This implies that
the computation must be carried on for each branch and that the state
of each branch must be maintained separately.
\subsubsection{Of}
\begin{list}{}
\item What information should be kept in a proviso? (meromorphic?)
\item What should be added? (global/local)
\item When can it be removed? (invalidated?)
\item When can it be ignored? (matrix inversion)
\item How do we combine this information (combinatorial explosion)
\item How do we compute this information (algebra of provisos)
\end{list}
\subsubsection{With}
\begin{list}{}
\item How should the proviso information interact with a computation?
\end{list}
\section{Representation: What is the language issue?}
\subsection{Transparency}
In an Axiom system every object has a type which defines the
operations that can be performed on the object. The operations are
exported by the class, referred to as a "domain" in Axiom. To see the
problem with Axiom's type system, which is typical of most type
systems, look at an operation from the type Polynomial.

Consider additions, which is an operation with the signature:
\begin{verbatim}
+(a:Symbol, b:Symbol) : Polynomial
\end{verbatim}
that is, '$+$' takes a symbol and a symbol and symbolically adds them,
returning a polynomial. The simple transformation that allows one to
produce an object of type Proviso would be to create a domain called
PROVISO and introduce an operation called ``new'' that takes a symbol
and returns a new PROVISO object, thus:
\begin{verbatim}
Proviso: Domain with
 { new:Symbol -> %
   +: (Symbol, Symbol) -> Polynomial;
   assume: (Symbol, Condition) -> %;
 }
\end{verbatim}
\noindent
then one could create objects of type PROVISO and operation on them
with the '$+$' operation from the PROVISO domain, thus:
\begin{verbatim}
x:=new('x)
y:=new('y)
z:=x+y
\end{verbatim}
\noindent
this approach would work but has the fundamental flaw that all of the
operations we wish to perform must be exported from the domain
PROVISO. Since provisos are intended to be a wrapper around other
types we get an explosion of the number of operations we need to
export from this domain. Essentially our type system collapses into
one type, PROVISO. This is unacceptable. Ideally it should be possible
to construct a wrapper type that has a property we refer to as
"transparency". Transparency would allow a type to be extended in both
functions available and representation. This extended type would
behave like the original type in all normal contexts. That is, unless
an operation is ``proviso-aware'' there is no need for another
operation to be aware that they are operating with a proviso. Such a
transparent domain would act exactly as a member of its component
domain except for proviso-related operations. Thus, declaring a symbol
to be a proviso object would have the effect of adding another slot in
its representation to carry the proviso information. This is similar
to the notion of a variant record in a strongly typed Pascal system.
\subsection{Post-Facto Extensions}
In Axiom it is possible to extend an existing domain to add operations
to the domain. Thus, one would write the following code:
\begin{verbatim}
extend Polynomial: Domain with
 { assume: (Symbol, Condition) -> %
 }
\noindent
which has the effect of adding the additional function "assume" to an
existing domain Polynomial. As far as we are aware, post-facto
extensions of classes only exists in the Axiom system.

Even so, this mechanism is not sufficient to support provisos because,
while extensions can add functions, they do not change the
representation of the object. Provisos require that the object
representation be extended to include space for the proviso
information.

Thus, in lieu of a full extension facility the approach we've take is
to rewrite the domains that are proviso-aware to carry the extra
proviso information as part of their data structure. The down side of
this approach is that additional memory will be allocated even if
provisos are never used. In the research prototype of the system this
is considered a reasonable tradeoff.
\subsection{Of: How do we compute proviso information?}
There is an issue about global versus local information.

Consider an apparently simple case. It seems obvious that every time a
division is performed one should add a proviso that the denominator of
the returned ratio should not be zero. This a a fairly straightforward
change to the system. We need only change the division routine to add
this information.

Consider the effect of this change. When we do a division we now know
that we made an assumption that the denominator cannot be zero. Thus,
we can check this condition later and avoid situations that violate
this assumption.

However, if we consider the domain of matrix computations we find that
there are two algorithms that will compute the determinant of a
matrix. One, gaussian elimination, uses division in the
computation. Using this algorithm the final result will contain
restrictions on the values of various variables. However, if we use a
different algorithm that is division free (?ref) then we will get the
same result but without the restrictions.

There are several solutions to this problem.

First, we could have a division routine check for a special proviso
property, say 'zero-free' which means that the division routine should
not add its assumption.. This places global knowledge within the
division routine. Of course, if the range of the variables is known
never to include zero then the division routine would not add the
provisos in the first place. In general, it seems to be unreasonable
for the low level division routing to know higher level information.

Second, we could have the higher level algorithm remove the various
assumptions added by the division routine. However, some of these
assumptions may have been added by other routines for other
reasons. This means that the global routine must know what provisos
will be added to the result, where they came from, and how they might
have been combined with other profisos in the course of the
intermediate computaiton. In general, it seems to be unreasonable that
a high level routine be aware of the possible combinations of provisos
in lower level routines.

Third, we could ignore the problem and claim that the provisos belong
there because of the algorithm chosen. For the purpose of this work
the third approach is taken.
\subsection{Of: Algebra of conditions}
Having decided how to handle the issue of global versus local
information we need to look at the computation of provisio information
as a domain of its own.

What kinds of information resides in a proviso?

An examination of the mathematics literature shows what appears to be
a wide range of possible conditions. However, a large number of these
can be captured in one or two froms, either as a symbol representing
type and/or property information or as an interval statement such as
$x \in [0..10]$. Intervals can be symbolic or numeric.

How do we combine this information in meaningful ways?

Wiebel and Bonnet (?ref) have developed an algebra of properties. Such
work is necessary to put the algebra of provisos on a firm theoretical
footing.

Because we've reduced the proviso information we consider to two
classes we have only to consider how to combine information within
these two classes. The question of combinding intervals in meaningful
ways is a question of set membership and the mathematics is
well-defined. If the endpoints of the intervals are numeric then
interval arithmetic is appropriate (?ref).

Symbolic property information is considered static but can be combined
with other information. How this combination is done is dependent on
the meaning of the symbolic information. For example, one could say
that a function $f(x)$ is continuous on the interval $[0..)$. For now
we consider symbolic information to be a separate domain and defer the
issue of combining symbolic information with interval information.
\subsection{With: How does proviso information interact with the
computation?}
\section{Prior Approaches}
When this problem has been attacked in other systems the effort has
been to create an ``assume'' facility. This allows one to make global
statements about the restrictions or assumptions to be placed on an
object. Thus, one would perform a computation assuming $x > 0$.
\section{What have others done?}
\subsection{Dynamic Questions}
Macsyma will perform a computation and when it needs to answer a
question it constructs a question and asks the user. While this seems
like a reasonable approach the problem is that the user can be asked
questions that may be stated in terms of variables that don't occur in
the original statement of the problem or be asked a question for which
the user has no answer. So one might get a question like: $is x > 0?$
where $x$ does not occur in the input equation. The generic approach
taken by users seems to be ``just say yet''.
\subsection{Carry Forward}
In the carry forward approach one uses functions such as signum or
other ``lazy'' mechanisms to continue the computation. Maple uses the
signum function to delay the binding of parameters until the final
result. Once the sign of the parameter is known the signum function
can be replaced by the sign of the parameter times 1 (or, in general,
the unit). The problems with this approach are that sometimes the
signum of a parameter is neither positive nor negative but zero. Then,
instead of a positive or negative 1 multiplier, we should use 0. This
could be fixed by using a different ``signum'' function. The second
problem is related to the solution of the first in that we need to be
able to create these special functions that have definitions which
depend on the parameters and can participate in the computation but
are ``lazy'' in their decisions. This is very difficult to do in
general.
\subsection{Depth First}
Depth first is an approach that uses a top-level control strategy and
a stack of decisions. Each decision point puts the other possible
choices on a stack and, when the computation returns to the choice
point, it is restarted with the next stacked decision. Depth first has
several problems, the most serious from a semantics point of view is
the confusion of provisos-for-decision vs provisos-for-control. When
we ask a question do we want to decide the answer (is $x > 0 \ldots$
yes) or do we want to split the answer into several cases and take
each branch? Another serious problem is that we need a general
backtracking control mechanism which exists over the top of the
computation. If the proviso information is ``discovered'' during the
computation that is performed without the top-level backtracker
running then the other branches could fall on the floor.
\subsection{Frames}
Frames introduces the idea of multiple name spaces. Axiom currently
supports frames. The variable $x$ could have one value in one frame
and a variable $x$ could have another value in another frame. They
both have the same name but are distinguished by the name space in
which they reside. Such an idea occurs in systems like common lisp
where symbols live in ``packages''. Frames introduce a method of
carrying the information needed in a very weak sense but do not
address the control issue in any way.
\subsection{Threads}
Threads are a very low level operating system dependent attack on the
problem. One cold create a new thread of computation at every branch
point using a call to the operating system. Each fork of the
computation would compute in parallel with different values of the
parameter.

Since each fork is a complete copy of the computation we have
certainly solved the control issue. It is not clear how the various
branches of the computation are to be joined together. This approach
is at such a low level that it makes it difficult to see how to change
the computation to take advantage of such a mechanism.
\subsection{Continuations}
Continuations are a mechanism that could be used to solve portions of
the proble, as evidenced by Gomez-Dias's work. One problem is that
such a solution depends on the underlying mechanism only available in
the Scheme language, called continuations. Continuations allow one to
get hold of the root of the enclosing $IF$ construct so that the test
result can be recomputed.

The problem is that the proviso is being evaluated as a side-effect of
the test condition of the $IF$ statement. Each proviso is reaching up
to the containing $IF$ to save state information. Continuations
provide the appropriate control mechanism if every provios implies a
branch (provisos-for-control). However they are note appropriate to
cases where the proviso simply adds additional information or
restrictions (provisos-for-decision).
\subsection{``NIF''}
This approach involves redefining the semantics of the $IF$ statement,
referred to as the {\bf New IF} or {\bf NIF} statement. There are two
ways of accomplishing this task. The first is to rewrite every
interesting $IF$ statement into a $NIF$ statement. Such an approach is
feasible if tedious. The second is theoretically more interesting. One
could define a domain called $NIF$ and have it export the $IF$
operation with a signature something like:
\begin{verbatim}
IF: (text, statement, statement, statement) -> result
\end{verbatim}
\noindent
so that there was a 3-way, or in general, $N$-way $IF$
statement. While there is not theoretical reason why $IF$, $GOTO$, and
other statements can't be viewed as functions and redefined by the
user it appears that object-oriented compiler technology is not up to
the task.
\subsection{Assume}
One approach is to assume a particular answer and evaluate the result
under that assumption. This has 2 problems, the first being that we
have to pre-assume certain results which we may only know we need the
answers to during the computation. The second is that we will get a
single result from the computation, the assumed result. 

Also assumes that happen before a computation must be global as the
objects that they refer to may not be in existence at the time they
are done so there is no place to put the assumed information except in
a global table.
\subsection{Rewrite}
One could change the algebra functions to know about provisos. This is
a large task but seemingly the only feasible solution if one wishes to
do more than just build a global assume-style facility.
\section{Provisos}
There is also the general problem of cross-branch information. Facts
from one branch can affect further computations in another branch.
\begin{list}{}
\item what is the proposed solution?
\item what is a proviso
\item how does this solve the problem?
\end{list}
\section{Proviso Information}
\begin{list}{}
\item what information could we maintain?
\item what information should we maintain?
\end{list}
\section{Implementation}
\begin{list}{}
\item how do we maintain that information?
\end{list}
\section{Computation of Provisos}
\begin{list}{}
\item how do we compute the proviso result of an operation?
\end{list}
\section{Computation with Provisos}
How does the proviso information affect the computation? There are two
uses of proviso information. The first use is to answer symbolic
questions. For example, we might want to be able to simplify a square
root such as $\sqrt(x^2)$. We could do this simplification if we knew
that $x$ was real. If $x$ were complex then the simplification is not
valid in general since $x^2 = -1$ if $x$ is $i$.

The second use for provisos is in contructing continuations. Consider
the question:
\begin{verbatim}
if x = 0
\end{verbatim}
\noindent
we could have 4 possible answers:
\begin{verbatim}
{ x < 0, x = 0, x > 0, unknown }
\end{verbatim}
\noindent
and, as a result, there are 4 possible continuations of the
computation. If the computation were broken up at this point we could
continue each branch of the computation with a proviso attached to
each branch restricting the result to the case we assumed. Thus, there
would be 4 continuations generated at this point in the
computation. Of course such a branching/continuation model assumes
some control mechanism is in place. The simplest and most elegant
control mechanism is to use continuations as they are implemented in
Scheme. These would allow multiple returns from an $IF$ statement, one
for each possible path. This approach was used by Gomez-Dias.

Alternatively one could use a backtracking control mechanism and keep
a stack of the possibilities. Yet another approach, used by Duval, is
to repeat the entire computation choosing different paths each time
through. 

There are many issues involved in repeating a computation in each of
these choices, not the least of which is that some steps in the
computation could de-allocate the storage in use for one of the
instances of an object causing disasterous results if the object is
reused in a repeated computation. This is an instance of the general
problem of side-effecting functions (such as storage allocation).
\section{Examples}
\subsection{Assumptions}
There are examples where we make statements about the valid ranges of
the variables before we do the computation.
\subsection{Computed Assumptions}
These are examples were we make statements about the valid ranges of
the variables from an analysis of the equation prior to the
integration.

In this example we can analyze the denominator to find that there is a
zero in the range of the integral. We can compute the result but need
to attach a proviso about when the result is valid.
$$integrate(1/x,x=0,\infty)$$
\subsection{Derived Assumptions}
These are examples where we make statements about the valid ranges of
the result from an analysis of the equation after the integration. In
this example we have an integral which diverges for a given value of
the parameter:
$$integrate(1/(x-2), x=0,\infty)$$
\noindent
The more general case has 2 answers, $1/a$ if $a > 0$, else divergent:
$$integrate(1/(x-a),x=0,\infty)$$
\subsection{Symbolic Numbers}
In the field of Numerical Polynomial Algebra there are many instances
where numeric computations suffer the problem of {\sl intermediate
cancellation}. For example, when computing with numeric polynomials 
the coefficients are sometimes only known to a finite precision. 
During matrix elimination we compute differences of polynomials which
may lead to a polynomial with ``tiny'' coefficients. There
are generally two cases that occur, either only one of the coefficients
becomes small or all of the coefficients become small.

Since the precision of the coefficients is only specified to a couple
decimal places the notion that a coefficient is small means that we
have gone below the bounds of known precision. In some cases it is
reasonable to assume that a small coefficient is identical to zero
and we can elide the term. If all of the coefficients are small it
may be reasonable to elide the whole polynomial.

In other cases the 'small' value may be due to {\sl intermediate
cancellation}. In this case the order of the operations becomes
important. For instance, if we know that a number N is known to 
two decimal places we can divide it by $1^6$ which will make it appear
to be so small that it is essentially zero. However we could later
multiply it by $1^6$ which will bring it back into range. In that case
it would be incorrect to assume the term has vanished. 

Using infinite precision arithmetic this may not be a problem. However
if we are using machine floats it may be the case that we create such
small numbers that we ``underflow'' the range losing significant digits.
In this case the remaining digits are noise and the multiplication can
magnify the noise to the point where it overwhelms the computation.

Instead we introduce the idea of a {\sl symbolic number}. A symbolic
number is an ordinary number wrapped in a proviso. Operations on the
number that could potentially lose significant digits are not carried
out directly but added to the proviso. At the final stage of the 
computation the operations stored in the proviso are carried out in
the order which preserves the maximum number of significant digits.

Thus, in the example given, if we take $0.01$ and divide it by $1^6$ we
delay the computation by forming a symbolic number 
\[\{0.01 {\rm\ pending\ division\ by\ }1^6\}\]
Later, when we encounter the multiplication we form another proviso
\[\{\{0.01 {\rm\ pending\ division\ by\ }1^6\}{\rm\ pending\ multiplication\ by\ }1^6\}\]
which we can immediately reduce to 
\[\{0.01{\rm\ provided\ true]}\]
which can be coerced back to a normal number
\[0.01\]
\subsection{Indefinite Integers}
\section{Conclusions}
\section{package PROVISO Provisos}
<<package PROVISO Provisos>>=
)abbrev package PROVISO Provisos
++  Author: Timothy Daly April 1995
@
<<*>>=
@
\eject
\begin{thebibliography}{99}
\bibitem{1} Bellman, R., Cooke, K.L.
{\sl Asymptotic behaviour of solutions of differential-difference
equations}
Mem. Amer. Math. Soc. 35 (1959)
\bibitem{2} Bellman, R., Cooke, K.L. 
{\sl Differential-difference equations}
Academic Press, New York (1963)
\bibitem{3} Feldstein, A., Iserles, A.
{\sl Numerical Methods for neutral equations with monotone delays}
To appear.
\bibitem{4} Fox, L., mayers, D. F., Ockendon, J. R., Tayler, A. B.,
{\sl On a functional differential equation}
J. Inst. Maths Applics (1971) 8, 271--307
\end{thebibliography}
\end{document}