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:
(help .) shows the list of commands available in the tools.
(check Church-Rosser .) checks the Church-Rosser property of the default module.
(check Church-Rosser <module-name> .) checks the Church-Rosser property of the specified module. This feature can be
used to check the Church-Rosser property of any (Core) Maude or Full Maude module specified in the same Maude session.
(show CRC critical pairs .) shows
the reduced form of the critical pairs that could not be joined in the
last check Church-Rosser command. Those joined are not shown.
(show all CRC critical pairs .) shows the unreduced form of all critical pairs computed in the last check Church-Rosser command.
(check coherence .) checks the coherence property of the default module.
(check coherence <module> .) checks the coherence property of the specified module.
(check ground coherence .) checks the coherence property of the default module (with all defined operations frozen).
(check ground coherence <module> .) checks the coherence property of the specified module (with all defined operations frozen).
(show ChC critical pairs .) shows the critical pairs computed in the last check coherence or ground coherence command.
(show all ChC critical pairs .) shows the unreduced form of all critical pairs computed in the last check coherence or ground coherence command.
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).
