axiom-math
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]