Re: [Axiom-developer] Axiom mathematical algorithms... Notation matters

[daly]

> How do you see this with respect the literate programming model?
> 
> Gene

I am deep in the Numerics at the moment and a lot of it involves
matrix manipulation. The notation in the referenced paper is a
lot clearer than the linear notation, making it clear which
array access corresponds to which matrix element. If you know
the algorithm this isn't a problem but if you don't know the
algorithm the usual linear notation for programs is opaque.

In addition, it shows local variables in traditional math style
as opposed to "programmer style" things like
   t1 := something
   t2 := something else
where t1 and t2 are poorly chosen names unrelated to the math.
It gets even more cluttered when the necessary coercions are added.

As for the literate programming model the Axiom textbook-style follows
the usual "explain the concepts" (with literature references), explain
the algorithm, (using the pseudocode), show the "formula" (in this case,
the Spad code), and show the proof. Axiom now automatically runs ACL2
(for the lisp code) and COQ (for the spad code) at build time. So far
there is one ACL2 proof. A COQ proof is in the works.

This "notation" fits best in the "explain the algorithm" step.
Latex makes it possible to do inline. The notation is intermediate
between the formula and the implementation.

Tim

> 
> On 3/19/2016 3:53 AM, daly wrote:
> > I've been thinking about the best method of presenting mathematical
> > algorithms. There is a gap between equations that represent the
> > mathematics and the actual code that represents the algorithm.
> >
> > The actual code has loops and does low-level data manipulation
> > that has been optimized away from the formula definition. This
> > is especially true of numerics, where I've been doing a lot of
> > recent work.
> >
> > The form of presentation in this paper seems to be the perfect
> > combination of formula and algorithm. See, for example, p14:
> > http://slicot.org/objects/software/reports/SLWN2014_1.pdf
> >
> > It would be ideal if this was the Axiom algebra language (Spad2?).
> > Constructing a parser/compiler for such input is easily a PhD thesis.
> > It would represent a major step forward in computational mathematics.
> >
> > That said, I think we should adopt this style for documentation.