[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.

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] Call for help**, *daly*, `2015/07/25`
**Re: [Axiom-developer] Call for help**, *daly*, `2015/07/25`
**Re: [Axiom-developer] Call for help**, *daly*, `2015/07/26`
**Re: [Axiom-developer] Call for help**, *daly*, `2015/07/26`
**Re: [Axiom-developer] Call for help**, *daly*, `2015/07/26`
**Re: [Axiom-developer] Call for help**, *daly*, `2015/07/27`