[Axiom-developer] Provisos

[root]

Journaling some comments made at ECCAD 2008:

Re: the symbolic-numeric panel

The question of interval computations arose during the panel discussion.

The panel discussion of intervals revolved around their numeric use.

However, it is perfectly reasonable to consider intervals symbolically.

Consider that most textbooks (assuming they bother) will write:

      1
      -              (provided x \ne 0)
      x

Notice that this can be translated into interval notation as:

      1
      -              [x \ne 0]
      x

Now if this division were to arise in the course of computation
we could "decorate" the whole computation with this proviso.

What is notable about this, however, is that we can continue the
computation in 3 distinct branches:

   branch 1    (1/x [x < 0])
   branch 2    (1/x [x = 0])
   branch 3    (1/x [x > 0])

Similarly, if we later add another proviso to the computation that
restricts x, or another variable y, or a constant, etc we can continue
to add these proviso decorations. Each newly decorated computation is
a "standalone branch". Thus, we might see:

   branch 1.1    (f(x,y) [[x < 0] & [x < y]])
   branch 1.2    (f(x,y) [[x < 0] & [x = y]])
   branch 1.3    (f(x,y) [[x < 0] & [x > y]])

   branch 2.1    (f(x,y) [[x = 0] & [x < y]])
   branch 2.2    (f(x,y) [[x = 0] & [x = y]])
   branch 2.3    (f(x,y) [[x = 0] & [x > y]])

   branch 3.1    (f(x,y) [[x > 0] & [x < y]])
   branch 3.2    (f(x,y) [[x > 0] & [x = y]])
   branch 3.3    (f(x,y) [[x > 0] & [x > y]])

Notice that we can run these branches in parallel because they are
naturally disjoint. Further sub-branches can also run in parallel.
As each branch completes we can combine the branches by doing
logical operations on the provisos themselves.

Thus we may find that only the condition [x > y] has "survived"
and we end up with only the branch x.3 cases. We can reason about
the proviso conditions:

   branch 1.3 & branch 2.3 & branch 3.3 ==>

     (f(x,y) [[x < 0] & [x > y]]) 
   & (f(x,y) [[x = 0] & [x > y]])
   & (f(x,y) [[x > 0] & [x > y]]) ==>

     (f(x,y) [x > y])

So there are computations "with provisos" (e.g. adding decorations)
and computations "of provisos" (e.g. logical operations on decorations).

I did a survey of all of the math books I could reach in several
libraries. About 80% of the conditions on equations can be rewritten
into proviso format, e.g. holonomic ==> [\forall x]

I believe that provisos will provide:

  correct reasoning within computation 
    for instance, it is valid to simplify 
       sqrt(x^2) -> x iff [[x >= 0] & [x \in R]])
    or for handling branch cut assumptions in trignometric cases.

  parallel computations
    since each branch carries the logically independent conditions
    the computation "unfolds dynamically" into "naturally parallel"
    subcomputations. (Stanford just opened a parallel lab and it
    would be worthwhile proposing a "symbolic parallel research"
    area to take advantage of the multicore work with CAS)

  a natural "assume" facility
    the user can decorate any equation with their own conditions
    and these are naturally available (e.g (f(x,y) [x > y])).
    These conditions may only be known from external problem constraints.



Anyway, I wanted to make the point that Provisos are a symbolic form
of interval computation. There is a whole area of research involving
symbolic, logical, and parallel computation (probably with grant money).

Tim