--- Bill Page <[EMAIL PROTECTED]> 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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer