The version available here contain some bugs I'm currently working on. If you are interested in using the CRC, please, contact me ().

The Church-Rosser Checker (CRC) is a tool to help checking whether an order-sorted equational specification satisfies the Church-Rosser property. The tool can be used to prove such a property for equational specifications in Maude, that is, for Maude functional modules.

The goal of executable equational specification languages is to make computable the abstract data types specified in them by initial algebra semantics. In practice this is accomplished by using specifications that are ground Church-Rosser and terminating, so that the equations can be used from left to right as simplification rules; the result of evaluating an expression is then the canonical form that stands as a unique representative for the equivalence class of terms equal to the original term according to the equations. For order-sorted specifications, being Church-Rosser and terminating means not only confluence---so that a unique normal form will be reached---but also a sort decreasingness property, namely that the normal form will have the least possible sort among those of all other equivalent terms. Therefore, the tool's output consists of a set of critical pairs and a set of membership assertions that must be shown, respectively, ground-joinable, and ground-rewritable to a term with the required sort.

For computational purposes it becomes very important to know whether a given specification is indeed ground Church-Rosser and terminating. Establishing the ground Church-Rosser property for a terminating specification is a thorny issue. The problem is that a specification with an initial algebra semantics can often be ground Church-Rosser even though some of its critical pairs may not be joinable. That is, the specification can often be ground Church-Rosser without being Church-Rosser for arbitrary terms with variables. In such a situation, blindly applying a completion procedure that is trying to establish the Church-Rosser property for arbitrary terms may be both quite hopeless---the procedure may diverge or get stuck because of unorientable rules, and even with success may return a specification that is quite different from the original one---and even unnecessary if the specification was already ground Church-Rosser.

The Church-Rosser Checker can be used to check specifications with an initial algebra semantics that have already been proved terminating and now need to be checked to be ground Church-Rosser. Since, for the reasons mentioned above, user interaction will typically be quite essential, completion is not attempted. Instead, if the specification cannot be shown to be ground Church-Rosser by the tool, proof obligations are generated and are given back to the user as a useful guide in the attempt to establish the ground Church-Rosser property. Since this property is in fact inductive, in some cases an inductive theorem prover can be enlisted to prove some of these proof obligations. In other cases, the user may in fact have to modify the original specification by carefully considering the information conveyed by the proof obligations.

The tool is written entirely in Maude, and is in fact a rewriting logic executable specification of the formal inference system that it implements. A complete execution environment for the tool has been built in Maude, and it has been integrated within Full Maude. The tool treats equational specifications as data that is manipulated. The CRC computes critical pairs and membership assertions by inspecting the equations in the original specification. This makes a reflective design---in which theories become data at the metalevel---ideally suited for the task. Indeed, the fact that rewriting logic is a reflective logic, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the tool. The same reflective design has been followed for other tools, like the ITP (Maude's inductive theorem prover), and the coherence checker tool (ChC).

The very high level of abstraction at which the tool has been developed has made it relatively easy for us to build it, makes understanding its implementation, as well as its maintenance and extension, much easier than if a conventional implementation, say in C, C++, or Java, had instead been chosen. Thanks to the high performance of the Maude engine, these important benefits in ease of development, understandability, extensibility, and in flexibility for introducing formally-defined proof tactics, are achieved without sacrificing performance. Even though it has not been optimized for performance, and in spite of using reflection and sophisticated rewriting modulo associativity and associativity-commutativity, the tool has competitive performance.

A previous version of this tool, together with an inductive theorem prover to prove theorems about such specifications developed by Manuel Clavel, was developed as part of the Cafe project by Francisco Durán. The tool was updated to Maude 2.2 with the help of Miguel Palomino. The current tool only accepts order-sorted conditional specifications where each of the operators has either no equational attributes, or only the commutativity attribute. Furthermore, it is assumed that such specifications do not contain any built-in sort or function, and that they have already been proved terminating (using, for example, the MTT tool). The tool attempts to establish the Church-Rosser property modulo the commutativity of some of the operators by checking a sufficient condition. We plan to develop a version of the Church-Rosser Checker that will handle different combinations of assoc, comm, and id attributes.
 

The CRC 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 CRC tool is loaded we can enter any Full Maude specification as usual and check the Church-Rosser property by using the check Church-Rosser comand. Assuming that there is no alias, the Maude executable is not in the path, etc., you may use the CRC tool as follows---note that the Full Maude and Church-Rosser 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 <CRC-path>/crc.maude
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude 2._ built: ___ __ ____ __:__:__
             Copyright 1997-200_ SRI International
                   Thu ___ __ __:__:__ 200_

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

        Church-Rosser Checker __ `(___ __th`, 200_`)

Maude> (fmod NAT is
>   sorts Zero Nat .
>   subsort Zero < Nat .
>   op 0 : -> Zero .
>   op s_ : Nat -> Nat .
>   ops _+_ _*_ : Nat Nat -> Nat [comm] .
>   vars N M : Nat .
>   eq 0 + N = N [label nat01] .
>   eq s N + M = s (N + M) [label nat02] .
>   eq 0 * N = 0 [label nat03] .
>   eq s N * M = M + (N * M) [label nat04] .
>  endfm)
rewrites: 1929 in 33ms cpu (119ms real) (56743 rewrites/second)
Introduced module NAT

Maude> (check Church-Rosser .)
rewrites: 17863 in 47ms cpu (70ms real) (372200 rewrites/second)

Church-Rosser checking of NAT
Checking solution :
  cp for nat04 and nat04
    s(N@:Nat +(N*@:Nat +(N@:Nat * N*@:Nat)))
    = s(N*@:Nat +(N@:Nat +(N@:Nat * N*@:Nat))).
 

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.
• CRC 2e.

The only documentation currently available is a technical report for the previous version of the Church-Rosser 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