The Church-Rosser and Coherence Checkers (CRC 3 and ChC 3)

Both CRC and ChC have been integrated inside the Maude Formal Environment. You may want to check the MFE web site to get the latest version of these tools.

The Church-Rosser Checker (CRC) is a tool to help checking whether a (possibly conditional) order-sorted equational specification satisfies the Church-Rosser property modulo any combination of associativity, and/or commutativity, and/or identity axioms.

The Coherence Checker (ChC) is a tool to help checking whether a (possibly conditional) order-sorted rewrite specification is coherent modulo any combination of associativity, and/or commutativity, and/or identity axioms.

The tools have been written entirely in Maude and are in fact executable specifications in rewriting logic of the formal inference systems that they implement. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tools.

On the installation and use

The tools are entirely written in Maude as an extension of Full Maude. The latest version CRChC 3j works on Maude 2.6 and Full Maude 2.6. To start the tools one just needs to load the Maude code of the CRChC after  starting Full Maude. If maude is your Maude executable, the Full Maude file is full-maude.maude, and the CRChC program is in crchc3.maude, and everything is in the same directory or in your path, you can start the CRC and ChC tools as follows:

  $ maude full-maude crchc3
             \||||||||||||||||||/
           --- Welcome to Maude ---
             /||||||||||||||||||\
        Maude 2.6 built: Dec 10 2010 11:12:39
        Copyright 1997-2010 SRI International
           Thu Jul  7 18:35:00 2011

        Full Maude 2.6b March 20st 2011

    Church-Rosser Checker 3j - October 27th 2010
    Coherence Checker 3j - October 27th 2010


The commands available in the CRC and ChC tools are the following:
Their use and the syntax of the results is described in the CRC 3 Manual and the ChC Manual.

Once CRChC 3 has been started, we can enter a module and check whether it satisfies the Church-Rosser property as follows.

 Maude> (mod IDENTITY is
           sort S .
           op 0 : -> S .
           op _+_ : S  S -> S [comm] .
           op f : S -> S .
           vars X Y : S .
           eq [e1] : X + 0 = X .
           rl [r1] : f(X + Y) => f(X) + f(Y) .
         endm)

 Maude> (check Church-Rosser .)
 
 Church-Rosser checking of IDENTITY
 Checking solution:
 All critical pairs have been joined.
 The specification is locally-confluent.
 The specification is sort-decreasing.

 Maude> (check coherence .)

 Coherence checking of IDENTITY
 Coherence checking solution:
 The following critical pairs cannot be rewritten:
   cp for e1 and r1
     f(X:S)
     => f(0)+ f(X:S).

Download

You need:

Documentation and examples
 
Please, send any comments or questions to email address 07/05/2013