On 07/26/2015 12:53 PM, Martin Baker wrote:
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
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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
