Coherence is a key executability requirement for rewrite theories, and therefore for Maude system modules. It allows reducing the, in general undecidable, problem of computing rewrites of the form [t]E U A -> [t']E U A, with A a set of equational attributes (associativity, commutativity, identity) for which matching algorithms exist, to the much simpler and decidable problem of computing rewrites of the form [t]A -> [t']A.

The Maude Coherence Checker (ChC), which is written in Maude using a reflective design as an extension of Full Maude, provides a decision procedure  for order-sorted---these are system modules whose only membership axioms are implicit ones, taking the form of subsort and operator declarations, and such that only equations (resp., only equations and rewrites) can appear in conditional equations (resp., conditional rules)---system modules whose equations and rules are unconditional. The only equational attributes supported by the current implementation are commutativity axioms, declared with the comm keyword. A future version will cover other attributes such as associativity-commutativity, and identity. The tool generates a set of critical pairs, whose coherence guarantees that of the entire system module. It then checks whether each of these pairs is coherent. The system module given as input to the tool is always assumed to be ground Church-Rosser and terminating. The Church-Rosser Checker and the Maude Termination Tool can be used to try to prove such properties.

For Maude system modules, which always have an initial model semantics, the weaker requirement of ground coherence, that is, coherence for ground terms, is enough. When the ChC tool cannot prove coherence---either because this fails, or because the input specification falls outside the class of decidable theories---it outputs a set of proof obligations associated with the critical pairs that it could not prove coherent. The user can then interact with the ChC tool to try to prove the ground coherence of the input system module by a constructor-based process of reasoning by cases. In the end, either:

1. all proof obligations are discharged and the module is shown to be ground coherent; or
2. proving ground coherence can be reduced to proving that the inductive validity of a set of equations follows from the equational part of the input system module, for which the ITP can be used; or
3. it is not possible to reduce some of the proof obligations to inductively proving some equations.

Case (3) may be a clear indication that the specification is not ground coherent, so that a new specification should be developed.

The ChC tool is written in Maude. It is a single file and for being used must be loaded as any other specification. It extends Full Maude, so the full-maude.maude file must be loaded before it (make sure you are using the latest version of Maude and Full Maude).

Once the ChC tool is loaded we can enter any Full Maude specification as usual and check the coherence property by using the check coherence comand. Assuming that there is no alias, the Maude executable is not in the path, etc., you may use the ChC tool as follows---note that the Full Maude and Coherence Checker tool files are given as arguments when running Maude, they could of course loaded later.

$ <Maude-path>/maude.bin <Full-Maude-path>/full-maude.maude <ChC-path>/chc.maude
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude 2._ built: ___ __ ____ __:__:__
             Copyright 1997-200_ SRI International
                   Thu ___ __ __:__:__ 200_

              Full Maude 2.__ `(___ __th`, 200_`)

            Coherence Checker _ `(___ __th`, 200_`)

Maude> (mod READERS-WRITERS is
>         protecting NAT .
>         sort Config .
>         op <_`,_> : Nat Nat -> Config [ctor] . --- readers/writers
> 
>         vars R W : Nat .
> 
>         rl [r1] : < 0, 0 > => < 0, s(0) > .
>         rl [r2] : < R, s(W) > => < R, W > .
>         rl [r3] : < R, 0 > => < s(R), 0 > .
>         rl [r4] : < s(R), W > => < R, W > .
>       endm)
Introduced module READERS-WRITERS

Maude> (mod READERS-WRITERS-ABS is
>         including READERS-WRITERS .
>         eq [e1] : < s(s(N:Nat)), 0 > = < s(0), 0 > .
>       endm)
Introduced module READERS-WRITERS-ABS

Maude> (check coherence .)
Coherence checking of READERS-WRITERS-ABS
Checking solution :
cp for e1 and r4
  < 1,0 >
  = < s N*@:Nat,0 > .

You need:

• Maude 2.3.
• Full Maude 2.3 (or from the Maude web site).
• crchc2a.maude or crchc2a.maude.gz (The Church-Rosser Checker and Coherence Checker tools are distributed together).

Previous versions

You need:

• Maude 2.2.
• Full Maude 2.2d.
• ChC 2.

The only documentation currently available is a technical report for the previous version of the Coherence Checker. It will be updated shortly.

Currently there are just a few examples available, we will try to add more soon.

Please, send any comments or questions to

06/04/2007