[Axiom-developer] Re: [Axiom-mail] Math Types inclusion

[Bertfried Fauser]

On Tue, 6 Apr 2004, root wrote:

Dear Tim,

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

Interesting, I haven't known that such a discussion is on the track.

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

Yes, in category theory (math), there is the concept of the "name" of an
operator. One can compute with the names of operators _without_ even
having defined elements. The same holds true for arrow only categories,
where objects are given via identity arrows, no elements at all. [This can
nicely be done in a Hopf algebra setting, one point why I like this
structure so much]

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

I do not know ACL2, but I fear not to have the resources to learn another
system. I think AXIOM has already the key features which are needed to
come up with computational and categorial issues.

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

In symmetric function theory, there are hints what to do. One can compute
with symmetric functions _without_ havings seen variables! (AXIOM does
this the same way, you specify the type of symmetric function (say power
sum) and the partition which characterizes it, that's sufficient to
compute with them, you need not even specify a name for the "variables",
they need not even to be actually _there_. However, one needs to make
assumptions about their domain (commutative, associative, etc..) which
enters the actual algorithms.

> We want a computation that captures the axioms and theorems rather than
> computation of individual results.

Once more, there is a big math problem in the back. In Maple, Rafal and I
do computations on a general element and _after_ the computation is
performed, this elements is cut out and eliminated. It works more like a
substrate or catalyst. However, regarding Clifford algebras, Zbigniew
Oziewicz and I (and probably others too) tried to get a entirely
categorial axiomatization but failed. If you try to do this, you get a
wast generalization of the structure. A categorial description does eg
know nothing about the base ring of the modules. So one has to deal with
characteristic free models which are much more complicated than those over
ordinary fields with characteristic zero.

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

I have studied linear categorial logic quite recently. It looks very
promising to solve quantum field and quantum mechanical problems. There
are quite a few but extraordinarily interesting papers around, showing how
categorial logic and proof theory __directly__ applies to quantum optics!
However, physics seem to need linear logic, and intuitionistic logic,
boolean logic will not do. During a lose discussion I told colleagues,
that my long term dream is to "Reformulate quantum field theory in terms
of categorial logic, so that (elementary particle) processes become a
proof in that logic, every process in nature would then be a step in a
quantum programming language called QFT" Of course, that's fare from being
actually realized, but a goal to struggle for.

> Does this seem to capture the essence of your struggle?
Yes, but I had also expressed very practical needs, due to my
unskillfulness in programming.

ciao
BF.

% PD Dr Bertfried Fauser
%       Institution: Max Planck Institut for Mathematics Leipzig 
<http://www.mis.mpg.de>
%       Privat Docent: University of Konstanz, Physics Dept 
<http://www.uni-konstanz.de>
% contact |->    URL : http://clifford.physik.uni-konstanz.de/~fauser/
%             E-Mail : address@hidden (address@hidden)
%              Phone : Leipzig +49 341 9959 735  Konstanz +49 7531 693491