maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [Maude-help] Crchc3 and termination

From: Francisco Durán <duran AT lcc.uma.es>
To: Emmanuel Castro <emmanuel.castro AT laposte.net>
Cc: maude-help AT cs.uiuc.edu
Subject: Re: [Maude-help] Crchc3 and termination
Date: Tue, 17 Aug 2010 00:26:54 +0200
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
List-id: <maude-help.cs.uiuc.edu>

Hi Emmanuel,

If there are no critical pairs the tool says that the specification is
confluent. And if sort decreasing then Church-Rosser. Your specification can
still be nonterminating.

If all critical pairs can be discarded, either because joinable, unfeasible
or context-joinable, then the specification is locally confluent. If in
addition is terminating then it is confluent.

Cheers,

Francisco

El 15/08/2010, a las 21:29, Emmanuel Castro escribió:

> In Crchc3, if the command (check Church-Rosser .) terminates and reply that
> a module is Church-Rosser, can it be taken for granted that the module
> terminates ?
>
> Thank you for your replies
>
> Emmanuel CASTRO
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help

[Maude-help] Crchc3 and termination, Emmanuel Castro, 08/15/2010
- Re: [Maude-help] Crchc3 and termination, Francisco Durán, 08/16/2010
  - Re: [Maude-help] Crchc3 and termination, Emmanuel Castro, 08/17/2010
    - Re: [Maude-help] Crchc3 and termination, Francisco Durán, 08/19/2010