Re: [Axiom-developer] Call for help

[Martin Baker]

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

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.

Martin