Re: MathScheme project

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 <[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.  [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
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer