Re: [Axiom-developer] LogiWeb

[Ralf Hemmecke]

Hi Klaus,

> But if you explain what you are doing (e.g. giving an URL I should
> start with), then I would be able to say something about whether or
> not Logiweb would be helpful to you and, if it is, how it could be
> used.

Well I am terribly sorry that I forgot to point you to the homepage of
the open source computer algebra system AXIOM.

http://axiom-developer.org/

But I guess, the information there is not organized enough for everyones
taste. So if you don't understand something, it's probably better to ask
on the axiom-dev list.

Maybe a good start would be to download the Axiom book (it's free) or 
try out AXIOM online inside the WIKI.

> Yes. It is an infrastructure more than anything else. One can publish
>  'pages' (or 'papers' or 'pamflets' if you like) on it. Such pages
> can be flat TeX, but they may also contain programs, lemmas, proofs,
> and similar. A page can also define what to do with formal contents
> (e.g.: compile the programs, run programs on specified data, render
> the output, invoke particular proof systems on particular proofs, and
> much more).

Oh, that sounds even more interesting that you can already compile
programs that are hidden in papers. In fact, currently a pamphlet file
is nothing else than an ordinary input file for noweb
(http://www.eecs.harvard.edu/~nr/noweb/). They contain the programs and
Makefiles are used to extract and build the program. In fact, one
pamphlet contains only a part of the whole AXIOM CAS.

BTW, what tool to you use to translate TeX into HTML?

> > Think of the Axiom Journal idea.

That idea is still a dream. But basically, I would like to be able to
take a paper and a system then grabs all the references in it and builds
the underlying AXIOM CAS as the author of the paper used it. So I should
be able to get back in time to get to the same situation as the author.
Maybe lamda calculus is abstract enough to make porting to future
platforms a non-issue. I really think your LogiWeb idea should be
exploited in our computer algebra context. In fact, I am happy to see
already connections to proof systems since joining CAS and theorem
provers is the future.

> > LogiWeb is GPL. The only drawback I see is that it is basically a 
> > one-man-project.

> That is a decision I made. I have led several small and big software
>  development projects in academia as well as the industry. But
> Logiweb is made the Knuth way: if you cannot program it yourself, it
> is too complicated. There not one character in the source code that I
> have not typed myself. The Knuth approach takes time, but the result
> tends to be small and coherent.

I completely understand your decision, but now it might be time to open
it up. Which means more people than just you need to understand the
scary details. LogiWeb would be dead immediately if there happens
something dragically to you. How much is LogiWeb already in use
somewhere? What would be a good start to read about the overall
infrastructure and the internals? Any linearly readable text available?

> But from now on, anyone can continue the developement of the system 
> without touching the source code: Anyone can add facilities to
> Logiweb by publishing Logiweb pages containing the facilities. I
> intend to continue doing bugfixes, minor updates, and porting (and I
> would not mind getting help on that:-)

Does LogiWeb have some features like WEB, i.e. change files by which one
can modify the originally published program? (Honestly, I don't really
understand the details of Knuth's .ch files, but it sounds to me like a
necessary feature to remove bugs without touching the original sources.

> > And I am still not clear about what it really means to program in
> > pure lambda calculus.
>
> It means that if you want to define e.g. the factorial function, you
>  would reference a page (typically the 'base' page at logiweb.eu)
> which defines numbers, Booleans, pairs, exceptions, addition,
> multiplication, etc. in lambda calculus, and then you would write
> e.g.
>
> x ! == if x = 0 then 1 else x * ( x - 1 ) !

> Other programming languages can be supported. In particular, I will 
> support Pascal if the Mizar sources are released. And anyone can add
>  support for any language by publishing a Logiweb page which tells 
> Logiweb how to do.

Fine. But before anyone can add something as complicated as Aldor, it
would be necessary to understand the principles of how a language
specification can be written in LogiWeb.

> But, on Logiweb, anything ultimately compiles to lambda calculus (at
> least in principle).

I probably need more understanding of the internals for that. But it is
not my main concern now. I'd rather like to investigate how LogiWeb
could be good for AXIOM.

> > It sounds a bit scary to me, ...
>
> It is, for the one who has to implement the low level details. You 
> should not bother.

Maybe not now. But somebody has to bother in 50 years or earlier if we
get new supercomputers on which LogiWeb does not run.

> Could you give a good starting URL to Aldor/SPAD (maybe www.aldor.org
> for Aldor?).

Yes. You find the Aldor User Guide at
http://www.aldor.org/mediawiki/index.php/User_Guides_for_Compiler_and_Libraries
(Note that the HTML and .pdf versions slightly differ.)

Thank you for your mail. I very much hope that this will become a 
fruitful cooperation.

Best regards
Ralf