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. 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' 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. Comments? Tim On Sat, May 6, 2017 at 11:32 AM, Jacques Carette <care...@mcmaster.ca> 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 >> >> >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
