axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] Call for help

 From: Raymond Rogers Subject: Re: [Axiom-developer] Call for help Date: Sun, 26 Jul 2015 13:35:34 -0400 User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.8.0



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