Re: [Axiom-developer] Call for help

[daly]

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

Excellent!





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

Yes, they do have to be part of the code. They also have to be 
available at compile time because the medium term plan is to 
use them in the compiler.

Previous markups are in comments just like you did below. See, for
instance, AbelianSemiGroup, which includes (minus latex)

++  Axioms:
++    associative("+":(%,%)->%) (x+y)+z = x+(y+z)
++    commutative("+":(%,%)->%) x+y = y+x

These could be added by making the compiler aware of another block.
That is, the compiler would know about

)abbrev category FOO Foo
Foo: Category == Bar with
    sig1
    sig2
  == add
    sig1 == ...
  assuming
    AssociativeAxiom:
    CommuativeAxiom:
    Proviso1:
    Definition1:

There is a bit of a struggle between an Axiom-like syntax and a
COQ-like syntax. Axiom syntax would make it easier on the compiler.
COQ syntax would make it easier on the proof checker.

The real win would be to find an isomorphism between the two.
This ought to be possible, or at least reasonable, since they are
both trying to express the same facts.

Definition stanzas would add things needed in the proof but are not
normal mathematical axioms. 




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

Agreed. Inheriting is the only reasonable thing to do. 
(Ah, the future joy of hacking the compiler. Sigh.)

This also has the potential benefit of replacing the attributes with
references to axioms, e.g. 

  LeftIdentityAttribute becomes LeftIdentityAxiom. 

This feels much less ad-hoc.





>3) Some categories could have exactly the same signatures but differ 
>only in their axioms.

Can you give me an idea of where this might happen?
This isn't an obvious case.





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

Would this be covered by the current mechanism (using 'if' as in:

   if $ has Monoid
     x ** y == exp(y * log x)

Or perhaps we can re-think the 'if' and move the conditional cases
into their own categories. This would have the benefit of 
simpliying the compiler and the inheritance machinery. It would
have the down side of expanding the category lattice.

Tim