Re: [Axiom-developer] indefinites

[root]

> On Saturday, June 26, 2004 11:56 PM William Sit
> address@hidden wrote:
> > 
> > Bill Page wrote:
> > > On Thursday, June 24, 2004 2:49 PM you Tim wrote:
> > > >
> > > > The distinction between Integer and Indefinite Integer is quite 
> > > > subtle.
> > > ...
> > However, there should be no disagreement that the two
> > mathematically are equivalent (that is, both obey the same 
> > rules operating on integers) but computationally different.
> >
> 
> I think we need to define more clearly what you mean by
> "mathematically equivalent" and "computationally different",
> but I don't think that I can agree that they are mathematically
> equivalent
.....[snip].....

Integer (INT) and Indefinite(Integer) INDEF(INT) are not categorically
equivalent.  Nor are they computationally equivalent. The algorithms
for working with INDEF(INT) need to work at a symbolic level so that
it knows that given x::INDEF(INT) and y::INDEF(INT) then
(x + y) = (y + x)

The subtle part that I mentioned is (given the subtle nature) harder
to explain. It turns out that the idea of an Indefinite(Integer) 
interacts strongly with another idea called Provisos (a limited
example of which is Maxima and Maple's assume facility).

For example, if we look at manipulating equations that contain only
INTs and INDEF(INT)s we can see the interaction. Suppose we have

 1*x = y*x

and we wish to divide both sides by 'x':

  1*x   y*x
  --- = ---
   x     x

should this be written

  1*x   y*x
  --- = ---   provided [x != 0]
   x     x

but clearly the equation is true even if 'x' is zero. How is the
divide operator supposed to know this? Clearly it can't so the
divide operator has to 'decorate' the result with the Proviso that
[x != 0] for both sides of the equation. However the higher level
operator ('equation divide') knows enough to elide the Proviso.
Or does it? EquationDivide might be able to make this conclusion
over the Integers but what if there are multiple zero-divisors?
Suppose the domain allows a provision that [x^p != 0] when 
dividing both sides of an equation? Can the equation-level divide
conclude that this is true for all x^p? What happens if 'x' is a
Indefinite(Polynomial(Integer)) or Polynomial(Indefinite(Integer))?

Indefinites and Provisos are intimately linked. The mathematics
of Provisos and its interaction with Indefinites, especially when
they are contained in both the equations and the Provisos is a
very subtle topic. 

Provisos, in general, are a hard topic. I've done some unpublished
research on this topic (which I'll try to scrape together and put on
this list so we can review the issues). Many of the manipulations
of Indefinites rely on Provisos for correctness.

Fateman's paper on matricies and Davenport's paper on indefinites
are worth a read.

Tim