[Axiom-developer] Provisos

[root]

> I have a research effort to rewrite the algebra using provisos.
> > This uses the idea of generalized intervals to contain conditional
> > statements that constrain the validity of computations.
> 
> Will all domain  need to be made provisos aware ?
> How will the conditional description be part of the type ?

Provisos are fundamental. If you look at math books carefully
you'll see that quite a few expressions, results, and reasoned arguments
have provisos. Axiom has a way of carrying types but not provisos.

It's a rich research area with very few results.
This was my PhD research and has held my interest for years.

This involves a complete algebra rewrite from the ground-up.
Provisos are fundamental to the whole system. Each Category,
Domain, and object has provisos which limit the validity.

Computation involves reasoning "with" the provisos. That is,
computing with a proviso and an operation like *,

  (1/x provided x != 0) * (1/y provided y != 0)

and computing "in" the provisos which amounts to doing computation
in the "provided" section to combine the results. 

This has implications about forking and combining results so that
you can get answers which have multiple branches, e.g. f(x) can return
         
         --
         |
  f(x) = | x   provided x > 0
         |
         | 1   provided x = 0
         |
         | 1/x provided x < 0
         |
         --

where the proviso-based computation automatically forked into 
multiple branches.

This also has interestng implications for multi-thread or 
multi-process work since you can compute a branch of the 
proviso in parallel and independent of other branches in 
some cases.

Since the provisos can be anything, a whole host of issues
arises. For instance, suppose the proviso reads:

   x provided P in [0,1]

where P is a polynomial? Well, types show up quickly. Is
[0,1] an interval over the reals? Domain matching becomes
an issue since 

   provided P in y

means that 'in' has a type on either side, essentially in(P,y)
and the types have to match. Which raises the issue of conversion
and coercion, which brings us to the Fortenbacher type work.

Handling infinities also arises which brings in the work of
Hansen and Walster on csets.

Handling "indefinites" like 

  x provided x is PositiveInteger

covers the assume facilities in most other systems. You might
be able to compute the type of something but not its value.

And just for excitement the compiler has to know about provisos
so it can decorate the resulting code properly.

This is how I waste my weekends :-)

t