Re: [Axiom-developer] Catching up on internals

[Tim Daly]

You're correct. My primary focus is on Spad code.

In a logic setting there are things called Typeclasses which are roughly

equivalent to Axiom Categories. Typeclasses have 3 parts:

   signatures    -- just like Axiom

   carriers        -- Axiom's Domain representation

   propositions -- formal properties

The fact that Axiom puts carriers in the domain allows us to have multiple

instances with the same signature set (e.g. Sparse vs Dense polynomials)

The fact that Axiom lacks propsitions causes us to invent a method of

declaring properties (e.g. commutative("*") ). This was fine for the 1970s

but mathematics has gotten much more precise and mechanical about

reasoning with such properties (e.g Coq, Agda, Isabelle, etc)

Mathematics has improved but Computer Algebra is still stuck in the

ad-hoc, informal rewrite semantics. It is time to use these research

results to improve Computer Algebra. Axiom has an excellent structure

based on Group theory which makes this feasible.

The Curry-Howard isomorphism is that propositions are types. That means

that propositions are part of the type declarations that should be in Axiom.

So instead of declaring 'commutative' we add the proposition stating the

commutative property to the appropriate Category.

Given a domain, e.g. NNI, we should be able to collect all of the propositions

it inherits from the Category chain and use them to prove properties of the

algorithms in the NNI domain, such as GCD(x,y) = GCD(y,x). Domain

specific properties can be added at the Domain level.

So step 1 is to decorate the categories with propositions. Which means that

step 0 is to be able to encode and distribute propostions. Which means that

step -1 is to figure out how to parse, represent, and manipulate propostions.

step -2 is to see what has been done before in this area.

step -3 is to create a survey article... which is what I've been working on

and hope to publish before the end of this semester.

Prior efforts seems to be mostly about CA and Proof systems running

in parallel and communicating in order to provide user-level proofs.

I'm trying to unify the two areas of mathematics into a single,

consistent system where system level proofs provide trusted results.

That said, the work still needs to be grounded with lisp-level proofs

since Axiom relies heavily on lisp-level primitives like List types.

I've proven one of the lisp functions so far (using ACL2). I'm adding

type signatures to the lisp code and rewriting functions to be strongly

typed (and more in line with a functional programming style).

At the moment, during build Axiom calls ACL2 for the lisp proofs and

Coq for the Spad proofs (the first of which is still under construction).

Carnegie Mellon University has been exceptionally generous in giving

me access to logic courses (quite a few in the CS department these days).

I get to ask questions of professors who have pioneered logic research.

Tim

On Sat, Nov 4, 2017 at 4:38 AM, Martin Baker <address@hidden> wrote:

On 04/11/17 00:42, Tim Daly wrote:

On the other hand, my current effort involves proving Axiom correct. That
should (in theory) eliminate whole classes of errors. This is at the expense
of proving new code correct which tends to get a negative reaction from
developers.

Tim,

I know little about proving code correct (though it looks like an interesting topic) so I'm certainly not doubting anything you say. Its just that (in my ignorance) I would have thought it would have been easier to prove high level code correct than low level code and therefore, for this reason,  better to move boot code to SPAD than Lisp?

By 'high level code' I mean code with meaningful static types and semantics closer to mathematical structures.

Martin B