axiom-math
[Top][All Lists]

## [Axiom-math] provisos and indeterminates

 From: daly Subject: [Axiom-math] provisos and indeterminates Date: Thu, 19 May 2005 22:45:35 -0500

```The proviso work is all in paper form in a pile and now in a
packed box. I'll see if I can guess which one it is but I'd
rather not unpack the world until after the move. I really should
keyboard this stuff. I did it before the net was all the rage and
the paper is just rotting away now.

the proviso idea is fundamental to math but ignored or treated badly
by all computer algebra systems. provisos arise in things like:

1
---   provided x != 0
x

it turns out that a deep investigation of the subject yields a
few insights.

1) provisos have two different forms of mathematics
a) computing WITH provisios (e.g what is (1/x)*(1/y))
b) computing IN provisos (e.g. what is (provided a>0)*(provided a<0))

2) provisos contain general branching
it is possible to have a computation (such as the above)
break into parts (e.g. x<0, x=0, x>0) at every stage of
the computation. this necessitates general control structures
such as backtracking, stacking, early cutoff, etc. I have
identified 8 different possible forms.

3) most proviso forms can be reduced to intervals (an unpublished result)

4) provisos are a poorly studied area of math but vital for understanding
computational mathematics.

As for the indeterminates (now called indefinites) this is a currently
funded NSF project at CCNY. There are no papers available yet. The basic
idea is to examine questions like:

if p and q are polynomials
we know what the third term of p^3 * q^4 is
but what is third term of p^n * q^m?

if M is a matrix and n is an indefinite integer
what is the general term for M_{i,j} in M^n

normally in a computer algebra system,
given n+1
we presume n is of type 'variable' and 1 is of type 'integer'
we promote both n and 1 to type 'polynomial(integer)'
we choose '+' from polynomial(integer)
and the result is that n+1 is of type polynomial(integer).

but suppose 'n' is an "indefinite integer"
then we can construct n+1 where '+' comes from indefinite(integer)
and the result is that n+1 is of type indefinite(integer)
so we can use this new thing where integer is expected
and construct things like polynomial(indefinite(integer))

does the 'indefinite' type propagate? do we get
indefinite(polynomial(indefinite(integer)))?

The two subjects are deeply related and very poorly studied.
They are both fundamental to computational mathematics.

Axiom is the perfect platform for doing this kind of research.
It has a 'suchthat' type which was my first attempt at this
but I've come to understand that the issue is more fundamental.

Tim

```