Zulip Chat Archive

Stream: general

Topic: Proving Axiom Sane


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 07 2019 at 08:04):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 07 2019 at 08:08):

Titles of what?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 07 2019 at 08:10):

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

view this post on Zulip Patrick Massot (Jun 07 2019 at 08:10):

or @Gabriel Ebner

view this post on Zulip Sebastian Ullrich (Jun 07 2019 at 08:12):

There isn't

view this post on Zulip Tim Daly (Jun 07 2019 at 08:13):

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

view this post on Zulip 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: May 16 2021 at 21:11 UTC