[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.


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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]