RE: [Axiom-developer] about Expression Integer (with Quizzes)

[Bill Page]

On February 27, 2006 10:37 AM Tim Daly (root) wrote:
> ... 
> my experience is that written mathematics notation is very
> ambiguous. we don't normally notice this because we view
> each equation in the context of a given subject and, usually,
> in the context of a few paragraphs that contain the semantics.
> 
> axiom attempts to capture the semantics and carry it in the
> type. if the semantics of the type fits your understanding of
> the equation then axiom works "correctly". if not, it appears
> to be a bug. (axiom is hardly bug-free but i'm focused on the
> DMP issue here)
> 
> so what is the semantics of 2*x + 1/x? well, it's ambiguous.
> each of you have successfully argued your understanding of 
> the semantics. and, in the context you've established, you
> are correct.
>

Right on! I agree completely with both your analysis and your
conclusion.
 
> but axiom has to assign a meaning that might not match your 
> understanding. this is where the ambiguity becomes apparent.
> it is also where mathematics and computational mathematics
> part company.

Of course not all mathematics is inherently ambiguous and there
are usually several different ways in which the ambiguity can
be resolved. I would like to suggest (of course I can't prove
it, yet. :) that the current approach to many mathematical
subjects in terms of formal category theory provides a way of
reducing the ambiguities in a way that is largely compatible
with Axiom. For example, it seems to me that the formal definition
given by Ralf Hemmecke in this email thread of a polynomial in
terms of a graded sum is of this sort. That is the reason why
Axiom's behaviour seems much less anomalous when described in
this way.

>...
> 'semantic context' is really an 'extended type' idea. that is,
> you want to be able to tell axiom what area of mathematics you
> are working in and have the type system adapt its meaning to
> that area. 
> 
> this is the section of the textbook where the author say things
> like: "i'm carefully distinguishing the Ring of coefficients
> from the variables in the polynomial" vs "this book explores
> polynomial arithmetic".
>

I agree. My point of view is that as designers of computer algebra
systems we need to be sensitive to the way that mathematics is
actually done. We want a system that is easy to approach for
someone with at least the usual non-specialist undergraduate
experience in math - one that they will find immediately useful
for at least some of things they want to do. But that does not
mean that we need to be "held hostage" to only certain ways of
doing mathematics. Where it seems an advantage, a system like Axiom
needs to be free to present it's own method for formalizing and
solving mathematical problems. In this case the user might need
to learn something new in order to use Axiom even though they may
have an advanced level of understanding of their subject in
conventional mathematical terms.

More than just the mechanical assistance that Axiom provides in
solving a problem, it is this new formality that I think is the
real value added by Axiom. This means that in some cases Axiom's
way of doing things needs to be very carefully and completely
documented. Unfortunately we do not have much documentation of
this type for Axiom.
 
> the compiler will let you keep the two domains separate and will
> force you to merge the domains when you want that behaviour. the
> interpreter is just guessing and you have to be careful to
> understand how and why it guesses. (which means we have to
> construct a model of the interpreter so we can formally state
> the coercion/conversion graph).

I agree. And again this is largely a function of the quality of
the available documentation. I think the existing Axiom interpreter
has it's good and bad points. Each of these needs to be understood
without having to endure a long period of learning by trial and error.

Good user interface design is a large and still largely un-solved
problem. So there is still a lot of room for improvement. But
changes to a complex existing system like Axiom need to be done
very carefully because even simple changes can potentially have
large and unexpected consequences for some applications and some
ways of using Axiom. But at the same time this might provide
sufficient motivation to continue the development of alternate user
interfaces such as proposed in the B# project.

> 
> in my world view a semantic context is another facet in the
> crystal. (but that's still long-term fantasy so we won't talk
> about it here).
> 
> anyway, i don't see that it is possible to resolve this debate.
> you are all arguing from different semantic contexts. until you
> agree to use the same assumptions there is no resolution.
> 

I think you are right. In fact, I would say that the point is not
so much that we should agree, but rather that we need to understand
how it is possible to accommodate several different points of view
even though they might appear at first to be contradictory.

I think we need to focus *first* on documenting clearly what Axiom
actually does, rather than trying to judge whether what Axiom does
is "right or wrong". Because Axiom is open source software, if
necessary, we can actually read the source code itself to determine
this exactly. And we can demonstrate our understanding with actual
experiments in Axiom. So far, I think we are doing a pretty good
job of this. But it still needs to be distilled into useful
documentation that can be read by non-specialists.

Second, we need to try to explain *why* Axiom does what it does.
This is harder and it might be difficult to get full agreement.
Some parts of Axiom were clearly the result of experiments that
were part of the overall research project. Some of these experiments
where more successful than others and unfortunately we do not have
very much documentation of this original research. My point of
view is that where necessary we should try to create models that
are (perhaps only largely) consistent with Axiom but motivated by
contemporary methods in mathematics. This is where I see category
entering. Since category theory is now also a fairly well accepted
tool in programming language semantics, I think we are in a good
position here.

Third, we can consider changes to Axiom that would make it more
self-consistent and that would make it conform more closely to
the models that we have developed above, in brief: to make Axiom
more categorical.

Regards,
Bill Page.