RE: [Axiom-developer] indefinites

[Bill Page]

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.

> > (6) -> x:Integer
> >                                            Type: Void
> 
> Here you've told the interpreter that 'x' is of type Integer. 
> Unlike Symbol, the Integer has no default value. Since you 
> didn't assign 'x' a value it has a value whose type is Void.
> 

Yes, of course. This is the axiom-developer forum not the
user forum. Your explanation isn't really necessary. What
Axiom is doing is clear. Why Axiom is designed to do what it
does is not so clear. Specifically, since x still has no
assigned value, it is not clear to me why Axiom does not at
least coerce it to Variable x which does have a value.

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. In fact we
can do some rather weird things with the fact that Variable
is a domain. For example, suppose we declare

   x:Variable y

Then

   x

gives the result

   x is declared as being in Variable y but has not been
   given a value.

We can write

  x:='y

but not

  x:='z

to which Axiom replies that it cannot convert the symbol z to
type Variable y.

All this seems a little strange and redundant since we can do
the same thing with symbols, but I guess it is mostly harmless.

> 
> > ... declaring the type of a variable to be Integer (or
> > Float etc.) prevents this coercion to symbol and so this
> > variable can no longer be used to form a Polynomial.
> 
> If you do a 
>   )show Integer
> (the output is too long to include here) you'll find that 
> Integer does not have a 'coerce' function from Integer to 
> Symbol. You told the interpreter that 'x' is an Integer and 
> thus you told the interpreter that only functions supported
> by Integer apply. Since there is no function that will coerce
> an Integer to a Symbol what you want doesn't exist. The
> interpreter is just doing what you told it to do.

Of course the interpret is just doing what I told it to do.
The point is that I think there *should be* a function that
will coerce an Integer to a Symbol (well actually Variable,
I suppose) when it has not been assigned a value.

> 
> > So I wouldn't mind so much if I got the following result
> > above
> > 
> > (7) -> x
> > 
> >    (7)  x
> >                                    Type: Indefinite Integer
> 
> Ummm, the issue is MUCH more subtle than it appears. 
> Indefinite(Integer), indeed, Indefinite anything is a whole 
> new type tower with completely different meanings for all of 
> the operations. The issues are subtle enough to be considered 
> material for a PhD thesis (or two) so I can't really explain 
> them in detail as I'm still pondering the questions.
>

I think you are looking at this from the wrong perspective,
focusing too much on the way Axiom does things now and not
enough on basic design and the ways in which Axiom represents
a compromise. I don't see why you claim "Indefinite anything is
a whole new type tower with completely different meanings for
all of the operations." After all the theory of types and the
use of variables (even typed variables) is a relatively old
subject in mathematics. But I can't really comment on what
counts as material for PhD thesis these days ... :)
 
> > 
> > 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.
> 
> 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

        1
                              Type: PositiveInteger

even though x has no assigned value.

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 key issue is that symbolic computation systems do very
> > > little "symbolic" computation (hasty generalization to make 
> > > the point). We'd like to be able to do computation "along the 
> > > theorem line" (that is, reasoning with known theorems) rather 
> > > than basic algebra.
> > > 
> > > Comments?
> > 
> > Tim, I agree with your point especially as it applies to Axiom. 
> > Perhaps the strict typing makes such symbolic computation more 
> > difficult. Other systems such as Maple and Mathematica seem to have 
> > more abilities when it comes to this kind of computation. I am also 
> > reminded of systems like Reduce in which symbolic tensor algebra 
> > (ITENSOR?), in the sense you mean above and in a manner similar to 
> > that described in Richard Fateman's paper that you quoted.
> 
> You can't even raise the question or construct a proper 
> answer in a system that does not do strict typing. The 
> research question itself is about strict typing so it makes 
> no sense to talk about the M* systems as they can't construct 
> types (at least in the meaning of the question).

I don't agree. Your claim was that

> ... 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.

> 
> Hope this doesn't add to the confusion too much.
> 

There is confusion???  :)

Seriously, I think this dialogue continues to be quite
worthwhile.

Regards,
Bill Page.