axiom-developer
[Top][All Lists]

## 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

```

reply via email to