[Axiom-developer] symbolic matrix multiply

[Tim Daly]

Richard,

Your paper
http://www.cs.berkeley.edu/~fateman/papers/symmat2.pdf
is very interesting.

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

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

This is a slightly more primitive notion than matrices of 
indefinite size but the ideas are essentially the same.

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.

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