On 25/07/15 12:38, d...@axiom-developer.org 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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
