[Axiom-developer] indefinites

[Bill Page]

On Tuesday, June 22, 2004 9:59 AM Tim Daly address@hidden
wrote:

> ... 
> We've been looking at the issue in terms of indefinites.
> In the current version of Axiom if you type:
> 
>   x+1
> 
> 'x' is known to be a symbol
> '1' is known to be an integer
> there is no plus which takes +(symbol,integer)
> so 'x' gets promoted to polynomial over integers
> '1' gets promoted to polynomial over integers
> '+(POLY(INT),POLY(INT)) exists
> and the result is
>   x + 1
>          Type: Polynomial Integer
> 

When I started using Axiom I was very surprised by the
following:

(1) -> x

   (1)  x
                                           Type: Variable x
(2) -> x+1

   (2)  x + 1
                                           Type: Polynomial Integer
(3) -> x:Symbol
                                           Type: Void
(4) -> x

   (4)  x
                                           Type: Symbol
(5) -> x+1

   (5)  x + 1
                                           Type: Polynomial Integer
(6) -> x:Integer
                                           Type: Void
(7) -> x

   x is declared as being in Integer but has not been given a value.
(7) -> x+1

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

(7) -> x::Symbol

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

--------

First, the type of x if no domain has be declared is "Variable x"
not symbol. That seems very odd (even wrong?) In what sense is
"Variable x" a domain? This seems like unnecessary confusion at
a rather basic level. But whatever "Variable x" is, it can apparently
be coerced to "Symbol" as you said, and we can use it to construct
a Polynomial, an Expression or whatever.

But worse, actually 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.
  

> Now it is often convenient, and especially important for 
> further research work we want to do, to be able to specify 
> that 'x' is an "indefinite integer". Thus there can be a
> signature 
>   +(Indefinite(Integer),Integer) -> Indefinite(Integer)
> so that
>   x + 1
>          Type: Indefinite Integer
>

So I wouldn't mind so much if I got the following result above

(7) -> x

   (7)  x
                                           Type: Indefinite Integer

-------

In fact it would make good sense for things to default to
something like Variable Any rather than Variable x and then
we could use the type Variable Integer instead of Indefinite.
I think there are already too many names for the same thing
in Axiom.

Now the first thing I would want is to be able to coerce
Variable Integer to Symbol. The second thing (maybe more
difficult?) is to be able to interpret it as Integer, at
least in the special case

  x:=1

Or in general it might be better if the variable retained it's
assigned domain (e.g. Integer) but if it has not (yet) been
assigned a value then it could still be coerced to a Variable
of that same type (e.g. Variable Integer).

> ... 
> Indeed, the idea of Indefinite(R) where R is a domain is
> the generalization. Thus, for your example, in Axiom the 
> appropriate type would be 
>   Matrix(Indefinite(Integer),Indefinite(Integer))
> 
> We can clearly construct such types in Axiom. What the 
> mathematically correct reasoning would be and what algorithms 
> apply is an interesting question that we need to explore.
>

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

Regards,
Bill Page.