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 <care...@mcmaster.ca
<mailto: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
<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
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
