[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiomdeveloper] Provisos
From: 
root 
Subject: 
[Axiomdeveloper] Provisos 
Date: 
Wed, 26 Jul 2006 20:01:39 0400 
> 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 groundup.
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 provisobased computation automatically forked into
multiple branches.
This also has interestng implications for multithread or
multiprocess 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
 Re: [Axiomdeveloper] Polynomials, abstract objects, provisos, (continued)
 Re: [Axiomdeveloper] Polynomials, abstract objects, provisos, Ralf Hemmecke, 2006/07/29
 Re: [Axiomdeveloper] Polynomials, abstract objects, provisos, Martin Rubey, 2006/07/29
 Re: [Axiomdeveloper] Polynomials, abstract objects, provisos, root, 2006/07/29
 Re: [Axiomdeveloper] Polynomials, abstract objects, provisos, Ralf Hemmecke, 2006/07/29
 Re: [Axiomdeveloper] sbcl and Axiom, Antoine Hersen, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 RE: [Axiomdeveloper] sbcl and Axiom, Page, Bill, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, Alfredo Portes, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 [Axiomdeveloper] Provisos,
root <=
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, Antoine Hersen, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 Re: [Axiomdeveloper] sbcl and Axiom, Gabriel Dos Reis, 2006/07/26
 RE: [Axiomdeveloper] sbcl and Axiom, Page, Bill, 2006/07/27
 Re: [Axiomdeveloper] sbcl and Axiom, root, 2006/07/26
 RNG vs. RING was: Re: [Axiomdeveloper] sbcl and Axiom, Ralf Hemmecke, 2006/07/27
 [Axiomdeveloper] Re: Rng, Martin Rubey, 2006/07/28
 Re: [Axiomdeveloper] Re: Rng, Ralf Hemmecke, 2006/07/28