Re: [Axiom-developer] Axiom's Sane redesign musings

[Tim Daly]

Martin,

> Are there some fundamental compromises that have to be made when combining 
> computer > algebra and proof technology?

> For instance in proof assistants, like Coq, equations are types for instance:

> x = x + 0

> is a proposition which, by Curry-Howard, can be represented as a type. To 
> prove the
> proposition we have to find an inhabitant of the type (Refl).

> But in computer algebra I would have thought this equation would be an 
> element of
> some Equation type (I'm skipping over a lot of details).

> Do you think both of these approaches could be brought together in a
> consistent and elegant way?

> Also my (limited) understanding is that Coq prevents inconsistencies which
> makes it not Turing complete and therefore cant do everything Axiom can do?

Martin,

There are many problems with the marriage of logic and algebra. For instance,
the logic systems want proof of termination which is usually not
possible. Often,
though, a partial proof that does not guarantee termination is interesting and
sufficient. TLA provides some possible ideas in this direction.

Another problem is that in the generality of dependent types, full
type resolution
is undecidable (hence, a lot of the heuristics built into Axiom's interpreter).
Still there are interesting discussions of programs as proof objects ongoing at
the moment on the Lean discussion thread
https://leanprover.zulipchat.com/#

Still other problems arise in equational reasoning or probablistic algorithms.
I have looked at (and not really understood well) logics for these.

On the other hand, things like the Groebner Basis algorithm have been proven
in Coq. The technology, and the basic axioms, are gathering greater power.

In particular, since Axiom has a strong scaffolding of abstract algebra, it is
better suited for proofs than other systems. The fact that Axiom's compiler
insists on type information makes it somewhat more likely to be provable.

I have a very limited project goal of proving just the GCD algorithms in Axiom.

The idea is to create a "thin thread" through all of the issues so that they can
be attacked in more detail by later work. I've been gathering bits and pieces
of GCD related items from the literature. See Volume 13 for the current state
(mostly research notes and snippets to be reviewed)
https://github.com/daly/PDFS/blob/master/bookvol13.pdf

The idea is to decorate the categories with their respective axioms. Then to
decorate the domains with their axioms. Next to write specifications for the
function implementations. Then finding invariants, pre- and post-conditions,
etc. Finally, to generate a proof that can be automatically checked. So each
function has a deep pile of inheritated informaion to help the proof.

For example, a GCD algorithm in NonNegativeInteger already has the
ability to assume non-negative types. And it inherits all the axioms that
come with being a GCDDomain.

The fact that computer algebra really is a form of mathematics (as opposed
to, say proving a compiler) gives me hope that progress is possible, even if
difficult.

Do I know how to cross the "x=x+0" type vs equation form? No, but
this is research so I won't know until I know :-)

Tim

On 6/19/19, Tim Daly <address@hidden> wrote:
> Sane: "rational, coherent, judicious, sound"
>
> Axiom is computational mathematics, of course. The effort to
> Prove Axiom Sane involves merging computer algebra and proof
> technology so Axiom's algorithms have associated proofs.
>
> The union of these two fields has made it obvious how far behind
> Axiom has fallen. Mathematicians and some computer languages
> (e.g. Haskell) have started to converge on some unifying ideas.
>
> As a result, the new Sane compiler and interpreter needs to
> consider the current environment that mathematicians expect.
> This falls into several areas.
>
> 1) SYNTAX
>
> It is clear that Axiom's syntax and user interface has not kept
> up with the proof technology. A trivial example is a signature.
> Axiom likes:
>
>    foo : (a,b) -> c
>
> whereas Lean / Coq / or even Haskell prefers
>
>    foo: a -> b -> c
>
> Given that many systems (e.g. Haskell) use the second syntax
> we need to consider adopting this more widely accepted syntax.
>
> 2) PROOF and SPECIFICATIONS
>
> And, obviously, Axiom does not support 'axiom', 'lemma',
> 'corollary', nor any specification language, or any language
> for proof support (e.g. 'invariant').
>
> Mathematicians have these tools readily available in many
> systems today.
>
> 3) USER INTERFACE
>
> Axiom's command line interface and hyperdoc were fine for its
> time but Lean and Coq use a browser. For example, in Lean:
>
> https://leanprover.github.io/tutorial/
>
> or in Coq:
>
> https://jscoq.github.io/
>
> The combination of a browser, interactive development, and
> "immediate documentation" merges a lot of Axiom's goals.
>
> 4) CATEGORY STRUCTURE
>
> William Farmer and Jacques Carette (McMaster University)
> have the notion of "tiny theories". The basic idea (in Axiom
> speak) is that each Category should only introduce a single
> signature or a single axiom (e.g. commutativity). It seems
> possible to restructure the Category hierarchy to use this model
> wilthout changing the end result.
>
> 5) BIFORM THEORIES
>
> Farmer and Carette also have the notion of a 'biform theory'
> which is a combination of code and proof. This is obviously
> the same idea behind the Sane effort.
>
> 6) INTERACTIVITY
>
> As mentioned in (3) above, the user interface needs to support
> much more interactive program development. Error messages
> ought to point at the suspected code. This involves rewriting
> the compiler and interpreter to better interface with these tools.
>
> Axiom already talks to a browser front end (Volume 11)
> interactively but the newer combination of documentation
> and interaction needs to be supported.
>
> Sage provides interactivity for some things but does not
> (as far as I know) support the Lean-style browser interface.
>
> 7) ALGORITHMS
>
> Axiom's key strength and its key contribution is its collection
> of algorithms. The proof systems strive for proofs but can't
> do simple computations fast.
>
> The proof systems also cannot trust "Oracle" systems, since
> they remain unproven.
>
> When Axiom's algorithms are proven, they provide the Oracle.
>
> 8) THE Sane EFFORT
>
> Some of the changes above are cosmetic (e.g. syntax), some
> are "additive" (e.g. lemma, corollary), some are just a restructure
> (e.g. "tiny theory" categories).
>
> Some of the changes are 'just programming', such as using
> the browser to merge the command line and hyperdoc. This
> involves changing the interpreter and compiler to deliver better
> and more focused feedback All of that is "just a matter of
> programming".
>
> The fundamental changes like merging a specification
> language and underlying proof machinery are a real challenge.
> "Layering Axiom" onto a trusted core is a real challenge but
> (glacial) progress is being made.
>
> The proof systems are getting better. They lack long-term
> stability (so far) and they lack Axiom's programming ability
> (so far). But merging computer algebra and proof systems
> seems to me to be possible with a focused effort.
>
> Due to its design and structure, Axiom seems the perfect
> platform for this merger.
>
> Work on each of these areas is "in process" (albeit slowly).
> The new Sane compiler is "on the path" to support all of these
> goals.
>
> 9) THE "30 Year Horizion"
>
> Axiom either converges with the future directions by becoming
> a proven and trusted mathematical tool ... or it dies.
>
> Axiom dies? ... As they say in the Navy "not on my watch".
>
> Tim
>