Re: [Axiom-developer] indefinites

[William Sit]

Bill Page wrote:
> 
> Tim,
> 
> On Thursday, June 24, 2004 2:49 PM you wrote:
> >
> > The distinction between Integer and Indefinite Integer is
> > quite subtle.
> 
> I really don't see it as much more subtle than high school
> level algebra. For example, it is not difficult to imagine
> assigning a problem such as: Let x be a positive
> integer, show that 0^x = 0.

Whether the distinction is subtle or not is subjective. 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.

Bill continues:

> In the Axiom book p. 24 the expression x:Integer is called
> a "declaration" and says only that it restricts the values
> that can be assigned to the variable, certain not that it
> is no longer a variable simply because we have declared a
> type! That's why I found Axiom's behaviour very surprising.
> 
> The glossary of the Axiom book, p. 715 defines 'variable'
> as follows: "a means of referring to an object, but not an
> object itself...". Therefore it also seemed quite surprising
> and inconsistent to me that when no declaration has been
> made for x, I saw the Axiom output
>    x
>                   Type: Variable x
> 
> which treats x as an *object* of type Variable.

The double meaning of "variable" is unfortunate. The above paragraph should have
used the term "identifier" instead of "variable". "Variable" should be reserved
for the domain constructor, and symbols used in polynomials should be referred
to as (algebraic) indeterminates.

An "indefinite", the way Tim and I use it, is not the same as an indeterminate.
It is a what Davenport called an "unknown" and is simply a place holder for a
(perhaps never) to-be-assigned value of a certain type (say integer). An
indefinite, ideally, may be used wherever an integer may be used in Axiom. The
problem of how to implement something like
  Do (body of loop) for i in 1..n
where n is an indefinite integer is not straightforward. Fateman's article
discusses possible implementation strategies.

Bill continues:

> > > It seems to me that it should be quite simple to provide
> > > symbolic overloading for almost all operations but do we
> > > really want
> > >
> > >   x+1
> > >
> > > to be of type Indefinite Integer as you suggest above?
> > > Axiom already has several possible types for this.
> [Tim's response]
> > Axiom has the machinery to handle this but no types that
> > handle it. That's the point of the research questions raised
> > by Davenport, Fateman, Sit, and myself (and probably others
> > I've yet to discover).
> 
> To tentatively answer my own question above, I think that we
> do not want the expression
> 
>   x+1
> 
> to be of type Indefinite Integer. If x was coercible to type
> Variable then it would simply be of type Polynomial Integer as
> before. But if the domains such as Polynomial and Expression
> could know that x was declared as say PostiveInteger then it
> could do things like evaluate
> 
>   0^x
> 
> as
> 
>         0 [corrected typo]
>                               Type: PositiveInteger
> 
> even though x has no assigned value.

EXPR INT is one way to handle the indefinites but as your example shows, it is
not thorough. Sure we can easily modify EXPR to handle this example. Note this
works only when x has not been declared to be of type Integer, so the
interpreter can treat x as a Symbol and coerced it first to POLY INT then to
EXPR INT.
An example of where this has been done is
   binomial(x,x)
Axiom will give 1 when x is undeclared and unassigned. This works because the
CombinatorialFunctions was designed to work within EXPR INT, AND the coercion of
x to EXPR INT succeeds.

> To do this, I think we need to extend the Variable domain to
> allow, for example, the following domain constructor
> 
>   Variable(PositiveInteger,x)
> 
> Then the declaration
> 
>    x:PositiveInteger
> 
> should default to
> 
>       x
>                      Type: Variable(PositiveInteger,x)
> 
> and most of the rest of Axiom would be unaffected except for
> some additional evaluations in those domains involving variables
> that can make use of the additional type information.

The Type ANY is very similar to what you suggested above. However, as currently
implemented, the interpreter flags any object which has not been assigned a
value in any function call as an error. So I don't know if we can define a
function that would not be flagged to produce Variable(PositiveInteger,x) if x
has no value but has been declared to be of some type.

Precisely because of this "restriction" or "feature" (which is reasonable given
the current paradym of symbolic computation), to allow such a coercion requires
a new implementation (namely, to create a value when there is none --- and the
natural choice is similar to how an undefined (AND undeclared) symbol x is
handled as Variable x --- the difference being that in the case of an
indefinite, x IS declared.

Declaration is of paramount importance in the world of indefinites. For example,
we may want to be able to compute the way we do in mathematics: Let  p be a
polynomial of degree m > 0. Then dp/dx is a polynomial of degree m-1. Here we
want p to be an indefinite polynomial in one variable x and m be an indefinite
positive integer. So we would like to be able to do:

  p: Indefinite DMP([x],INT)
                              Type: Indefinite DMP([x],INT)
  m:= degree p
                              Type: Indefinite NNI
  degree D(p,x)
    m-1                       Type: Indefinite NNI

(there may need be provisos on m, but let's ignore that for now). Eventually,
when this is operational, neither the input nor the output need to use the word
"Indefinite" (which is needed only internally: so every declaration without an
accompanying assignment will belong to the indefinite domain; an object of the
indefinite domain can be "assigned" a value and be "retracted" to the domain,
all transparently done. This may suggest a simple method is to put a tag on the
object, whether it has been assigned a domain value or not. This would probably
work for a while until we want to go to more abstract levels such as computing
with indefinites like p+q. The code for the underlying domain will be so messed
up with conditionals that it may be wiser to separate the domain from its
indefinite version. After all, we separate the domain INT from POLY INT. Fateman
has some good suggestions to use lazy evaluation techniques to hold the
proliferation of conditionals and handle indefinite loops.

However this is done, the representation of the indefinite integer x will be
different from the representation of an integer x that has not been assigned a
value (indeed, the latter does not yet have one). This necessary change in
representation causes all the operations involving integers to be syntactically
invalid on indefinite integers.

Bill continues:

> [Tim wrote:]
> > ... symbolic computation systems do very little "symbolic"
> > computation ...
> 
> I don't think that this has anything directly to do with strict
> typing. It seems to me that the way that Axiom implements strict
> typing (specifically: no typed variables) makes this sort of
> "symbolic" computation more difficult. And my counter claim is
> that other systems have more functionality in this regard than
> Axiom, but I agree that they do this through means other than
> strict typing. For example, Maple has the "assume" facility,
> e.g.
> 
>   assume(x,posint);
> 
> that interacts with many other different symbolic operations.
> 
> And I want to repeat for emphasis that even without any form
> of typing, systems like Reduce have been used to implement
> purely symbolic operations on tensors and differential forms
> that, for some applications, are much more powerful than
> manipulating the underlying (coordinate) representations of
> these objects.

Can you give some such examples? (for discussion's sake).

William