Zulip Chat Archive

Stream: general

Topic: Proving Axiom Sane


Tim Daly (Jun 07 2019 at 08:02):

In \cite[p~7}{Mour15} "Elaboration in Dependent Type Theory", there is an example of a semigroup structure which extends a has_mul structure.
The elaborator figures out this "chain" while defining "mul_assoc".

Axiom has similar separate structures (we call them categories, ... don't ask) that have a similar kind of chaining. Axiom has its own elaborator, although it is just a part of the compiler.

Does Lean provide a command / api to output fully elaborated structures?

Patrick Massot (Jun 07 2019 at 08:04):

Beware this paper is about Lean 2, not the current version or the next one.

Tim Daly (Jun 07 2019 at 08:05):

Do you have titles? I'll look them up and put them in the lean.bib file.

Patrick Massot (Jun 07 2019 at 08:08):

Titles of what?

Tim Daly (Jun 07 2019 at 08:09):

I assumed that if the elaboration has changed there is a paper that describes the new elaborator.

Patrick Massot (Jun 07 2019 at 08:10):

I don't think so, but you should ask @Sebastian Ullrich.

Patrick Massot (Jun 07 2019 at 08:10):

or @Gabriel Ebner

Sebastian Ullrich (Jun 07 2019 at 08:12):

There isn't

Tim Daly (Jun 07 2019 at 08:13):

Is there a command / api to show the full elaboration?

Tim Daly (Jun 08 2019 at 08:59):

Axiom has general type constructs like Group, Ring, Field which exports 'signatures' of functions that must be implemented (e.g. a multiply operator) by any domain (e.g. polynomials need to implement multiply). What Axiom lacks, and I am working to provide, are the 'axioms' that a Ring needs to satisfy and specifications of polynomials (e.g. the multiply operation) that define the operations. To do this I have to re-implement the Axiom compiler for the Axiom language (called Spad, short for Scratchpad).

The new compiler (called Sane) has the dual job of producing Axiom compatible code (common lisp functions) and Lean compatible proofs. I have done a 'first-cut' deep dive into the Lean source code. It seems that the Sane compiler needs to compile to Lean syntax (as well as common lisp). This is basically a 'dual tail' compiler.

Such a compiler would make Axiom's computer algebra functions available in Lean.

There are, of course, 'second level issues', such as proving the Sane compiler lisp output is correct. But, as we all know, "it's kittens all the way down" so it is not a simple job. But it does seem to be a realistic path forward, merging Axiom and Lean.


Last updated: Dec 20 2023 at 11:08 UTC