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

[Tim Daly]

Yes, but even more than that.

The goal is to make Axiom a "trusted system" for the whole of
computational mathematics.

To do this, consider this (not entirely random) collection of systems
and facts:

1) Trusted systems are built using the de Bruijn principle. See, for example,
https://pdfs.semanticscholar.org/2498/8797cf3e98c3a4a7c3dc775f8c02ce252c33.pdf

The basic idea is to have a trusted kernel that is composed of
a small number of logic operations known to be correct. All other
operations get "compiled" into these trusted operations. This is
how the proof systems operate, by choosing a logic such as CIC
and then constructing a CIC kernel.

2) Axiom is really nothing more that a "Domain Specific Language"
on top of common lisp. For Axiom to be trusted, the lisp must be
trusted, which the whole of common lisp is not.

3) We would like a common lisp that is proven "down to the
metal". There is a lisp (not common lisp) kernel called Milawa
https://link.springer.com/article/10.1007/s10817-015-9324-6
that has this property. It starts with a proven kernel and builds
up layers (currently 11) towards ACL2, a common lisp theorem
prover.

4) There is a theorem prover called Matita which appears to be
of interest as another "intermediate step". See
http://matita.cs.unibo.it/index.shtml

5) There is also a newly forming Lean prover and I am trying
to follow along and get up to speed on it: See:
https://leanprover.github.io/

5) There is the mistaken belief that common lisp is a typeless
language. However, CLOS has defclass and every defclass
constructs a new type. So by careful design it is possible to
construct a "fully typed" domain specific language and compiler
in common lisp.

So what does this mean for a Sane Axiom system?

The game is to build the Sane compiler using CLOS so it is
strongly typed. The output of the compiler generates lisp code
that conforms to some (possibly higher, Axiom-specific) layer
of the Matita lisp. So compiler output would be in a provably
type-safe subset of lisp.

In addition, the Sane compiler is being constructed so that
the compiler itself can be proven correct. Everything in the
compiler is strongly typed as is its output.

Ultimately the goal is a proven Sane compiler that accepts
a provable Sane language for computer algebra which generates
proven computer algebra code running on a lisp that is
proven "down to the metal".

The end result is a trusted system for computational mathematics.

Like the blind philosophers, I can grab any part of this
elephantine system and describe it in great detail. My struggle
is to "envision the whole", make it sensible, and then construct
it in a provable way.

I've been at this for about 7 years now. I took 10 classes at
CMU. read several hundred papers (see the Axiom bibliography
volume, https://github.com/daly/PDFS/blob/master/bookvolbib.pdf)
and spent a few years "coming up to speed on the
proof theory" side of computational mathematics. Now I
finally have (poor) command of computer algebra, proof
theory, and provable programming. Having all the parts,
the question is "Can I construct the elephant?". I don't know.
But I am trying.

Tim


On 6/26/19, Martin Baker <address@hidden> wrote:
> Tim,
>
> When I read this I am picking up a slightly different flavor than what I
> got from your first message in the thread.
>
> You first message seemed to me to be about "merging computer algebra and
> proof technology" but this message seems to be about running the two in
> parallel.
>
> I really like the idea of merging the two because Axiom has a steep
> learning curve and proof assistants have a steep learning curve. If they
> were merged the leaning curve would still be steep but at least there
> would only be one.
>
> This seems to be more about:
> * specifying axioms (and other identities?) in the category.
> * decorating the domain with some denotational semantics stuff.
> then checking it, at compile time, by running a separate proof assistant
> program.
>
> Is this what you are suggesting.
>
> Martin
>
> On 26/06/2019 01:16, Tim Daly wrote:
>> Martin,
>>
>> My current "line of attack" on this research is to try to prove the
>> GCD algorithm in NonNegativeInteger.
>>
>> While this seems trivial in proof systems it is expensive to
>> compute from the inductive definition. While this seems
>> trivial in computer algebra, the implementation code lacks
>> proof.
>>
>> There are several steps I'm taking. I'm creating a new compiler
>> that handles Spad code with several new additions. The new
>> language (and the effort in general) is called "Sane".
>>
>> One step is to make sure the new compiler generates code
>> that runs in Axiom. This is challenging as there is almost no
>> documentation about Axiom internals so it all has to be
>> reverse-engineered.
>>
>> Next is the addition of "axioms" to the categories, such as
>> adding axioms for equality to BasicType, where equality is
>> defined to include reflexive and transitive properties.
>> (Equality, by the way, is probably THE most controversial
>> topics in logic, c.f. the univalence axiom in HoTT). These
>> axioms decorate the category signatures and are inherited.
>>
>> Next is the addition of axioms to domains, also decorating
>> the signatures with axioms.
>>
>> Next is the logical specification of properties of the data
>> type implementation of the domain, called the REP in
>> Axiom and the "carrier" in logic. For example, think of a
>> binary tree REP and what properties you can guarantee.
>>
>> Next is adding a specification for the operations that
>> implement the signatures. These are specific to each
>> function that a domain implements.
>>
>> Next is decorating code with pre- and post-conditions
>> as well as loop invariants and storage invariants.
>>
>> Next the collection of all of the above is cast into a form
>> used by a proof system (currently Lean) that implements
>> dependent types (Calculus of Inductive Construction).
>>
>> Next a proof is constructed. The resulting proof is attached
>> to the Axiom code. Proof checking is wildly cheaper than
>> proof construction and the new Sane compiler would
>> perform proof checking at compile time for each function.
>>
>> So if there is a breaking change somewhere in the tower
>> the proof would fail.
>>
>> Challenges along the way, besides reverse-engineering
>> the Spad compiler, include adding languages for stating
>> axioms, for stating REP properties, for stating function
>> specifications, for stating program properties, and for
>> stating proof certificates. The pieces all exist somewhere
>> but they are not necessarily compatible, nor well defined.
>>
>> Is this all possible to do? Well, of course, as this is all
>> "just mathematics". Do *I* know how to do this? Well,
>> of course not, which is what makes this a research effort.
>>
>> Ultimately I'm trying to build an instance of merging proof
>> and computer algebra at a very deep, proven level. Think
>> of it as a PhD thesis project without the degree incentive :-)
>>
>> Tim
>>
>>
>> On 6/25/19, Martin Baker <address@hidden> wrote:
>>> On 6/25/19, William Sit<address@hidden>  wrote:
>>>   > The expression  x = x + 0, whether treated as a type or an equation,
>>>   > can only make sense when x, =, + and 0 are clearly typed and
>>> defined.
>>>   > It makes little sense to me that this, as an equation, can be
>>> "proved"
>>>   > to be valid universally (that is, without the definition of, say +).
>>>
>>> If x is a natural number defined like this in Coq:
>>>
>>> Inductive nat : Set := O : nat | S : nat -> nat
>>>
>>> then x = x + 0 is not an axiom but is derivable.
>>> Of course this all depends on the structures and definitions, I didn't
>>> mean to imply that it is valid universally.
>>>
>>> On 25/06/2019 19:28, Tim Daly wrote:
>>>> The "elegant way" that Martin is questioning is the problem
>>>> of combining a certain kind of logic operation (refl aka
>>>> "reflection" where both sides are equal) with the notion of
>>>> a mathematical unit.
>>>
>>> I think that refl (short for "reflexivity" of = relation), is the usual
>>> abbreviation for the only constructor of an equality type in Martin-Lof
>>> type theory.
>>>
>>> I get the impression that this theory is very powerful in proof
>>> assistants and I am questioning if you proposing to build this into
>>> Axiom and how?
>>>
>>> Martin
>>>
>>
>