Re: [Axiom-developer] Call for help

[Martin Baker]

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