Re: MathScheme project

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 <[email protected] 
> <mailto:[email protected]>> 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
>     <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
>     <http://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 <https://arxiv.org/abs/1106.1862>
>     [2] https://arxiv.org/abs/1204.0053 <https://arxiv.org/abs/1204.0053>
>     [3] http://imps.mcmaster.ca/doc/hlt.pdf
>     <http://imps.mcmaster.ca/doc/hlt.pdf>
>     [4] https://arxiv.org/abs/1405.5956 <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>
>         <http://www.cas.mcmaster.ca/%7Ecarette/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
>
>
>

_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer