axiom-developer
[Top][All Lists]

Re: [Axiom-developer] Call for help

 From: Martin Baker Subject: Re: [Axiom-developer] Call for help Date: Sun, 26 Jul 2015 17:53:25 +0100 User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0

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

reply via email to