[Axiom-developer] opus 1, act 1

[root]

Well, that's a long email. I'll have to reply in smaller chunks as 
it is after midnight and I've gotta get to work early tomorrow.

>I think that this should be/could be so is quite
>deeply routed in the design of Axiom and it's type
>system. The distinction between
>
>  x^2 - 1
>
>as something of type: POLY INT versus what appears
>as essentially the same thing
>
>  x^2 - 1
>
>as something of type: UP(x,FRAC INT) actually occurs
>very frequently in Axiom (e.g 1::Float, 1.0::Integer).
>Unfortunately it is something rather subtle and not
>easily explained (rationalized?) to the novice user,

Think of it in terms of Java code. You can have two classes
(POLYINT and UPxFRACINT) that have the same print representation
but different properties.

I suppose that POLY(INT) is similar to UP(x,INT) since the coefficients
are integers. There is a way to coere INTs to FRAC(INT)s (the
denominator becomes 1). However notice that FRAC(INT) does not occur
at the top level of the "type tower". That is, to coerce
UP(x, INT) to UP(x,FRAC INT) you have to "reach into" the type tower
and convert something below the top level type of UP. This is a hard
problem in general and there is no good theory I'm aware of that says
how to do this in a theoretically correct way.

>yet seems essential for new Axiom users to learn this as
>soon as possible - that's one reason why I was really
>quite impressed by the quality of the NAG Axiom for
>Windows tutorial, because it is the first Axiom tutorial
>I have seen that tries to address this.

The book talks about it. It is not easy to understand if you are
not both a programmer and a mathematician. Programmers "get it" in the
sense of Java types. Mathematicians "get it" in the sense of 
categories. Neither is fully correct.

I've been making the point as part of our 30 year planning horizon
that we really need a new department that is a cross between the
math and comp. sci. departments. Call it computational mathematics.
There are a boatload of issues that only a computational mathematician
cares about (program proof, correctness, complexity, type coercions,
type lattices, algorithmic mathematics, lambda reductions, etc).
We need to give the correct background to the next generation and
we need research in these issues done by PhD students.

>There is also the problem that François brings up
>involving the presumptions of those users who have
>been previously exposed to one of the other popular
>computer algebra systems (e.g. Maple, MuPad, Mathematica,
>Maxima ... ) which do not share Axiom's strongly typed
>metaphor. (I am one of these people. <grin>) Such a users
>looks for general operations on expressions like "expand",
>"simplify", "combine" etc. and for the most part finds
>them missing from Axiom! To convince some of these users
>about the wisdom of Axiom's approach may require some
>specially written tutorials and comparisons. And I think
>our current discussion is a step toward this.

I think it was Knuth that said "Teaching BASIC to beginning
programmers causes brain damage and the student will never
recover". The 4Ms have created the illusion that you can 
freely compute results without worrying about the issues that
Axiom struggles with. I believe that this illusion makes it
very difficult to build ever-larger systems. If you can't 
appeal to some theory then the complexity alone will overwhelm
your efforts. Think of the benefits of a strongly typed language
like Java vs a typeless language like BASIC. You can build 
programs in BASIC but you eventually hit the wall when the 
complexity gets high. Java lets you get further. By analogy
I'm arguing that the 4Ms make simple things simple but complex
things ever harder and that Axiom reverses that. I claim that
Axiom scales and the more theory we develop the better it scales.

Of course all of this theory does not help the beginner use Axiom.
At my institute (CAISS at City College of New York) we are planning
to build a series of simple menu-driven front ends for Axiom in a
large variety of courses. The front end hides the complexity because
it only works in a single type (e.g. Expression or POLY(INT)) that
is sufficient for the beginner. Because the operations are all in
one type the issue of type conversion is diminished.

>But inspite of the apparently complexity of Axiom's
>current type system (which I agree is largely due it's
>poor state of documentation and more than a little adhocracy

Yes, the interpreter uses some adhoc methods to try to guess 
what type you might want. It selects functions based on the
type of its arguments as well as the type of the result so it
has to work very hard if you don't give it enough information.
The problem is that YOU have underspecified the input. The
interpreter has to guess and sometimes it does it badly. 

There is no general theory that underpins all of Axiom's type lattice.
We need to create one. The mathematics is pretty sound but there are
a lot of "computational" issues with the mathematics that need work.

>(but with previous experience) will expect to see. For
>example involving the binomial(p,q) function discussed
>by François. There seems to be a whole in Axiom's type
>system that does not allow it to deal conveniently with
>this case nor with factorials in general. We need to
>have clear documentation on the structure of the
>algebra and it's type system so that it will be more
>clear where this new functionality would be most
>efficiently and effacatiously added. As Tim frequently
>points out, Axiom is a "long term project"... <sigh>

It is possible to build a series of cover functions that always
work in one type. That will eliminate most of the problems you
are seeing. Expression(Polynomial(Fraction(Integer))) is a type
tower that is probably general enough to do what you want. Of 
course the cover functions will have to coerce things back and
forth internally to use the existing functions (such as you did
with partfrac).

>Clearly Axiom is trying to choose types that are somehow
>"smallest" or most conservative. Surely UP(x,PI) is smaller
>than POLY INT. No? How about (sin x)::EXPR PI. Why is
>POLY PI an invalid type?

POLY takes an argument which is a RING.
You can ask Axiom about these properties thus:

-> )show POLY

  Polynomial R: Ring    

which means that Polynomial requires an argument which is of type Ring.
So we can ask Axiom about INT and PI:

-> INT has RING

  true

-> PI has RING
  
  false

So when you try to construct POLY(PI) Axiom checks the category of
PI to see if is a Ring. It isn't (it lacks inverses). So Axiom will
not let you construct an incorrect type. The same mechanism keeps
you from constructing Polynomials of files, or matricies of streams.
Files don't have the properties necessary to be a Ring and Polynomials
assume their coefficients are Rings. When you operate on Polynomials
the operations for the coefficients (e.g. subtracting) are done by
looking up the operation "in the coefficient domain". If you do:

)show PI

you'll see that PositiveInteger does not support subtraction so
it does not make sense to build Polynomials over PositiveIntegers.
In general if you can construct the type tower the operations will
be correct. This is the big advantage of Axiom over the 4Ms.

Sleep calls. More later. 

Tim
address@hidden
address@hidden