Re: [Axiom-developer] MathScheme project

[Jacques Carette]

Comments inline below.

On 2017-05-06 16:31 , Tim Daly wrote:

Jacques,

I'm reading your paper "The MathScheme Library: Some Preliminary

Experiments".  https://arxiv.org/pdf/1106.1862.pdf

The LeftNearSemiring description on page 4 is essentially

what I'm aiming to implement in Axiom.

Are you trying to do it as we are, by carefully building up the 'signature' via combinators?  I know Axiom has most of the needed infrastructure, except for 1) renaming, and 2) a notion of 'join' that properly solves the "diamond problem".  That's the big difference between MathScheme and Axiom.  See paper [2] below.

We differ on the choice of 'axiom' vs 'proposition'. I see what you label

as 'axiom' as a continuation of the type signatures. You have

   * : (U, U) -> U

which in Type Theory is basically

   U : Type

   F : ( Type x Type ) -> Type

Similarly what you label as 'axiom' is really just another type signature

(per Curry-Howard) and I'd label it as a 'proposition'

Actually, we agree.  This is just a label - we use 'axiom' to mean 'signature of type prop'.  It's meant to be surface syntax closer to traditional mathematics.  As our internal core is dependently typed, there is no real difference.

So where '*' needs to be implemented in any Domain that inherits from

LeftNearSemiring the 'proposition'

associative_* := forall x,y,z:U  (x * y) * z = x * (y * z)

means any Domain which inherits from LeftNearSemiring would have to prove

those propositions using operations from the Domain being constructed.

Agreed.  That is exactly what we mean.

Jacques

Comments?

Tim

On Sat, May 6, 2017 at 11:32 AM, Jacques Carette <address@hidden> wrote:

Hello Tim.

I believe we've met -- but 10+ years ago, at either an ISSAC or an ECCAD.

In any case, Bill and I are quite familiar with Axiom.  We've had many conversations about it with James Davenport, Stephen Watt and Gabriel Dos Reis.

Yes, MathScheme is a current project.  Its main web site is available at http://mathscheme.cas.mcmaster.ca.  [The list of papers is out of date, we're working on that; and we are also open-sourcing various bits of it as we clean the implementation].

Personally, I would encourage you to build a proof-of-concept using Axiom and Agda (rather than Coq); or even Idris.  I believe the approach to proofs there is much closer to Axiom than what you will get with Coq.  Or, since you are at CMU, Lean ?

What you will undoubtedly encounter is that Axiom's current "batteries included" approach to library building where, for example, the Category AbelianGroup [Book Volume 10.2, Category Layer 6, AbelianGroup.input on p.667 of the pdf at www.axiom-developer.org/axiom-website/bookvol10.2.pdf ] really builds abelian group as a Z-module.  While this is mathematically correct, it is not very modular.  At [1] we show how we have made this quite a bit more modular, using the combinators of [2].  To recover the "batteries included" version (which we believe in [3]), we have 'invented' Realms [4].  To us, Axioms' AbelianGroup Category is closer the AbelianGroup Realm than the fundamental 'theory' of AbelianGroup as found in textbooks.

We are also actively working on what you'd understand as rep/per. PL and logic people refer to this as reflection/reification (or quote and eval if you come from LISP).  In Coq, you have likely encountered ssreflect.  These are all instances of the same idea. Extremely powerful but also very dangerous.

Lastly, and perhaps most importantly, we have spent years thinking about how to have a properly typed Expr type.  In Axiom, this really has root in the 'eval' operation of InnerEvalable (and then Evalable and ExpressionSpace).  Expr is both absolutely essential, but extremely problematic as it 1) internalizes semantics, and 2) generally involves partiality (undefinedness) in deep ways.  If this interests you, we can forward a number of papers where we start to deal with that.

Sincerely,
Jacques

[1] https://arxiv.org/abs/1106.1862
[2] https://arxiv.org/abs/1204.0053
[3] http://imps.mcmaster.ca/doc/hlt.pdf
[4] https://arxiv.org/abs/1405.5956

On 2017-05-05 1:22 AM, Tim Daly wrote:

I'm Tim Daly, Lead Developer on Axiom.

I just came across this posting:
http://www.cas.mcmaster.ca/~carette/IR-MathScheme-Standard.pdf <http://www.cas.mcmaster.ca/%7Ecarette/IR-MathScheme-Standard.pdf>

Is this a current project?

I'm currently at Carnegie-Mellon doing research on proving Axiom
correct. As you're certainly aware, Axiom's category structure is
based on group theory.

In Type Theory you find the concept of typeclasses which have
three distinct parts:
  1) the "carrier" (aka the representation)
  2) the signatures of functions for the typeclass
  3) the propositions (aka types) that these fulfill.

Axiom has a domain called NonNegativeInteger (NNI) which is very
close to the usual 'nat' type in COQ. Lean, and other systems.

Currently in Axiom the Category supplies the signatures (2 above)
which a Domain (e.g. NNI) which inherits from the Category must
implement (e.g. =)

In Axiom the carrier (1 above) is a property of the Domain, which
allows Domains (aka Types) to have different representation. That
enables Axiom to have a sparse poly representation, a dense
poly representation, a recursive poly rep, etc., all of which inherit
from the same category structure, each in its own Domain.

Axiom is currently missing the propositions (3 above). Since Types
are Propostiion (Curry-Howard) there is a way to integrate the
propositions into the Category hierarchy.

A Category that requires a signature such as
  = : (x, y) -> Boolean
needs to also provide propositions for symmetry, reflexivity, and
associativity.

Any Domain that inherits from the Category would have to provide
proofs for the symmetry, reflexivity, and associativity propositions
using operations from the newly defined domain.

My current goal is to construct a proof-of-concept example using
Axiom and COQ.

I'd be interested in more information on your MathScheme project.

Tim Daly