[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] about Expression Integer (with Quizzes)
From: |
root |
Subject: |
Re: [Axiom-developer] about Expression Integer (with Quizzes) |
Date: |
Mon, 27 Feb 2006 10:37:14 -0500 |
ok, time for me to weigh in on this subject....
but i will do it at a meta-level.
i think it is important to distinguish between mathematics and
computational mathematics.
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 sematics 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.
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.
the 'solution' to this problem is to develop the computational idea of
a 'semantic context'. essentially what is needed is the ability to say
(at least in computer science terms):
"i want 'x' to be globally scoped" or "i want 'x' to be locally scoped"
but that isn't the best long-term approach. 'semantic context' is really
an 'extented 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".
the compiler will let you keep the two domains separate and will
force you to merge the domains when you want that behavior. 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).
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.
t