Re: [Axiom-developer] indefinites

[root]

Bill,

The distinction between Integer and Indefinite Integer is quite subtle.
Normally we think of a number, like 1, as an integer. In fact, if you
just type 1, Axiom is further restricts the type to the subtype
PositiveInteger:

(1) -> 1
 
    (1) 1
                                           Type: PositiveInteger

> When I started using Axiom I was very surprised by the
> following:
> 
> (1) -> x
> 
>    (1)  x
>                                            Type: Variable x

Non-numeric tokens become things of type Variable, as above.

> (2) -> x+1
> 
>    (2)  x + 1
>                                            Type: Polynomial Integer

The interpreter must make sense of this list of tokens
and find a compatible set of types where there is a '+' operator
with a signature matching the types. The interpreter eventually
"lifts" both to Variable(x) and PositiveInteger to POLY(INT) and
finds the signature +(POLY(INT),POLY(INT)) -> POLY(INT)

> (3) -> x:Symbol
>                                            Type: Void

Here you've just asked the interpreter to remember that the
token 'x' is of type Symbol. Notice that you now have a thing
with a Type Symbol which has a default value of its token name.
You could have said:

         x:Symbol := 'y

and now the value of the symbol 'x' would by 'y'. 

> (4) -> x
> 
>    (4)  x
>                                            Type: Symbol

Since you didn't assign the Symbol a value it defaults to its own name.

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

Here you've used the Symbol 'x' and the PositiveInteger 1 with the
'+' function. This gets promoted by the interpreter as before to 
POLY(INT) to find the signature +(POLY(INT),POLY(INT)) -> POLY(INT)

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

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

Here you've tried to take the value of 'x', which is Void. The
interpreter complains. If you want the value of 'x' you must
assign it a value as in:

         x:Integer:=1


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

Here, again, (as in lisp) you've used a token of type Integer and
another token of type PositiveInteger. Axiom finds the signature
+(INTEGER,INTEGER) -> INTEGER. It promotes PositiveInteger to Integer
and calls '+'. The '+' function tries to take the value of its first
argument, 'x', and gets Void. It's like the lisp (+ x 1) where 'x'
has no value.


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

Here you've asked for the value of 'x' to be converted to Symbol.
If 'x' had the value 'y' then this would work. But you've already
told Axiom that 'x' is an Integer so no matter what value you assign
to 'x' you can't get a Symbol because there is no way to coerce an
integer to a Symbol.


--------

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

Variable is a perfectly valid domain. We can ask Variable what operations
it supports and we get:

(3) -> )show Variable
 Variable sym: Symbol  is a domain constructor
 Abbreviation for Variable is VARIABLE 
 This constructor is not exposed in this frame.
 Issue )edit /boot/axiom/mnt/linux/../../src/algebra/VARIABLE.spad to see 
algebra source code for VARIABLE 

------------------------------- Operations --------------------------------
 ?=? : (%,%) -> Boolean                coerce : % -> Symbol
 coerce : % -> OutputForm              hash : % -> SingleInteger
 latex : % -> String                   variable : () -> Symbol
 ?~=? : (%,%) -> Boolean              

As you can see the Variable domain supports an operation 'coerce' which
when given a thing of Type Variable will return a thing of Type Symbol.


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

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.
   

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


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


ummm, no. for a variety, (indeed whole fiber bundles) of reasons. 

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

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

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

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

Tim