Re: [Axiom-developer] Aldor and Lisp

[Martin Rubey]

Dear Camm, Cliff, *,

thank you for responding. It seems that my post went ignored on comp.lang.lisp
-- except by you, folks :-) -- so maybe I have to "augment" my
strategy. Details follow below, along with explanations. Sorry, it's a long
post.

First things first: the ultimate goal of this and other posts is to attract
or keep alive interest in axiom. I think that it is a shame that axiom makes so
little noise. I guess that most people just don't know it.

I.) Of course, one possibility is to regularly scan the questions on
sci.math.symbolic and see how we answer them with axiom. Unfortunately, many
things people want cannot really done with axiom: This concerns, for example,

* optimization
* summation
* solving inequalities

Aha! The latter point is *nearly* solved now, since Renaud made his CAD
algorithm available. I did not have time to show how to use it to solve
inequalities, but I know that it should be easy now. I'll do so as soon as
possible.

II.) Apart from this, I'm constantly looking for "side areas", where Axiom
could attract interest. One of these was the AxiomUI effort with
summerofcode. This was WONDERFUL. Well, AxiomUI is not finished, and it is not
certain when it will be, but *at least* one person, namely Kai Kaminski now
knows a fair bit about Axiom. I hope he will recommend it, or at least use it
himself if in need.

Of course "side area" is *not* a pejorative term here. But you don't need to
know any mathematics to play in it. It happens that Kai is a mathematician, but
this was not necessary.

I see two more side areas: porting Axiom to other Lisps and the Aldor - Lisp
issue.

IMPORTANT: I don't intend to convince anybody working on Axiom anyway that he
should port Axiom to Ansi Common Lisp. I want to convince people who are *not*
working on Axiom to start working on Axiom.

So, maybe Camm (since you are known on comp.lang.lisp), you could post a reply
saying something like

"Uh yes, a port of Axiom to ANSI Common Lisp would be nice. It wouldn't be too
much work anyway, as far as I know Axiom. By the way, it's really a nice
system..."

:-)

I'm not a marketing guru, but I think we are allowed to use dirty tricks.

III.) The Aldor issue is *much* more complicated than anything else. That's for
certain. So here follows a short description of what is missing.

-------------------------------------------------------------------------------

The difference between Aldor and Spad is *not that* big. Aldor adds

* a new, but alternative(!) syntax. I.e., the Aldor compiler understands two
  different syntaxes, one of which is the syntax used by Spad. No work on this
  side.

* it adds the "extend" keyword. This allows you to add code to already existing
  domains and categories. For example, you have a domain
  "UnivariateTaylorSeries", short "UTS". It works and you don't want to touch
  that code. However, you really would like to allow sums and products of
  Taylor series, since the can be computed explicitely, as in

  sum((a0(i)+a1(i)*q+a2(i)*q^2+...),i=1..m) =
  sum(a0(i),i=1..m)+sum(a1(i),i=1..m)*q+sum(a2(i),i=1..m)*q^2+...

  (Products are more complicated)

  Currently, we would have to modify the code in UTS. With the "extend"
  keyword, we could say (I don't have the syntax handy)

  extend domain UTS(Coeff, var, cen) = sum: (%, SegmentBinding Coeff) -> %

* Aldor adds "really" dependent types, as in

  Test: with {f:(n:Integer)->IntegerMod(n) } 
    == add {f(n:Integer):IntegerMod(n) == coerce(10)$IntegerMod(n) }
  
  Note that the signature of f depends on its argument. This is currently
  impossible in Spad, leading to ugly constructs for example in
  ExpressionToUnivariatePowerSeries(R,FE) world: All signatures there go to
  type Any, since we would need a signature like

    iTaylor: (fcn:FE,x:SY,a:FE) -> UTS(FE,x,a).


There are some other small differences, I don't know by heart.

-------------------------------------------------------------------------------

Fortunately, only one of these differences cannot be used by Axiom: dependent
types. An example for that failure can be found on MathAction, I'll make it an
Issue today.

Even there, it seems that Axiom does all the computations correct, it seems to
fail rather towards the end, maybe only when it comes to *displaying* the
type of the result. Not sure here.

So, the first step would be to make the Axiom interpreter understand all code
produced by Aldor, i.e., Axiom (the interpreter) should learn to deal with
dependend types.

===============================================================================

Here follow some random answers:

Dear Camm,

Camm writes:

> Just my 2 cents here -- it really doesn't matter what tool we use, as
> long as it is open source and we can get mind-share circled around its
> development.  I know this first hand in working with GCL from scratch
> knowing no lisp at all.  Once one decides to invest in the learning
> curve, the very last thing we should do is flip flop -- expertise is
> knowing no lisp at all.  Once one decides to invest in the learning
> curve, the very last thing we should do is flip flop -- expertise is
> the value we supply and it takes time and is hard to come by.  Given
> where the cards appear to lay right now, extending/fixing SPAD to
> match Aldor appears the obvious choice.  I am assuming a lot here, but
> it is primarily that the factors behind the Aldor rewrite decision
> went something like 1) this code has cruft, time for a rewrite 2)
> we're in the AI winter, nobody uses lisp anymore, and its slow, 2.5)
> its more fun and easier to start over than try to understand and build
> upon the work of others, even if it does effectively destroy the value
> of everyone's time spent on the older stuff, 3) lets build something
> totally new in C.  These motivations are not commensurate with those
> we face in the open source world.  I'm also assuming that Aldor is
> basically like spad but nicer, faster, and a little more powerful. 

