[Axiom-developer] RE: Aldor and Axiom

[C Y]

--- Bill Page <address@hidden> wrote:

> On February 13, 2006 4:22 PM C Y wrote:
> > 
> > --- Bill Page wrote:
> > > ... (Sorry Cliff, I don't mean to sound
> > > too harsh but we have so few resources working on Axiom that I
> > > worry that such unrealistic ideas can only serve to divert our
> > > attention from what we can actually accomplish.)
> > 
> > No problem - I definitely don't have experience with implementing
> > compilers, and I have no desire at all to be "irresponsible". 
> 
> Ok, good. Communicating by email is always a danger since it is so
> hard to "smile while you say something that sounds critical". Just
> sometimes I feel so strongly about something that I can resist. :)

Heh.  No worries - I have a very bad habit of voicing opinions on
things I'm not really qualified to discuss, so I invite the occasional
strong response ;-).
 
> > But from my perspective (which may or may not be accurate) we are 
> > being hindered by the uncertainty surrounding SPAD vs. Aldor.
> 
> I that the Axiom is being hindered by the fact the Aldor is not yet
> available as open source.

Certainly true.  However, based on your comments below, I would suggest
the following steps might be immediately useful:

a)  Post the downloads for aldor on the Axiom site (I still can't get
through to aldor.org :-( and the site is slower now) - I think this is
allowed under the license no problem.

b)  Let's incorporate aldor into the main Axiom now - if it is firm we
will be using Aldor (and based on my recollection everyone is in
agreement Aldor is the way forward over SPAD) lets not wait for the
legal stuff to finalize - that could take many more months.  We could
at least do the following:

  i)  Work out how the Aldor compiler and the lisp structure of Axiom 
      should work together, and make that the default setup.  I know
      the BOOT vs. Lisp vs. Aldor debate could go on, and may yet, but
      for now let's go with Tim's Lisp work and the current Aldor.org
      compiler.  I don't (think) those issues will depend on having the
      compiler source code - am I wrong?  I think I recall it being
      said that the interperter needed to be educated about Aldor, for
      example?
  ii) Start retargeting the more important Axiom libraries to Aldor. 
      Absolute worst case scenario we retarget to SPAD again, and I
      doubt we will face worst case in the long run.  So let's assume
      Aldor until proven otherwise, and start to retarget code now.

Does that make sense, or is it too risky?  I think that's more or less
what's been going on of late anyway, but it might help to make it an
"official" project goal so people can be confident they aren't working
at cross-purposes with the main Axiom project.

> > If we can't implement our own Aldor compiler, that's OK, but we
> > can't wait forever for the one that does exist to be released -
> > projects can die from uncertainty and lack of momentum.
> 
> True.
> 
> > If some resolution isn't found fairly soon I would recommend we
> > pick a direction and go, even if it's cleaning up SPAD and not
> > worrying about Aldor except maybe for a design idea or two.
> > ...
> 
> I still firmly believe that Aldor is the best way forward. Given
> that everyone who has posted to the:
> 
>   http://wiki.axiom-developer.org/FreeAldor
> 
> petition (including Steven Watt!) has been positive about the
> idea of making Aldor open source, I think we should just proceed
> based on that idea.

OK.  On that basis, do my earlier suggestions make sense?

> At this point I think we could even safely
> start distributing the Aldor source code as an (optional?) part
> of the Axiom source code distribution. We could state clearly
> up front that the eventual license conditions are not yet
> finalized but cover simply all bases by provisionally choosing
> the most restrictive open source licensing - GPL for now. Later
> this could be opened up to the BSD-style license that covers
> most of the rest of Axiom, provided the interested parties all
> agree.

No, GPL won't quite work - Aldor.org requires complete rights to
derivative works, IIRC.  I think we can just stick the Aldor license
with the Aldor compiler and leave it at that, for now.  At a guess that
clause in the Aldor license was included to handle some of the same
issues I remember being mentioned for Axiom back in the
pre-code-release days, but that was when I was more into Maxima so I
confess it's a bit hazy.  

Out of curosity, does anybody know what the language of the Aldor
compiler is?  IIRC it can target a couple different languages for
compiler output(?) but I don't recall what language it's actually
written in.

> > OK.  I guess my confusion comes in with what our actual plan is.
> > Are we going to use Aldor.org to work with our existing code 
> > base, making a few tweaks and updates to take advantage of Aldor's
> > features but keeping the rest as SPAD?
> 
> No. I would propose that we proceed according to the original
> plan at IBM - to convert all (or as much as possible) of Axiom's
> library code from SPAD to Aldor.

OK.

> > How do we resolve things like Aldor's libalgebra vs. Axiom's
> > libraries?
> 
> I would propose that we forget about Aldor's native libraries for
> now (as nice, though limited, as they are).

Hmm.  OK, so you suggest we first get Axiom as it stands over to Aldor
and then proceed with any low level design changes, if any are
warranted?
 
> > Are we intending to link the discussion and definitions of
> > SPAD/Aldor to the core set theory, category theory, and other
> > foundational mathematical principles that Axiom is built on?
> 
> Yes! At least, where and when possible. I think this will necessarily
> be an ongoing task.

OK.  I know Axiom is supposed to be founded on category theory and/or
set theory, but does anybody know where the real "core" of that logic
resides?  I always figured that was the most fundamental mathematical
part of the code, but maybe I'm wrong.  I was kinda hoping Axiom could
serve as a modern, computerized Principia Mathematica++. 
(Interestingly, if a first edition is available, might it be out of
copyright?  Perhaps we could incorporate the Principica Mathematica
itself, or a variation, as a literate document!)

I think there are really two levels of mathematical "CAS" usage, if you
define "CAS" broadly enough:

a)  People working on proofs of new principles, formalizing mathematics
(proof systems like COQ, metamath, etc.)

b)  People who USE the mathematics in specific cases of the general
cases, for practical purposes (everything from solving a particular
symbolic integral to physics and engineering applications).  These
users benefit from the rigor sought and implemented by a) but do not
require the proof of the validity of their particular answer if the
system as a whole can be trusted.  (Maple, Mathematica, Maxima, etc.)

Axiom is in a bit of a unique position - it functions more at the level
of b), but some of its design properties hint that it could straddle
both a) and b) to the benefit of both.  Clearly there have already been
a few efforts in that direction - I wonder if Aldor's compiler could
target proof-engine languages as well as Lisp and C.  If a CAS user
wanted a formal proof of a statement, they could issue an Axiom level
command to generate a proof of a statement - Aldor could then compile
the top level statement to a form that a theorem prover could digest,
call the theorem prover, and have it digest it - then return the proof.
 Maybe it could even provide an interaction environment for interactive
proof systems.  Of course, that would require creating proof-engine
libraries of all of Axiom's built-in libraries, which should validate
both Axiom's correctness and the robustness of its type system, in
theory.

The nice part is that this can be done gradually, after the fact - it
is not a "do this before implementing anything" situation.  If that
ability is added to Aldor, it will become a tool to improve the
quality, correctness, and confidence in the libraries, but it is not
absolutely needed.

For Aldor gurus, am I correct that Aldor can target Lisp and C as
outputs of its compiled Aldor code?

> > I realize I'm almost useless for this kind of work, but since it
> > seems to be the biggest need of Axiom right now I would like to
> > help if I can,
> 
> I think your questions and suggestions are very useful. Someone
> has to raise the level of discussion somehow! :)

:-).  Thanks.

> > even if it's only something like creating a literate document
> > introducing basic set theory or category theory (e.g. something
> > I might be able to grasp in time, but also useful to documenting
> > the core Axiom system all other work must rely on.)  I guess what
> > I'd most like to see is a stage-by-stage kind of plan for the
> > Algebra subproject.  Sort of a:
> > 
> > a)  Document SPAD compiler, foundations in mathematical theory,
> > core structures of Axiom algebra
> > b)  Identify and document "core" functionality, which is to say
> > functionality which a large part of the Axiom system depends 
> > on.  Debug code and concepts, possibly implement unit test
> > framework.
> > c)  Work our way up the ladder, so to speak.  Higher level
> > functionality documented as the underpinnings become well
> > documented and well defined.
> > 
> > type of list.
> 
> I would replace a) with conversion of the Axiom library to
> Aldor, but the rest seems great to me.

OK.  I take it the compiler itself doesn't contain the definitions of
any of the algebraic types or constructs?

> > Maybe this isn't workable with something as involved as
> > Axiom, but right now it's almost overwhelming - where should
> > one look first for the job of building a rock solid core on
> > which the subsequent tuning, debugging, and development can
> > depend?    
> > 
> 
> I think you have the right idea. :)

Cool :-).  Then I vote for full steam ahead with Aldor - the legal
issues will take time, but there seems to be some confidence that they
can eventually be sorted out.  Let's bundle the sucker and start some
algebra tuning!

Cheers,
CY

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