#27 Pattern matcher and hephys package

[Rainer Schöpf]

Certain forall rules for exponentials conflict with the simplication for hyphs expressions. Try this:

_______________________________________
index u;
vector v;
for all a,x let a^logb(x,a)=x;
(u.v)^2; %error
for all a,x clear a^logb(x,a);
(u.v)^2; %ok
___________________________________

When the pattern matcher tries the rule, it first replaces the free variable a by (u.v) and then tries to match the second argument to expt to logb(x,u.v). During simplification the error occurs.

The problem ist that (u.v) is part of a hephys expression, whereas the code in hephys.red assumes that it always sees complete such expressions.

Rainer

the hephys code assumes that no partial hepyhs expressions are simplified, which

[Rainer Schöpf]

Addendum: this particular example does no longer show the error, because of additional pattern match rules.

Replacing logb by an arbitrary operator triggers it:

index u;
vector v;
operator f;
for all a,x let a^f(x,a)=x;
(u.v)^2;

***** Unmatched index u