Re: Simplification rules

Dear Igor,

"Igor Khavkine" <[email protected]> writes:

> -> symr := g(b, (a | notOrdered?(a,b)) == g(b,a)

there are some typos hidden in the line above. The operation "rule" is missing,
"notOrdered?" is undefined, and you seem to be replacing g(b, a) by g(a, b)...

Still:

symr := rule g(b, (a | a < b)) == g(a, b)

does not seem to work. After some experimenting, it occurred to me that the
suchThat predicate "|" might refer only to a *single* variable. I.e., in

(a | a < b)

b seems to be taken to be a constant. Note however, that I did *not* verify
this claim!

Still, this idea leads to a workaround, by using hyperdoc and browsing
RewriteRule. Try the following:

g := operator 'g
swap := rule g(b, a) == g(a, b)
symr := suchThat(swap, [a,b], l +-> (output l; l.1 < l.2))

Unfortunately, the condition seems to be evaluated once too often. I have no
idea why:

(14) -> symr g(x,y)
   [y,x]
   [y,x]

   (14)  g(x,y)

(15) -> symr g(y,x)
   [x,y]
   [y,x]
   [y,x]

   (15)  g(x,y)

Maybe Axiom tries to apply a rule until the result doesn't change anymore...

Hope this helps,

Martin

PS: if you are going to do more serious stuff with symmetric functions, please
contact me once more. I'd expect that it would be wise to have an appropriate
domain. Maybe something like that does already exist...