Maude-help mailing list

[<hcantunc AT gmail.com>]

Hello,

I have the following specification.

(mod TEST is
sort Value .

var A : Value .

op _._ : Value Value -> Value [ctor assoc] .

eq A . A = A .

endm)

I use the MFE tool https://github.com/maude-team/MFE and try to check whether
this specification satisfies the Church-Rosser property. After I run the
command (ccr TEST .) I get the following warning and nothing else.

Advisory: could not find an operator _._ with appropriate domain in meta-
module
    TEST when trying to interprete metaterm '_._['A:Value,'A:Value,
    'Y@@@:`[Value`]].
Advisory: could not find an operator _._ with appropriate domain in meta-
module
    TEST when trying to interprete metaterm '_._['A:Value,'A:Value,
    'Y@@@:`[Value`]].


There are some work in the literature which addresses this issue, which is
cited in the Maude manual:
https://link.springer.com/chapter/10.1007/978-3-642-16310-4_6

which says "the very challenging case of associativity without commutativity
for which no finitary unification algorithms exist."

I was wondering if there's any way to achieve this.