axiom-developer
[Top][All Lists]
Advanced

[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

```

reply via email to

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