I think you are absolutely correct here. At least, I hope so...


> > (Porting to "other common lisps" would also be greatly appreciated...)
> 
> Here too, it is a complete waste of time, IMHO, trying to make sure axiom or
> any system runs on 11 different compilers.

As I detailed above, I think it depends on *who* is doing the port. If some
lisp guru who is not (yet) interested at all in Mathematics does it: great! If
you would be doing it: Camm, STOP it! :-)

> I've been having a lot of correspondence lately with theorem-prover
> authors, and I've come to appreciate Tim's original idea of using one
> to verify AXIOM.  Having something like this would clearly put AXIOM
> at the head of the pack IMHO.

This would be very nice, but I doubt that a theorem prover could be used to
verify Axiom. And, I think that it would be a waste of time. There are
thousends of hidden assumptions in Axioms code. Maybe in Maxima there are
millions, but still. A correctness prover would simply tell you: incorrect. :-)

I rather think that Axiom should provide the functionality of a Theorem prover,
as for example, "Theorema" from Bruno Buchberger / RISC Linz does for
Mathematica.

PS: Could you PLEASE post your (preliminary) patch to the new()$Symbol bug to
IssueTracker or to this list -- then I'll put it on IssueTracker! I ran into
this bug again...

-------------------------------------------------------------------------------

Dear Cliff,

> [...] but currently I'm still trying to figure out dimensionless dimensions
> and other fun.  I guess I'm kinda hoping that by the time I finally get this
> well enough to try any actual coding the decision as to which path to take
> will have been made and progress begun.

You can safely code in either Spad or Aldor. There is even an automated
translater from Spad to Aldor, so this route is completely "safe". If you
decide to code in Aldor, backporting to Spad is mostly trivial --if you don't
use dependent types, that is.

PLEASE stick to your project! It is important to us, as you can see from that
commercial guy.

> A mathematical proof failing for a "minor" reason as opposed to a "major" one
> still fails,

As a mathematician: a "minor" mistake is one that can be fixed (by myself), a
"major" one is one that I don't know how to fix...


[big snip]

> mathematicians are very reluctant to accept the idea of computers as useful
> or reliable tools in matters such as proofs, and given the behavior of modern
> software its a bit hard to blame them.

Don't worry. Most Mathematicians I know accept Computer proofs meanwhile. The
point rather is that we would like to *understand* the proofs. And a paper and
pencil proof is usually easier to understand than two thousend lines of
computer generated calculations.

I made an experience I'd like to share: In the course of proving something, I
needed to prove that a certain polynomial inequality holds. I only knew that my
polynomial would have positive coefficients, to put you into the picture. I
failed. However, I was able to prove it for polynomials of degree 3.

For polynomials of degree 4, Mathematicas InequalitySolve proved
it. Unfortunately, I don't know how, since it only answered "True". Of course,
it did use a CAD, but it was impossible for me to see what it really did. I
hope that we can modify Renauds package so that
 
> a) Axiom and similar pieces of software are capable of constructing proof
> arguments for any and all mathematical outputs.

Again, I'm pretty sure that trying to prove the correctness of Axiom itself is
the wrong path. If you are *really* interested and have the talent, go
ahead. But if you think that anybody would use Axiom because it was proven
correct, I'm sure that you are mistaken.
 
> > > Of course, the current compiler and interpreter for Axiom's extension
> > > language ("spad"), is written in a dialect of lisp (called "boot"), which
> > > itself is written in lisp.
 
> If I may ask, how come the boot step is needed?  

As far as I know, it's a historical failure. Some people working on Axiom
didn't like Lisps parens and prefix notation...

> Do we need it in the Aldor -> Lisp translation?  I understand the need to
> limit the power of Lisp in Aldor

No, Aldor is just as powerful as Lisp in the Turing sense. From the programmers
perspective, it is not as powerful since it doesn't have macros. By the way,
Lisp was originally designed as a means to prove things about computer
language. It was at first not intended to be actually used for programming. So,
I'd say that proving things about Aldor programs will be much harder than
proving things about Lisp programs :-(

All the best and keep your Units project alive!

Martin