Jacques, I'm reading your paper "The MathScheme Library: Some Preliminary The LeftNearSemiring description on page 4 is essentially 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 Comments? On Sat, May 6, 2017 at 11:32 AM, Jacques Carette <[hidden email]> wrote: Hello Tim. _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Comments inline below.
On 2017-05-06 16:31 , Tim Daly wrote:
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.
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.
Agreed. That is exactly what we mean. Jacques
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |