Maude-help mailing list

[Paco Durán <duran AT lcc.uma.es>]

Hi, 

Different advisories might be given, but the tool should still do something, 
and either give an error or a proof. The assoc-only case can be handle in 
many situations, and I'd say this is one of them. 

I'll look into the details as soon as possible. 

Thanks for the report,

Francisco


> On 10 Jan 2020, at 18:01, 
> <hcantunc AT gmail.com>
>  
> <hcantunc AT gmail.com>
>  wrote:
> 
> 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.

Attachment: smime.p7s
Description: S/MIME cryptographic signature