RE: [Axiom-developer] Question concerning types...

[Bill Page]

On September 17, 2006 1:59 PM Ralf Hemmecke wrote:
> ...
> Gaby wrote:
> > 
> > yes.  My working assumption is that if we had Variable(D: domain)
> > to mean anything, it would be such that operations of D would 
> > be *lifted* to Variable(D: domain) and would work as if we had an 
> > algebra (in the Universal Algebra sense).  In this case "+" would
> > be lifted to Variable Integer, so that x + y can be interpreted as
> > an element of a free monoid generated symbols.  That is not rocket
> > science.

No. The question is: Is it computer science? ;) I am glad that you
appear to think so.

> 
> I agree with you that if D had type T then Variable(D) should 
> have type T (plus maybe some exports that allow to create
> "indeterminates").

The meaning of this statement is unclear to me. Do you mean:
If D has category T then Variable(D) should have category T?
If so, I would disagree. Variable(D), as a universal algebra
over some symbols must have a different (but related) type,
perhaps Variable(D) has Universal(T)?

> 
> Looking at it mathematically (and simplified) then all we do 
> is that we take a universal algebra D = (A, F) where A is the
> carrier set and F are the functions on it. Variable(D) is maybe
> a bad name, but all we do is that Variable(D) = (A', F') is a
> universal algebra where A' is the union of the set A, a set X 
> of indeterminates, and all things that can be generated from A
> and X by applying functions from F'. F and F' behave identically
> on A.
> 
> Mathematically, that's not a big deal. But Aldor domains are
> actually multi-sorted algebras. That makes the situation a little
> more complicated.
>

I think sometimes you think too much about Aldor and not enough
about Axiom... ;)
 
> So I still disagree with you that x+y should be of type 
> FreeMonoid(Variable(Integer)). From what I said above, it seems
> more natural to me that its type is Variable(Integer) (well,
> it's a bad name, maybe Indefinite(Integer) would be better).
> 

The interesting thing to me is that all you appear to be doing here
is "re-inventing" the Expression domain constructor.

It seems to me that 'Expression(Integer)' is a good enough name. :-)


> Anyway, what we want is a nice way of adding elements and more or
> less keeping the type of the domain. And that is not possible if
> you just define "Indefinite" having one argument D. One must know
> the type of D (a category) so that the return type would be clear.
> 
> Indefinite(C: Catagory)(D: C): C == add {
>      Rep == Union(d: D, ???)
>      ...
> }
> 
> The ??? should be something that allows arbitrary expressions formed 
> from D, the functions in C and some indeterminates X. (I have no idea 
> how that would look like. Maybe just delayed evaluation of function 
> composition.)

I strongly recommend that you take a close look at how Expression is
implemented in the Axiom library.

> 
> > [...]
> > 
> > | (1) -> (a1,a2,a3,a4):Expression Quaternion Fraction Integer
> > |         Type: Void
> > | (2) -> m := matrix[[a1,a2],[a3,a4]]
> > | 
> > |           +a1  a2+
> > |      (2)  |      |
> > |           +a3  a4+
> > |         Type: Matrix Expression Quaternion Fraction Integer
> > | 
> > | given by Bill suggest that the Axiom interpreter is a bit
> > | more relaxed.
> >

The key thing to recall is something Martin wrote earlier.

On September 17, 2006 3:44 AM Martin Rubey wrote:
> 
> Gabriel Dos Reis <address@hidden> writes:
> 
> > However, I seem to remember Ralf telling people that they 
> > should never ever enter EXPR T in Axiom; so without knowing
> > what you do futher with your matrix I can't say the EXPR domain
> > constructor is a good way to go; you have to try.
> 
> I think that one has to be more careful before judging EXPR 
> that way. I'd rather say: try to avoid EXPR as much as you can,
> but there are things which cannot be handled without.

I think the only reason to "avoid" Expression is because in some
sense it represents a less powerful and less generalizable approach
to computer algebra.

> 
> EXPR QUAT FRAC INT would be the domain of expressions, with 
> coefficients (i.e., all "numbers" that appear) being from
> QUAT FRAC INT.
> 
> Internally (and that might be good for understanding), the 
> elements are stored as fractions of multivariate polynomials
> with coefficients being QUAT FRAC INT and symbols being "kernels",
> i.e., things that cannot be evaluated further.
> 
> Cliff, maybe you would be happy with the domain
> 
> POLY QUAT FRAC INT?
> 
> this one is "safer" - doesn't provide as much functionality though.
> ... 

As Martin says, Expression is really implemented internally in
Axiom as 'Fraction MultivariatePolynomial' where the polynomial
symbols include first of all, all symbols (such as the symbols
a1, a2, a3, a4) plus a large number of other expressions, e.g.
'sin(a1)' which are not evaluated any further in the Expression
domain.
 
> > Funny enough, I tried similar thing and sent a message before
> > seeing Bill's.  That is a natural thing to do if you have a
> > Universal Algebra background -- e.g. you're used to the 3M's.

Actually the suggestion that the 3M's have anything to do with
Universal Algebra kind of made me "gag" ;) Seriously, I doubt the
implied connection. But it is true that Axiom's Expression domain
constructed was designed specifically to address the type of
"symbolic" calculations often done in these other packages.

> 
> Maybe. I don't say that shouldn't be allowed in the interpreter,
> but the compiler would generate a matrix of 4 uninitialized entries.

No that is not true. In the domain Expression the symbol 'a1'
simply stands for itself. It is not "uninitialized'.

> Now what happens if you print m(1,1)? If that prints something 
> reasonable then it tells me that the compiler knows about a special
> domain constructor, namely Expression.

Yes.

> Drop "Expression" from above, what would be on screen for "stdout
> << m(1,1)"? The interpreter can add smart things. I am asking for
> the compiler.
> 

I don't understand. Obviously Expression is a domain that the SPAD
compiler understands. Implementing Expression in Aldor should be
quite straight forward.

Regards,
Bill Page.