Re: Simplification rules

On 10 Aug 2006 15:04:19 +0200, Martin Rubey <[email protected]> wrote:
> 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)...

Right, sorry about that. Must have been hasty.

> 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!

That's what I suspected as well.

> 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))

Excellent! I've also noticed suchThat(), but apparently wasn't as good
at deciphering its documentation.

> 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)

Even if the rule gets evaluated a few more times than necessary the
example you provided seems to work. Thanks a lot!

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

That would explain infinite loops in simple minded rules like the
first one I thought of.

Igor