Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi,

I don't see anyway to do what you want: encoding transitivity requires
unification to find the middle element and Maude only supports
matching conditions which require the rhs of the := to be fully
instantiated.

While we may support unification in the future it won't be supported
for fmods; rewriting with unification (aka narrowing) has severe
confluence and termination issues and is normally only useful with a
strategy.

Steven

On Wednesday 17 November 2004 01:55 pm, Ding, Hui wrote:
> Can we specify the following rule in Maude functional module? I cannot
> figure it out.
>
> If PropertyMap (AA, A, B) = BB and PropertyMap (BB, B, C) = CC
> Then PropertyMap (AA, A, C) = CC
>
> AA stands for a certain property of component A, and BB stands for a
> certain property of component B. "PropertyMap (AA, A, B) = BB" means
> component A's property AA is mapped to component B's property BB. That is,
> the above is a transitive rule.
>
> The sort, op, vars declaration is as follows:
>
> sort Component .
> sort Property .
> op PropertyMap: Property Component Component-> Property .
>
> vars AA BB CC : Property .
> vars A B C : Component.