Re: [Axiom-developer] B#

[C Y]

I'm in a bit over my head here but maybe these questions will be useful
in straightening me out...

--- root <address@hidden> wrote:

> re: the future of aldor
> 
> there are some sticky IP issues with aldor. Manuel was a major
> contributor and he is no longer able to agree to donate his code.
> i'm in discussion with people associated with INRIA about making
> his code and research available but that, like everything else,
> moves at a (pre-global-warming) glacial pace.

I thought NAG still had the rights to Aldor, with Aldor.org getting a
license?  Or was there post-NAG work done on the Aldor.org version we
would want to use?

I know Manuel wrote quite a lot of code we would definitely want to use
but I thought that was "over and above" the core Aldor compiler - did I
misunderstand how that worked?

> re: aldor replacing spad
> 
> aldor may or may not replace spad. that's a huge task. and it will
> be made worse because it's unlikely that any one of us will be
> willing to perform a straight spad to aldor conversion without
> generating numerous opinions regarding "better ways to do this" 
> (witness the ongoing Monoid/Ring discussion).

Heh - like you said, there's no such thing as a simple job.  I
personally would be willing to support a straight conversion as step
#1.  Eventually, no matter how we do this, virtually all of Axiom will
need to be revisited and properly understood/documented, so I think
compared to the magnitude of that task the language coversion becomes a
detail.  It will undoubtedly raise issues that will need revisiting
later, but I think those issues would likely would have (or should
have) been raised regardless so no harm done.

> even without that level of issue it's tempting to try to break the
> algebra cycles using post-facto extensions. this will generate more
> very interesting but, to the actual implementors, painful discussion.

Looking at it one way, this might be an indicator that we are actually
undertaking to do something truly worthwhile.  As I heard somewhere,
"Nothing worth doing is easy."  We're taking on problems that need to
be solved but are difficult to solve - always the sign of a good
research project :-).

> re: B-natural
> 
> B-natural won't replace the interpreter because the real semantics of
> an expression is carried in the type. B-natural has the essential
> goal of hand-waving away the type issues to make it easier for people
> who don't care about the type. but i believe this raises some very
> hard coercion/conversion questions which will turn out to be 
> fundamental.

I think that issue remains no matter what we do - do we really
understand what the current interpreter does either, for that matter?

In some larger sense, we seem to be asking the question "what is the
best way to merge the casual semantics of day to day mathematical
calculations and the full rigor of a system which places paramount
importance on correctness?"  Or, even more fundamentally, "what do we
ignore in day to day mathematical work and how can we sure it actually
is safe to ignore it?"

Take, for example, the use of noPole in an integration problem.  As I
understand it, this allows Axiom to proceed in applying algorithms to
an expression which it wouldn't normally accept, but also introduces
the risk that Axiom might "ignore" a problem with using those
techniques and produce an incorrect result.  I guess a logical
follow-up would be - if the answer proves useful - for the user to
request that Axiom attempt to generate a proof that in this specific
case the noPole option can be safely ignored.  This latter step is
probably ignored in most cases, if the answer "works", but really
shouldn't be if the answer is to be used in any "rigorous" application.
 Granted such a feature would be highly non-trivial, but I think this
is an example of the benefits which might result from combining proof
logic with a CAS.  (In concept, anyway - I have no idea if those
systems could actually do something like this.)

Clearly there is a useful middle ground between fully rigorous and
casual/risky, since tools like Mathematica, Maple, and Macsyma are
widely used.  Am I right in thinking that we, by the nature of what we
are trying to do, are faced with the task of actually defining that
middle ground?

Interesting work!

Cheers,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com