Re: [Axiom-developer] Call for help

[Raymond Rogers]

On 07/26/2015 12:53 PM, Martin Baker wrote:
> On 25/07/15 12:38, address@hidden wrote:
> > Axiom has moved into a new phase. The goal is to prove Axiom correct.
>
> Tim,
>
> Why not do the easy bit first and just mark up the operators, in 
> domains, with the following common Axioms/Identities?
>
> Only for functions with signature: ($,$)->Boolean
>
> reflexivity forall(x): x<=x
> antisymmetry forall(x,y): x<=y and y<=x implies x=y
> symmetry forall(x,y): x<=y and y<=x implies error
> transitivity forall(x,y,z): x<=y and y<=z implies x<=z
I have problems with antisymmetry and symetry.
> Only for operators with signature: ($,$)->$
>
> commutativity: forall(x,y): x o y=y o x
> associativity: forall(x,y,z): (x o y) o z=y o (x o z)
> unit: forall x: x o 1=x
> idempotence: forall x: x o x=x
> absorption1: forall(x,y): x o (x * y)=x
> absorption2: forall(x,y): x * (x o y)=x
> distribution1: forall(x,y,z): x o (y * z)=(x o y) * (x o z)
> distribution2: forall(x,y,z): x * (y o z)=(x * y) o (x * z)
>
> where 'o' and '*' are replaced with the actual operator symbol.
>
> Perhaps you could translate the above to COQ syntax?
>
> This might be the easy bit because you only need to check for the 
> above signatures and in most cases it is fairly well known if 
> operators obey these identities.
>
> What would be very interesting would be to have a program which 
> generates these identities, wherever they occur in the Axiom library, 
> put random values into the variables and check for non-compliance.
I was also thinking along similar lines; but are the above assertions 
that can be made x \in R  or tests/validations of input variables/arguments?
These are of course simple cases; but I love simplicity.
Random variables?   I wouldn't go there; for one thing "corner cases" 
have to done if nothing else.  As a matter of fact if you can find 
"corners" and prove consistency between "corners" (say a convex hull in 
function space) then proving corners is powerful in the sense we want.   
That is not trying all possibilities.  For instance equivalence 
relations might be phrased as an assertion of convexity inside certain 
things.  If you like I might be able to rattle on about this; of course 
it's probably my own eccentric terminology and I am studying Lie 
Groups/Algebra so am inclined to apply the ideas to types of toothpaste :)
Ray

--
 Two views on life:
life is an art not to be learned by observation.
George Santayana:Interpretations of Poetry and Religion
It's kinda nice to participate in your life
Raymond Rogers