Re: [Axiom-mail] Math Types inclusion

[root]

Actually, it seems that you are treading on an area we are currently
discussing internally. Essentially it amounts to the following
observation: Computer algebra systems are not "symbolic" at the level
we want to work. 

Essentially you'd like to work with the domains themselves rather
than elements of the domains, if I understand you correctly. Or at
least with a "canonical element" of a domain. 

We've had much discussion about this issue. It is the driving force
behind my attempt to unify the ACL2 work and Axiom. Somewhere between
the two approaches lies a useful kind of computational reasoning.

Categorically, Axiom seems capable of handling these domains.
However, the issue of representation and computation is different
than what we traditionally do. We want a representation that captures
the whole domain structure rather than a single element. We want a
computation that captures the axioms and theorems rather than
computation of individual results.

ACL2 is too far toward the proof end of the reasoning and Axiom
is too far toward the computational end of the reasoning. We need
to be able to represent and compute the lower central series, for
example, not as individual elements but as entire objects.

Does this seem to capture the essence of your struggle?

Tim