[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Call for help
From: |
Martin Baker |
Subject: |
Re: [Axiom-developer] Call for help |
Date: |
Mon, 27 Jul 2015 08:16:11 +0100 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0 |
On 26/07/15 20:27, address@hidden wrote:
Martin,
I like the idea of "specific mathematical axiom markup" as a first
cut. I will try this idea.
> There is a distinction to be made between mathematical AXIOMS for
> the category (e.g. associative) and SIGNATURES for the functions
> in a category (domain, package).
In order to discuss the issues I have invented some pseudo code below
for 4 interlinked lattice categories. I find it easier to invent
categories that don't already exist in Axiom library to avoid
discussions about what the original author intended.
My conclusions from this exercise are:
1) I have shown the Axioms/Identities/Theorems (or whatever they are?)
as comments but I think they should be part of the code.
2) I think they need to be inherited in the same way the function
signatures are. Otherwise the Lattice category would have to duplicate
all the axioms for both the MeetSemilattice and the JoinSemilattice. So
domains would inherit axioms from categories. Proofs could still be done
at the domain level even if the axioms are specified at the category level.
3) Some categories could have exactly the same signatures but differ
only in their axioms.
4) Axioms are operator specific and not for the whole category. For
instance the lattice category inherits a commutativity axiom for join
and another commutativity axiom for meet. There is not just one
commutativity axiom. For more 'numerical' categories I guess we would
assume a commutativity flag applies to * and that + is always
commutative but relying on assumptions like that does not seem to
generalise well.
Martin
-------------------------------------------------------------------------
)abbrev category MEETLAT MeetSemilattice
++ Description: meet semilattice
++ Implementations in logic, sets and orders
++ Axiom: commutativity forall(x,y): x/\y=y/\x
++ Axiom: associativity forall(x,y,z): (x/\y)/\z=y/\(x/\z)
++ Axiom: unit forall x: x/\true()=x
++ Axiom: idempotence forall x: x/\x=x
MeetSemilattice: Category == SetCategory with
_/_\: ($, $) -> $
++ returns the logical 'meet', e.g. 'and'.
true: constant -> $
++ returns true.
)abbrev category JOINLAT JoinSemilattice
++ Description: join semilattice
++ Don't use for exterior Grassmann product operator as
++ that anticommutes
++ need to check precedence when used as an infix operator
++ Axiom: commutativity forall(x,y): x\/y=y\/x
++ Axiom: associativity forall(x,y,z): (x\/y)\/z=y\/(x\/z)
++ Axiom: unit forall x: x\/false()=x
++ Axiom: idempotence forall x: x\/x=x
JoinSemilattice: Category == SetCategory with
_\_/: ($, $) -> $
++ returns the logical 'join', e.g. 'or'.
false: constant -> $
++ returns false.
)abbrev category LAT Lattice
++ Description: lattice
++ Axiom: absorptionMeetOverJoin forall(x,y): x/\(x\/y)=x
++ Axiom: absorptionJoinOverMeet forall(x,y): x\/(x/\y)=x
Lattice: Category == Join(MeetSemilattice,JoinSemilattice)
)abbrev category DISTLAT DistributiveLattice
++ Description: not every lattice is distributive so treat this
++ as a different case
++ Axiom: distribution1 forall(x,y,z): x/\(y\/z)=(x/\y)\/(x/\z)
++ Axiom: distribution2 forall(x,y,z): x\/(y/\z)=(x\/y)/\(x\/z)
DistributiveLattice: Category == Lattice
- [Axiom-developer] Call for help, daly, 2015/07/25
- Re: [Axiom-developer] Call for help, daly, 2015/07/25
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help,
Martin Baker <=
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/27
- Re: [Axiom-developer] Call for help, daly, 2015/07/27
- Re: [Axiom-developer] Call for help, daly, 2015/07/27