Conditional Confluence

Nachum Dershowitz

Department of Computer Science, School of Mathematical Sciences

Tel Aviv University, Ramat Aviv, Tel Aviv 69978, Israel

                    nachumd@cs.tau.ac.il

Bernhard Gramlich Fakultät für Informatik, Technische Universität Wien Favoritenstraße 9 – E185/2, A–1040 Wien, Austria

                     gramlich@logic.at

Mitsuhiro Okada Department of Philosophy, Faculty of Letters, Keio University 2-15-45 Mita, Minato-ku, Tokyo 108-8345, Japan

               mitsu@abelard.flet.keio.ac.jp

G. Sivakumar

Computer Science and Engineering Department, Indian Institute of Technology

Bombay, Mumbai 400 076, India

                   siva@cse.iitb.ernet.in

Claus-Peter Wirth FR Informatik, Saarland University Postfach 15-11-50, D-66041 Saarbrücken, Germany

                      cp@ags.uni-sb.de

June 19, 2014

Abstract

Conditional rewriting has been studied in various different contexts, e.g. in algebraic data type specifications, as a computational paradigm combining logic and functional programming, and as key mechanism in rewriting logic. In these settings, a fundamentally important issue is whether a given conditional rewrite system has the Church-Rosser, or confluence, property. In this paper, we survey all known confluence criteria scattered over the literature within a uniform framework. In some cases we also present extensions and generalizations of known results. Moreover, we show by means of simplified counterexamples that dropping any precondition in these criteria is impossible. Finally, we characterize (local and general) confluence of conditional rewrite systems by means of a natural transformation into unconditional rewrite systems which sheds new light on well-known non-confluence phenomena in conditional rewriting.

meta comments: misc.

General Aspects:

Topic of the paper (focus):

• confluence of terminating ctrs:

– types: 0, 1, 2, 3 (4)

– equality: semi-equational, join, normal, oriented • for completeness: also other known criteria without termination

Structure of the paper:

• abstract

• introduction, motivation, contribution and overview

• preliminaries (on trs and) ctrs

• confluence criteria with proofs and counterexamples (main part)

• comparison with related work, discussion, related topics

• conclusion Presentation / terminology / notation:

• notation for ctrs?

• proofs: analytic figures or triangle diagrams?

• tables for results (criteria / types of ctrs / counterexamples)

• omit (2.2) in in favour of (3)? probably yes!

• main focus “join case”, then derive the rest Questions to be considered/solved:

• all/other types of CTRSs considered?

• syntactic/semantic notions of critical peaks covered?

• (un)decidability / computability issues

• examples (also new ones, from different domains)

• local vs. global versions of confluence criteria systematically considered?

• weakening(s) of normality possible?

• counterexamples to omitting any condition

• weakenings of decreasingness (for oriented deterministic CTRSs): quasi-reductive, quasi-simplifying

• …

Detailed Aspects:

General introduction and motivation:

• where is conditional (term) rewriting used, why is it important?

• why is confluence important?

• results obtained so far:

– scattered over the literature

– technically complex and challenging proofs

– very subtle phenomena in conditional rewriting as compared to ordinary (unconditional term) rewriting

– (inherent) difficulty and complexity of conditional rewriting Focus of the paper:

• focus here:

– confluence criteria for terminating conditional rewrite systems revisited in depth – confluence criteria for (possibly non-terminating) conditional rewrite systems

treated only briefly, for completeness

– unified presentation of known confluence criteria plus extended ones

– revised uniform proofs

– discussion of results and of potential generalizations/extensions Technical criteria and underlying papers:

(1) confluence via decreasingness ([DOS88a]) (2.1) confluence via left-linearity, normality, and shallow joinability ([DOS88b]) (2.2) confluence via overlay systems with joinable critical pairs ([DOS88b])

(3) confluence via quasi-overlay joinability of shared parallel critical peaks ([GW96]), generalizes overlay criterion of (2.2))

Main results and proof structures:

• …

• …

• … Related results, ideas and papers (chronologically):

• [BK86]: confluence of 2-CTRSs via orthogonality and normality

• [Toy88]: confluent (c)trs with membership conditions • [Siv89]: proofs and computations in conditional equational theories

• [DO90]: confluence, completeness of narrowing, built-in predicates, termination aspects, higher-order rewriting

• [DO88a]: Conditional Equational Programming and the Theory of Conditional Term Rewriting

• [DO88b]: Proof-Theoretic Techniques for Term Rewriting Theory

• [DO90]: A Rationale for Conditional Equational Programming

• [ALS94b]: On Conditional Rewrite Systems with Extra Variables and Deterministic Logic Programs (includes a confluence criterion under termination)

• [WG94]: only local termination assumption in confluence proof (for positive/negative CTRSs)

• [Gra95]: only local termination assumption in confluence proof (below some term s)

• [SMI95]: Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides (confluence criterion without termination, extends [BK86] to the case of extra variables in rhs)

• [Gra96e]: Termination and Confluence Properties of Structured Rewrite Systems (including conditional rewrite systems, confluence criteria, modularity)

• [Gra96b]: Confluence without Termination via Parallel Critical Pairs (notion of parallel critical pairs)

• [Wir95]: Syntactic Confluence Criteria for Constructor-Based Positive/Negative-Conditional Term Rewriting Systems (extremely technical and complicated)

• [Wir97]: Positive/Negative-Conditional Equations (including confluence criteria with

and without termination for pnctrs) Main contributions / differences to previous results (should be made as explicit as possible):

• uniform presentation in a unifying framework:

– classification of the various approaches and their underlying ideas, starting from the same basic proof attempt and the resulting difficulties

– counterexamples illustrating the problems

– historical discussion of related ideas and results

• previous preliminary presentations of these results scattered over several papers ([DOS88a], [DOS88b], [Siv89], [GW96], [Wir97])

• stronger local versions of (1) and (2.1) above

• improvements / generalizations / extensions:

– slightly generalized versions of decreasingness:

∗ require solvability of condition for considered substitutions before ordering checks; strictly more general, but non-effective in general

∗ left-to-right decreasingness

∗ compatibility with a termination pair

– generalized joinability of critical peaks, (in)feasibility of critical peaks

– substantially simplified counterexamples

– discussion of limits and of further conceivable weakenings of preconditions • systematic study of different types of CTRSs:

– condition types: join, normal, semi-equational, equational systems

– variable types: 1 (no extra variables), 2 (extra variables only in conditions), 3

(variables of rhs are in lhs or conditions), 4 (no restrictions)

• a precise characterization of local confluence Further important criteria:

• with termination:

– strongly deterministic and quasi-reductive 3-CTRSs with joinable critical pairs

are confluent ([ALS94b])

• without termination:

– orthogonal normal 2-CTRSs are (level-/shallow-) confluent ([BK86])

– non-overlapping, possibly non-left-linear TRSs with membership conditions are confluent ([Toy88]); extends confluence by orthogonality principle of [Ros73] (cf. also [Hue80]) to non-left-linear TRSs via a special from of CTRSs

– level-(shallow-)confluence of orthogonal properly oriented right-stable 3-CTRSs

([SMI95])

Miscellaneous aspects:

• extra variables in rhs

• logicality

• modularity

• transformational techniques

• ground confluence

• … meta comments: structure

Structure of the Paper:

Introduction and Overview:

• Where is conditional (term) rewriting used, and why is it important (fundamental)?

• Why is confluence important?

• Confluence criteria for (unconditional) TRSs: Newman, Critical Pair Lemma, confluence of SN TRSs via joinability of critical pairs; decidability.

• Confluence criteria for CTRSs:

– Known results scattered over the literature.

– Technically complex and challenging proofs.

– Very subtle phenomena in conditional rewriting as compared to ordinary (un-

conditional) rewriting

• Motivation for this paper:

– Surevy all known results in uniform framework, with proofs, and discussion of underlying ideas.

– Systematic investigation of possible extensions and generalizations.

• Main contributions (summary):

– Survey of all known confluence criteria for CTRSs unifying framework.

– A thorough discussion of the fundamental problems in conditional rewriting and the basic proof ideas for confluence criteria.

– Simplified counterexamples to dropping conditions in known confluence criteria.

– Various improvements, generalizations and extensions of previous (positive) results.

– A precise characterization of local confluence of CTRSs

• Main contributions (detailed):

– Uniform presentation in a unifying framework:

∗ classification of the various approaches and their underlying ideas, starting from the same basic proof attempt and the resulting difficulties

∗ counterexamples illustrating the problems

∗ historical discussion of related ideas and results

∗ previous preliminary presentations of these results scattered over several

papers ([DOS88a], [DOS88b], [Siv89], [GW96], [Wir97])

– stronger local versions of criteria (1) and (2.1) (see below)

– improvements / generalizations / extensions:

∗ slightly generalized versions of decreasingness:

· require solvability of condition for considered substitutions before ordering checks; strictly more general, but non-effective in general · left-to-right decreasingness · compatibility with a termination pair

∗ generalized joinability of critical peaks, (in)feasibility of critical peaks ∗ substantially simplified counterexamples

∗ discussion of limits and of further conceivable weakenings of preconditions – systematic study of different types of CTRSs:

∗ condition types: join, normal, semi-equational, equational systems

∗ variable types: 1 (no extra variables), 2 (extra variables only in conditions),

3 (variables of rhs are in lhs or conditions), 4 (no restrictions)

– precise characterization of local confluence of CTRSs

• Focus of the paper:

– confluence criteria for terminating conditional rewrite systems revisited in depth – confluence criteria for (possibly non-terminating) conditional rewrite systems

treated only briefly, for completeness

– underlying previous papers and their relationship

• Structure of the remainder of the paper:

– Preliminaries: needed notations and terminology for ARSs, TRSs, CTRSs.

– Basic Problems in Conditional Rewriting:

∗ semantics of equality in conditions (type of CTRS)

∗ extra variables in conditions, rhs

∗ one-step reducibility no longer syntactic matching problem, but undecidable in general

∗ variable overlaps become critical in general

∗ ...

– Confluence Criteria: Results (with Proofs) and Counterexamples:

(1) confluence via decreasingness ([DOS88a]) (2.1) confluence via left-linearity, normality, and shallow joinability ([DOS88b]) (2.2) confluence via overlay systems with joinable critical pairs ([DOS88b])

(3) confluence via quasi-overlay joinability of shared parallel critical peaks

([GW96]), generalizes overlay criterion of (2.2))

– Confluence Criteria: Further Extensions and Generalizations:

∗ slightly generalized versions of decreasingness:

· require solvability of condition for considered substitutions before ordering checks; strictly more general, but non-effective in general · left-to-right decreasingness · compatibility with a termination pair

∗ generalized joinability of critical peaks, (in)feasibility of critical peaks ∗ discussion of limits and of further conceivable weakenings of preconditions ∗ systematic study of different types of CTRSs:

· condition types: join, normal, semi-equational, equational systems · variable types: 1 (no extra variables), 2 (extra variables only in conditions), 3 (variables of rhs are in lhs or conditions), 4 (no restrictions)

– A Precise Characterization of Local Confluence

– Confluence Criteria: Other Known results (mention and discuss):

∗ with termination:

· strongly deterministic and quasi-reductive 3-CTRSs with joinable critical pairs are confluent ([ALS94b]) · what else?

∗ without termination:

· orthogonal normal 2-CTRSs are (level-/shallow-) confluent ([BK86]) · non-overlapping, possibly non-left-linear TRSs with membership conditions are confluent ([Toy88]); extends confluence by orthogonality principle of [Ros73] (cf. also [Hue80]) to non-left-linear TRSs via a special from of CTRSs · level-(shallow-)confluence of orthogonal properly oriented right-stable 3-CTRSs ([SMI95]) · what else?

– Discussion (possibly mix with conclusion):

∗ summarize obtained results

∗ discuss main ideas underlying the presented confluence criteria; discuss applicability issues(!); how to prove termination;

∗ discuss related work and ideas:

∗ [ALS94b]: extra variables in rhs (for SN CTRSs)

∗ [WG94]: only local termination assumption in confluence proof (for positive/negative CTRSs)

∗ [SMI95]: level-confluence of CTRSs with extra variables in rhs (confluence criterion without termination, extends [BK86] to the case of extra variables in rhs)

∗ [Gra95]: only local termination assumption in confluence proof (below some term s)

∗ [Wir95]: syntactic confluence criteria for constructor-based positive/negative CTRSs (extremely technical and complicated)

∗ [Gra96b]: confluence without termination via parallel critical pairs (notion of parallel critical pairs)

∗ [Wir97]: positive/negative-conditional equations (including confluence criteria with and without termination for pnctrs)

∗ also related: [DO88b], [DO88a], [DO90], [JW86], [Kap87b, Kap87a], [Kap84], [BGM87], [BGM88], [ALS94a], [YALSM97, YALSM00], [Gra94], [Gra95], [Gra96c], [Gra96b], [Gra96a], [Gra96d], [KMN88], …

∗ what else?

∗ what early papers should be mentioned, too?

∗ summarize obtained results (own and other ones, preferably with tables – Conclusion:

∗ repeat main contributions

∗ emphasize new insights (if any)

∗ provide ideas / suggestions for further research

– Bibliography: all relevant papers should be included! what is missing? what can be omitted / is subsumed elsewhere?

end of meta comments: misc.

1 Introduction and Overview

Conditional equational logic and its operational counterpart, conditional rewriting, is a basic framework that underlies various fields like algebraic specification, functional logic programming, rewriting logic, and rewrite based first-order theorem proving. It is a natural extension of (unconditional) equational logic and (unconditional term) rewriting. As in the latter case, for guaranteeing uniqueness of computation results, confluence or, equivalently, the Church-Rosser property, of conditional rewriting is of fundamental importance in these fields.

By Newman’s Lemma ([New42]), confluence of any terminating (abstract) rewrite relation is well-known to be equivalent to local confluence. For terminating (unconditional term) rewrite systems (TRSs for short) the Critical Pair Lemma of Knuth & Bendix ([KB70], [Hue80]) enables allows reduce the test of local confluence to checking joinability of all critical pairs of the system considered. Hence, for finite terminating TRSs, confluence is decidable. If the Critical Pair Joinability Test is not successful, a completion process may be initiated that tries to complete the given system into a logically equivalent and confluent one (cf. [KB70], [Hue81], [BD94]). The basic idea here is to by repeatedly compute and normalize critical pairs, and to generate new equations and corresponding rewrite rules from non-trivial normalized critical pairs, according to some fixed reduction ordering.

For terminating CTRSs, somehow surprisingly the Critical Pair Lemma does no longer hold, i.e., joinability of critical pairs is not equivalent to local confluence ([DOS88b, DOS88a]). Hence, in general testing confluence of terminating CTRSs by checking joinability of all critical pairs is not possible any more. Nevertheless, under certain additional preconditions a Critical Pair Test for checking confluence of terminating CTRSs is indeed possible. There are a couple of results of this type which, however, are scattered over the literature. A common feature of all these papers is that they are technically involved and have complex proofs. The latter fact is due to several very subtle phenomena in conditional rewriting as compared to ordinary (unconditional) rewriting.

In the current paper we collect previous results, discuss the underlying ideas and various ways of extending and generalizing them.

Our main contributions in this survey on conditional confluence are as follows (a more detailed summary will be given later in Section 7):

• We survey all known results in a uniform framework, together with complete proofs.

• We thoroughly discuss the relevant fundamental problems in conditional rewriting and the basic proof ideas for confluence criteria.

• We give substantially simplified counterexamples to dropping any precondition in these known confluence criteria.

• We develop various improvements, generalizations and extensions of previous (positive) results.

• We provide a complete characterization of (local and general) confluence of CTRSs via a natural transformational approach into corresponding TRSs.

We do hope that this state-of-the-art survey in characterizing and checking confluence of CTRSs helps to make known and new results widely accessible and to achieve further progress in the field.

The focus of the paper is on confluence of terminating CTRSs. The relevant papers on which we build here in particular are [DOS88a], [DOS88b] and [GW96]. Thus, in a sense the present paper is a substantially extended and revised version of these previous papers by the authors. For the sake of completeness, however, we also consider and summarize confluence criteria for (possibly) non-terminating CTRSs.

The remainder of the paper is structured as follows. In Section 2 we introduce needed basic notions, notations and terminology for abstract rewriting and (conditional) term rewriting. Then, in Section 3 we discuss various basic problems arising in conditional rewriting (which do not exist in the unconditional case). This concerns especially the following aspects:

• Due to the presence of equality in a conditional equation / conditional rewrite rule, there exist several natural ways of interpretating the operational semantics of equality in the conditions, giving rise to different classes of CTRSs.

• In contrast to unconditional rewrite rules (where one typically requires that variables in the right-hand side of a rule also appear in its left-hand side), for conditional rewrite rules it sometimes makes sense to allow extra variables in conditions and, possibly also, in right-hand sides. Again this yields different types of CTRSs.

• Because of the conditions, applying a conditional rewrite rule does not reduce any more to a simple syntactical matching problem, but becomes undecidable in general, even for terminating systems. We briefly touch the issue of how to guarantee decidability of the rewrite relation.

• Finally, and this is the most important topic w.r.t. the subject of paper, we discuss the problem of variable overlaps between conditional rewrite rules. For TRSs, such kinds of local divergences are trivially joinable, whereas in the conditional case this is not any more the case. In essence, this phenomenon is the source of the failure of the critical pair test for local confluence.

In the main Section 4 we present and discuss (partially generalized versions of) the confluence criteria for terminating (join) CTRSs, stemming from [DOS88a, DOS88b] and [GW96]. These criteria guarantee confluence of a terminating (join) CTRS R with joinable critical peaks provided one of the following criteria is satisfied:

(1) R enjoys a property stronger than termination, namely decreasingness ([DOS88a]).

(2) R is normal, left-linear and has shallow-joinable critical peaks ([DOS88b]).

(3a) R has overlay joinable critical peaks ([DOS88b]).

(3b) R has quasi-overlay joinable shared parallel critical peaks ([GW96]).

Since (3b) properly generalizes (3a), we will concentrate on (1), (2) and (3b). From these main technical results we derive a couple of consequences and corollaries. Actually, instead of (1)-(3b) we prove more general local versions of these results from which the global versions are derived immediately. Furthermore, we discuss the preconditions in all of these confluence criteria. We show by means of counterexamples that none of them can simply be dropped. Compared to the counterexamples in [DOS88b, DOS88b], the ones given here are much simpler and reveal more clearly what goes wrong without the respective precondition.

In Section 5 we then investigate further extensions and generalizations of the main results in Section 4. More precisely, we study here

• slightly generalized versions of decreasingness,

• generalized versions of joinability as well as (in)infeasibility of critcial peaks,

• the limits and further conceivable weakenings of the preconditions in the presented confluence criteria, and

• the case of other types (regarding extra variables) and classes (regarding the interpretation of equality in the conditions) of CTRSs, i.e., the question what similar or other confluence criteria hold for these cases.

The difficulty of obtaining confluence criteria for terminating CTRSs means that local confluence of such systems cannot be easily characterized in a direct way as it was the case for unconditional TRSs. In Section 6 we address this fact – for terminating as well as for non-terminating systems – and give a natural complete characterization of local confluence of CTRSs in the spirit of a Critical Pair Lemma, by a transformational approach. This characterization is primarily interesting from a conceptual point of view, but in some cases may also be of practical value.

Finally, in Section 7 we discuss in some depth related work and other known confluence criteria, both for terminating and (possibly) non-terminating systems. We point out and interrelate essential ideas from these papers. We also touch applicability issues for these criteria, i.e., the question of how to verify their preconditions. Last but not least, we give a concise tabular summary of (currently) known confluence criteria for CTRSs.

We conclude in Section 8 by summarizing our main contributions and emphasizing some (old and new) insights into the problem of (verifying) conditional confluence. Last but not least we sketch here some ideas and suggestions for further research in this direction.

2 Preliminaries

Preliminaries to be included:

• basic notions of ARSs (like confluence, termination, etc., arrow notations)

• terms, positions, variables, subterms, replacement, contexts

• CTRSs:

– basic definition with different types of equality in the conditions (semi-equational, join, normal, meta?, built-ins?)

– definition of rewrite relation

– depth of rewriting (slightly different from [DOS88b, DOS88a]!); notions for

depth: s →_{m} t, s →_{≤m} t

– variable conditions

– special case of unconditional rules

• encoding of conditions via an equality

• Definition 2.1 critical peaks and critical pairs, having joinable critical pairs/peaks

3 Basic Problems in Conditional Rewriting

Briefly discuss the following basic problems in conditional rewriting:

• semantics of equality in conditions (type of CTRS)

• extra variables in conditions, rhs

• one-step reducibility no longer syntactic matching problem, but undecidable in general

• variable overlaps become critical in general

4 Confluence Criteria: Results and Counterexamples

First let us recall the relevant results known from unconditional term rewriting.

Theorem 4.1 (Critical Pair Lemma for TRSs [KB70], [Hue80]) A TRS R is locally confluent iff R has joinable critical pairs.

It is well-known that local confluence implies confluence under termination for arbitrary ARSs.

Theorem 4.2 (Newman’s Lemma [New42]) A terminating ARS is locally confluent iff it is confluent.

Combining the two previous results yields the well-known confluence criterion for terminating TRSs.

Theorem 4.3 (confluence test for terminating TRSs [KB70]) A terminating TRS R is locally confluent (hence confluent) iff R has joinable critical pairs.

A stronger local version of this confluence criterion is easily obtained by only requiring termination of a given term t.

Theorem 4.4 (confluence test for terminating terms in TRSs) A terminating term in a TRS R is locally confluent (hence confluent) if R has joinable critical pairs.

The proof (of the “if-direction” here) is essentially the same as above, but by only considering the reduction graph of R below the considered term in the application of Newman’s Lemma (Theorem 4.2).

Next let us concentrate on conditional rewriting. Subsequently, for the rest of this section, we shall tacitly assume that every considered CTRS R always is a join CTRS of type 2, i.e., possibly with extra variables but only in the conditions.

From a naive point of view, one would hope that the above confluence criteria for TRSs also extend to the conditional case, with an appropriate extension of the notions of critical pair and joinability of the latter (see Definition 2.1)

However, this is not the case as was first observed in [DOS88b]. The following counterexample^{1} is much simpler than the original counterexample(s) of [DOS88b].

Example 4.5 (joinability of critical pairs is not sufficent for (local) confluence)

R = \{ \begin{matrix}(1) & f(x) → & g(b) & ⟸ g(x) ↓ f(b) \\ (2) & g(a) → & f(a) \\ (3) & a → & b \end{matrix} \}

This system is easily seen to be terminating. Its only critical pairs is obtained by overlapping the rule (3) into (2), yielding g(b) ←_{(3)} g(a) →_{(2)} f(a) which is joinable since we have f(a) →_{R} g(b) using (1) since the condition g(a) ↓ f(b) is satisfied because of g(a) →_{(2)} f(a) →_{(3)} f(b). However, R is not (locally) confluent as witnessed by the variable overlap

f(b) ←_{(3)} f(a) →_{(1)} g(b)

of (3) into (1). Here the attempt of closing the reduction diagram by a step of the form

f(b) →_{(1)} g(b)

fails since the condition to be verified, g(b) ↓ f(b) immediately leads to a cycle. In fact, both f(b) and g(b) are in normal form.

There are several different approaches to recover confluence criteria via critical pairs for CTRSs. In fact, it seems that any reasonable proof attempt for showing confluence of terminating systems with joinable critical pairs either has to require

(a) a strengthened termination assumption (which enables a justified inductive reasoning also when recursing into the conditions), or

(b) some syntactical restrictions on the rules and / or strengthened forms of joinability for critical pairs, which are exploited in an inductive proof using a well-founded ordering that is based on (an extension) of the reduction ordering corresponding to the termination assumption.

4.1 Confluence Criterion I: Strengthening Termination

In some sense, intuitively, the failure (of joinability of a variable overlap) in Example 4.5 above (with R a terminating(!) system) seems to be due to the cycle phenomenon mentioned above, i.e., to a non-proper decrease of the terms considered. This suggests to require a decreasingness property stronger than termination ([DOS88a]).

1a similar one is due to [Mid92] as mentioned in [Gra96e]

Definition 4.6 (decreasing CTRSs) A CTRS R is said to be decreasing if there exists a a well-founded ordering > such that

• > contains the proper subterm ordering ▷,

• > contains the reduction ordering →_{R}^{+}, and

• lσ > s_{1}σ, t_{1}σ, …, s_{n}σ, t_{n}σ for every rule l → r ⟸ s_{1} ↓ t_{1}, …, s_{n} ↓ t_{n} and every substitution σ.

Note that the last condition requires in particular that R has no extra variables in the conditions. Furthermore observe that > need not be monotonic. In Example 4.5 above, R is terminating, but obviously not decreasing because otherwise we would get e.g. f(b) > f(b) which contradicts well-foundedness of >.

Decreasing CTRSs enjoy many nice properties, since when applying a rewrite rule, verifying the conditions becomes a strictly simpler problem. In particular, basic rewriting notions like the following become decidable for finite decreasing CTRSs: one-step reduction, reachability, joinability, (ir)reducibility.

The following are some sufficient conditions for decreasingness.

Simplifying systems ([Kap87b]): A CTRS R is said to be simplifying if there exists a simplification ordering > (i.e., a well-founded monotonic ordering with the subterm property) such that

• lσ > rσ, s_{1}σ, t_{1}σ, …, s_{n}σ, t_{n}σ for every rule l → r ⟸ s_{1} ↓ t_{1}, …, s_{n} ↓ t_{n} and every substitution σ.

Reductive systems [JW86]: A CTRS R is said to be reductive if there exists a a well-founded ordering > such that

• > contains the reduction ordering →_{R}^{+}, and

• lσ > s_{1}σ, t_{1}σ, …, s_{n}σ, t_{n}σ for every rule l → r ⟸ s_{1} ↓ t_{1}, …, s_{n} ↓ t_{n} and every substitution σ.

Clearly, any simplifying system is reductive, and reductivity implies decreasingness, but not vice versa.

Example 4.7 (decreasingness properly extends reductivity) The CTRS

R = \{ \begin{matrix}(1) & a → & c & ⟸ b ↓ c \\ (2) & b → & c \\ (3) & f(b) → & f(a) \end{matrix} \}

is clearly terminating, and also decreasing, but not reductive, because there is no monotonic extension > of the reduction ordering →_{R}^{+} (that includes f(b) →_{R}^{+} f(a)) satisfying a > b.

Decreasingness is a natural sufficient criterion to recover the Critical Pair Lemma for CTRSs. We first prove a stronger local version of this result for which we need a local version of being decreasing.

Definition 4.8 (decreasing term) Given a CTRS R and a term s (over the signature of R), we say that s is decreasing w.r.t. R if s is (R-)terminating and if there exists a well-founded ordering > satisfying

• > ⊇ ▷,

• > ⊇ (→_{R}^{+})_{below s}, and

• lσ > s_{1}σ, t_{1}σ, …, s_{n}σ, t_{n}σ for every rule l → r ⟸ s_{1} ↓ t_{1}, …, s_{n} ↓ t_{n} and every substitution σ.

Theorem 4.9 (decreasingness confluence criterion, local version) Let R be a CTRS and s be a term (over the signature of R). Suppose s is decreasing w.r.t. R. Then s is confluent if R has joinable critical pairs. Proof: By induction using the well-founded ordering > and case analysis on the first steps in a divergence starting from any term s′ below s, i.e., with s > s′, we show that s′ is confluent. Decreasingness of s (and of s′) ensures that the induction hypothesis becomes applicable whenever we recurse into the conditions a rewrite rule. This reasoning applies in particular also for the case of a variable overlap.

As an obvious consequence of this we obtain the following global criterion.

Theorem 4.10 Let R be a decreasing CTRS. Then R is locally confluent and hence confluent iff it has joinable critical pairs.

4.2 Confluence Criterion II: Strengthening Structure of Joinability

Let us next reconsider Example 4.5, taking into account the depths of rewrite steps and sequences.

Example 4.11 (Example 4.5 reconsidered) We had one critical pair by overlapping (3) into (2), namely,

f(b) ←_{1} f(a) →_{1} g(b)

with the joining reduction sequence

f(a) →_{2} g(b)

of depth 2. It is obvious that there is no way here of closing the local divergence above by only reduction steps of depth 1.

This consideration suggests somehow to restrict the depths of joining reductions in critical pair divergences in a reasonable way, and motivates the following notions.

Definition 4.12 (shallow joinability / confluence, level confluence) A CTRS R is said to be shallow-confluent if for all terms s, t_{1}, t_{2} (and all m, n ∈ ℕ) with t_{1} ←_{R_{m}}^{∗} s →_{R_{n}}^{∗} t_{2} there exists a term u with t_{1} →_{R_{n}}^{∗} u ←_{R_{m}}^{∗} t_{2}. R is level-confluent if R_{k} is confluent for every k ≥ 0. We say that R has shallow-joinable critical peaks if for every instance t ← s → u of a critical peak of R with

t ←^{∗}_{m} s →^{∗}_{n} u

there exists some term v with

t →^{∗}_{n} v ←^{∗}_{m} u

Remark 4.13 It is easy to see that shallow-confluence and level-confluence can also be characterized using the depth of rewriting sequences as follows.

• R is shallow-confluent iff for all terms s, t, u (and all m, n ∈ ℕ) with t ←_{m} s →_{n} u there exists a term v with t →^{∗}_{n} v ←^{∗}_{m} u.

• R is shallow-confluent iff for all terms s, t, u (and all m, n ∈ ℕ) with t ←^{∗}_{m} s →^{∗}_{n} u there exists a term v with t →^{∗}_{n} v ←^{∗}_{m} u.

Furthermore, by definition shallow-confluence implies level-confluenec.

Remark 4.14 A subtelty in the definition of shallow-joinable critical peaks lies in the fact that we didn’t define this notion as follows: Any critical t ← s → u with t ←_{R_{m}} s →_{R_{n}} u for some m, n should imply the existence of some v with t →_{R_{n}}^{∗} v ←_{R_{m}}^{∗} u. With this definition we would get e.g. in Example 4.5 for the critical peak g(b) ← g(a) → f(a), by choosing m = 2 and n = 1, that for g(b) ←_{R_{2}} g(a) →_{R_{1}} f(a) we obtain joinability via g(b) ←_{R_{2}} f(a) as desired. However, the minimal choice of m and n above yields g(b) ←_{R_{1}} g(a) →_{R_{1}} f(a) and only g(b) ←_{R_{2}} f(a), hence no joinability of the desired form. In other words, this means that to ensure shallow-joinability (at least for critical peaks), in all instances of critical peaks t ← s → u one has to consider either

a) all m, n with t ←_{R_{m}} s →_{R_{n}} u, or

(b) the minimal m, n with t ←_{R_{m}} s →_{R_{n}} u, i.e., with t ←_{m} s →_{n} u.

Since (a) and (b) are equivalent, and since (b) is obviously easier to check than the infinitary (a), it is natural to use the depth of rewriting steps in Definition 4.12 above.

The following confluence criterion essentially relies on shallow-joinability.

Theorem 4.15 (shallow-confluence criterion, local version) Let R be a left-linear, normal CTRS and s be a term (over the signature of R). Suppose s is terminating (w.r.t. R). Then s is confluent if R has shallow-joinable critical pairs. Proof: By induction on the measure (m + n, u) using as well-founded ordering the lexicographic combination of the usual ordering > on natural numbers and of the “rewrite relation below s”, i.e., →_{R}^{+} +_{below s}. Here we consider divergences of the form u ←^{∗}_{m} t →^{∗}_{n} v with “t below s”, i.e., with s →^{∗} t and prove by induction the existence of some w such

that u →^{∗}_{≤n} w ←^{∗}_{≤m} v

As straightforward consequence of this local criterion we obtain the following result from [DOS88b].

Theorem 4.16 (shallow-confluence criterion, global version) Let R be a left-linear, normal and terminating CTRS. Then R is confluent iff it has shallow-joinable critical pairs.

Next we show that none of the preconditions (for confluence) in Theorem 4.16 can simply be dropped.

Left-linearity: Let’s consider the following variant of Example 4.5.

Example 4.17 (Left-linearity cannot be dropped in Theorem 4.16) The CTRS

R = \{ \begin{matrix}(1) & f(x) → & g(b) & ⟸ h(g(x), f(x)) ↓ c \\ (2) & g(a) → & f(a) \\ (3′) & a → & b & ⟸ h(g(a), f(a)) ↓ c \\ (4) & h(x, x) → & c \end{matrix} \}

is terminating, normal, not left-linear and has shallow-joinable critical peaks. The only such peak by overlapping (3′) into (2), g(b) ←_{2} g(a) →_{1} f(a), is shallow-joinable due to g(b) ←_{2} f(a) using the first rule and using (2) and (4) for the condition. Yet, R is not (shallow-)confluent, since the variable overlap f(b) ←_{2} f(a) →_{2} g(b) is not joinable.

Observe that the only purpose of taking (3′) instead of (3) here (as compared to Example 4.5 is to enforce the reduction step from a to b to have depth 2, hence to render the system shallow-confluent. The non-left-linear rule (4) is needed to make the system normal (cf. the conditions of (1) and (3)). ^{2} However, the price is to have a non-left-linear rule (4).

Shallow-joinability: Actually, we do already have a counterexample for this case:

Example 4.18 (Shallow-joinability cannot be dropped in Theorem 4.16) The CTRS R in Example 4.5 is left-linear, terminating and normal (since f(b) is an irreducible ground term), but violates shallow-joinability as shown, hence is non-(shallow- )confluent.

Normality: Again we consider a slightly different variant of Example 4.5, namely the following:

Example 4.19 (Normality cannot be dropped in Theorem 4.16) The CTRS

R = \{ \begin{matrix}(1) & f(x) → & g(b) & ⟸ f(x) ↓ g(x) \\ (2) & g(a) → & f(a) \\ (3′) & a → & b & ⟸ c ↓ d \\ (4) & c → & d \end{matrix} \}

is terminating, left-linear, has shallow-joinable critical peaks (as is easily verified), but is obviously not normal, since the rhs condition term g(x) of the first rule is non-ground. And, indeed, the system is not shallow confluent, hence not (locally) confluent as witnessed by the variable overlap of (3) into (1), f(b) ←_{2} f(a) →_{2} g(b). But the only way of finding a common reduct would be to apply the first rule to f(b) which is impossible since f(b) ↓ g(b) does not hold.

Observe that the only purpose of taking (3′) instead of (3) and adding rule (4) here (as compared to Example 4.5 is to enforce the reduction step from a to b to have depth 2, hence to render the system shallow-confluent. We could therefore also take the system

R = \{ \begin{matrix}(1) & f(x) & → & g(b) ⟸ f(x) ↓ g(x) \\ (2) & g(a) & → & f(a) \\ (3′′) & a & →_{2} & b \end{matrix} \}

2This could also be achieved in many other ways.

where the last rule (3′′) just indicates that the step from a to b should have depth 2 no matter how this is realized (of course, the relevant properties of the system should not be modified by the way this is done).

4.3 Confluence Criterion III: Strengthening Shape of Joinability

All counterexamples to confluence of terminating CTRSs with joinable critical peaks considered so far enjoy the property that they are not only overlapping, but also allow overlaps strictly below the root. In other words, none of the systems in Exmaples 4.5, 4.17, 4.18 (which is the same as in 4.5), 4.19 is an overlay system. This turns out to be essential and can be turned into yet another powerful positive criterion for confluence of terminating CTRSs. In order to provide some intuition for the basic problems and motivation for this approach let us give a simple, but instructive example.^{3}

Example 4.20 (non-overlays are essential [GW96]) The CTRS

R = \{ \begin{matrix}(1) & f(a, a) → & b \\ (2) & a → & b \\ (3) & f(b, x) → & b & ⟸ f(x, x) ↓ b \\ (4) & f(x, b) → & b & ⟸ f(x, x) ↓ b \end{matrix} \}

is terminating. It has two (symmetric) outside critical peaks (between the last two rules) with no feasible instances at all, and the two inside critical peaks f(b, a) ←_{1} f(a, a) →_{λ} b and f(a, b) ←_{2} f(a, a) →_{λ} b both of which are joinable from left to right: f(b, a) → b, f(a, b) → b, because in both cases the third or fourth rule, respectively, is applicable due to f(a, a) → b (using the first rule), hence f(a, a) ↓ b. However, R is not (locally) confluent. For instance, we have

lσ′ = f(b, b) ←_{2} f(b, a) = lσ →_{λ} rσ = b ,

where the rule l → r ⟸ P applied in the right step is f(b, x) → b ⟸ f(x, x) ↓ b, with matching substitution σ = {x ↦ a}, and where σ′ = {x ↦ b}. But the two reducts f(b, b) and b are both irreducible. In particular, lσ′ →_{λ,σ′,l→r⟸P} rσ′ does not hold. Intuitively, the reason for that is that recursively checking the condition (P σ′) ↓ leads to the shared parallel critical peak

f(b, b) _{{1,2}}← ∥ − f(a, a) →_{λ} b

which has a duplicated critical redex and which is not joinable. In other words, a variable overlap has become critical by duplication of the contracted (terminating) redex a in the condition. This suggests to prevent such situations in advance by incorporating a priori such critical situations into the definition of the relevant critical divergences to be analyzed, and naturally leads to the notion of shared parallel critical peaks.^{4}

Definition 4.21 (quasi-overlay joinability of innermost critical peaks) property (*)

3Note that like Example 4.18 this CTRS is also a counterexample to the confluence of terminating, left-linear, normal CTRSs with joinable, but not shallow-joinable, critical pairs.

4The precise form of the appropriate shared critical peak conditions below, however, in particular the required form of joinability, is quite subtle and emerged in [GW96] only from carefully analyzing various unsuccessful proof attempts.

Theorem 4.22 (technical key result for quasi-overlay joinable CTRSs) Theorem 6 in [GW96] Proof: detailed proof as in [GW96]

Consequences:

Theorem 4.23 (local criterion for confluence of terminating terms) Theorem 7 in [GW96] Proof: easy with Theorem 4.22

Theorem 4.24 (global criterion for confluence of terminating terms) Theorem 8 in [GW96] Proof: Obvious from Theorem 4.24.

Theorem 4.25 (global quasi-overlay joinability of shared parallel critical peaks of terminating terms) Corollary 9 in [GW96]

adding an ordering:

Definition 4.26 (≻-quasi-overlay joinability of innermost instances of critical peaks) property (**)

Theorem 4.27 (≻-extended global criterion for confluence of terminating terms) Theorem 11 in [GW96] Proof: as in [GW96]

Theorem 4.28 (≻-quasi-overlay joinability of shared parallel critical peaks) Corollary 12 in [GW96]

An example of application of Theorems 4.27, 4.28:

Example 4.29 (example of applicability of ≻-quasi-overlay joinability)

R = \{ \begin{matrix}(1) & f(x, x) → & g(x, x) \\ (2) & a → & b \\ (3) & h(f(x, x)) → & a \\ (4) & h(g(x, y)) → & b & ⟸ h(f(x, y)) ↓ b \end{matrix} \}

Question: Find a confluent example where none of the crieria applies!

5 Confluence Criteria: Extensions and Generalizations

6 A Precise Characterization of Local Confluence

7 Discussion

7.1 Confluence Criteria: An Overview

8 Conclusion

References

[ALS94a] Jürgen Avenhaus and Carlos Loría-Sáenz. Higher order conditional rewriting and narrowing. In J.-P. Jouannaud, editor, Proc. 1st Int. Conf. on Constraints in Computational Logics (CCL’94), volume 845 of Lecture Notes in Computer Science, pages 269–284. Springer-Verlag, 1994.

[ALS94b] Jürgen Avenhaus and Carlos Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In F. Pfenning, editor, Proc. 5th Int. Conf. on Logic Programming and Automated Reasoning, volume 822 of Lecture Notes in Artificial Intelligence, pages 215–229, Kiev, Ukraine, July 1994. Springer-Verlag.

[BD94] Leo Bachmair and Nachum Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41(2):236–276, 1994.

[BDJ78] Daniel Brand, John A. Darringer, and William H. Joyner Jr. Completeness of conditional reductions. Technical Report RC 7404, IBM Research Center, Yorktown Heights, N.Y., December 1978.

[BGM87] Pier Giorgio Bosco, Elio Giovannetti, and Corrado Moiso. Refined strategies for semantic unification. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT’87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and Logic Programming and Specifications (CFLP), volume 250 of Lecture Notes in Computer Science, pages 276–290, Pisa, Italy, March 1987. Springer-Verlag.

[BGM88] Pier Giorgio Bosco, Elio Giovannetti, and Corrado Moiso. Narrowing vs. sld-resolution. Theoretical Computer Science, 59:3–23, 1988.

[BK86] J.A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323–362, 1986.

[DJ90] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Formal models and semantics, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243–320. Elsevier, 1990.

[DMS90] Nachum Dershowitz, Subrata Mitra, and G. Sivakumar. Equation solving in conditional ac-theories. In Hélène Kirchner and Wolfgang Wechler, editors, Proc. 2nd Int. Conf. on Algebraic and Logic Programming (ALP’90), volume 463 of Lecture Notes in Computer Science, pages 283–297, Nancy, France, October 1990. Springer-Verlag. ISBN 3-540-53162-9.

[DO88a] Nachum Dershowitz and Mitsuhiro Okada. Conditional equational programming and the theory of conditional term rewriting. In Institute for New Generation Computer Technology (ICOT), editor, Proceedings of the International Conference on Fifth Generation Computer Systems 1988, pages 337– 346, Tokyo, Japan, November 28–December 2 1988. 3 Volumes, OHMSHA Ltd. Tokyo and Springer-Verlag, 1988 ISBN 3-540-19558-0, 0-387-19558-0 and 4-274-19558-0.

[DO88b] Nachum Dershowitz and Mitsuhiro Okada. Proof-theoretic techniques for term rewriting theory. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), pages 104–111, Edinburgh, Scotland, UK, July 1988. IEEE Computer Society. ISBN 0-8186-0853-6.

[DO90] Nachum Dershowitz and Mitsuhiro Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

[DOS88a] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Canonical conditional rewrite systems. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 538–549. Springer-Verlag, 1988.

[DOS88b] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan and J.-P. Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 31–44, Orsay, France, 1988. Springer-Verlag.

[DP87] Nachum Dershowitz and David A. Plaisted. Equational programming. Machine Intelligence, 11:21–56, 1987. Oxford University Press.

[GM87] Elio Giovanetti and Corrado Moiso. Notes on the elimination of conditions. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Rewriting Systems (CTRS’87), volume 308 of Lecture Notes in Computer Science, pages 91–97, Orsay, France, July 1987. Springer-Verlag. ISBN 3-540-19242-5.

[GM88] Elio Giovanetti and Corrado Moiso. A completeness result for E-unification algorithms based on conditional narrowing. In M. Boscarol, L. Carlucci Aiello, and G. Levi, editors, Proc. Workshop on Foundations of Logic and Functional Programming (WFLP’86), volume 306 of Lecture Notes in Computer Science, pages 157–167, Trento, Italy, December 1988. Springer-Verlag.

[Gra94] Bernhard Gramlich. On modularity of termination and confluence properties of conditional rewrite systems. In Giorgio Levi and Mario Rodríguez-Artalejo, editors, Proc. 4th Int. Conf. on Algebraic and Logic Programming, Madrid, volume 850 of Lecture Notes in Computer Science, pages 186–203. Springer-Verlag, 1994.

[Gra95] Bernhard Gramlich. On termination and confluence of conditional rewrite systems. In Nachum Dershowitz and Naomi Lindenstrauss, editors, Proc. 4th Int. Workshop on Conditional and Typed Rewriting Systems, Jerusalem, Israel (1994), volume 968 of Lecture Notes in Computer Science, pages 166–185. Springer-Verlag, 1995.

[Gra96a] Bernhard Gramlich. Conditional rewrite systems under signature extensions: Some counterexamples. In K.U. Schulz and S. Kepser, editors, Proc. 10th Int. Workshop on Unification (Extended Abstracts), CIS-Bericht-96-91, Universität München, pages 45–50, June 1996.

[Gra96b] Bernhard Gramlich. Confluence without termination via parallel critical pairs. In H. Kirchner, editor, Proc. 21st Coll. on Trees in Algebra and Programming, volume 1059 of Lecture Notes in Computer Science, pages 211–225. Springer-Verlag, April 1996.

[Gra96c] Bernhard Gramlich. Confluence without termination via parallel critical pairs. In Proc. Coll. on Trees in Algebra and Programming (CAAP’96), 1996. To appear.

[Gra96d] Bernhard Gramlich. On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems. Theoretical Computer Science, 165(1):97–131, September 1996. special issue of ALP’94.

[Gra96e] Bernhard Gramlich. Termination and Confluence Properties of Structured Rewrite Systems. PhD thesis, Fachbereich Informatik, Universität Kaiserslautern, January 1996.

[GW96] Bernhard Gramlich and Claus-Peter Wirth. Confluence of terminating conditional rewrite systems revisited. In H. Ganzinger, editor, Proc. 7th Int. Conf. on Rewriting Techniques and Applications (RTA’96), volume 1103 of Lecture Notes in Computer Science, pages 245–259, New Brunswick, NJ, USA, July 1996. Springer-Verlag.

[HOHT97] S. Hattori, K. Okano, T. Higashino, and K. Taniguchi. Modularity of levelconfluence for conditional term rewriting systems with extra variables in righthand sides. In TGCOMP, 1997.

[Hue80] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, October 1980.

[Hue81] Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23(1):11–21, 1981.

[Hus85a] Heinrich Hussmann. Unification in conditional-equational theories. Technical Report MIP-8502, Univ. Passau, Passau, January 1985. (Corrigenda 1988).

[Hus85b] Heinrich Hussmann. Unification in conditional-equational theories. In Proc. EUROCAL ’87 (?), Lecture Notes in Computer Science, pages 543–553, Linz, Austria, April 1985. Springer-Verlag.

[JS86] Bharat Jayaraman and Frank S. K. Silbermann. Equations, sets, and reduction semantics for functional and logic programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, pages 320–331, Cambridge, Massachusetts, USA, 1986. ACM Press. August.

[JW86] Jean-Pierre Jouannaud and Bernard Waldmann. Reductive conditional term rewriting systems. In Proceedings of the 3rd IFIP Working Conference on Formal Description of Programming Concepts, pages 223–244. North-Holland, 1986.

[Kap84] Stéphane Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33:175–193, 1984.

[Kap87a] Stéphane Kaplan. Positive/negative conditional rewriting. In Stéphane Kaplan and J.-P. Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 129–143. Springer-Verlag, 1987.

[Kap87b] Stéphane Kaplan. Simplifying conditional term rewriting systems: Unification, termination and confluence. Journal of Symbolic Computation, 4:295– 334, 1987.

[KB70] Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K., 1970. Reprinted 1983 in “Automation of Reasoning 2”, Springer, Berlin, pp. 342–376.

[Klo92] Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 2–117. Clarendon Press, Oxford, 1992.

[KMN88] Deepak Kapur, D.R. Musser, and Paliath Narendran. Only prime superpositions need be considered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation, 1988(6):19–36, 1988.

[KW97] Ulrich Kühler and Claus-Peter Wirth. Conditional equational specifications of data types with partial operations for inductive theorem proving. In H. Comon, editor, Proc. 8th Int. Conf. on Rewriting Techniques and Applications (RTA’97), volume 1232 of Lecture Notes in Computer Science, pages 38–52, Sitges, Spain, June 1997. Springer-Verlag.

[Mar97] Massimo Marchiori. On deterministic conditional rewriting. Technical Report MIT LCS CSG Memo n.405, MIT, Cambridge, MA, USA, October 1997.

[Mid92] Aart Middeldorp. Personal communication, 1992.

[MS88] Chilukuri K. Mohan and Mandayam K. Srivas. Conditional specifications with inequational assumptions. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 161–178, Orsay, France, 1988. Springer-Verlag.

[MS89] Chilukuri K. Mohan and Mandayam K. Srivas. Negation with logical variables in conditional rewriting. In Nachum Dershowitz, editor, Proc. 3rd Int. Conf. on Rewriting Techniques and Applications (RTA’89), volume 355 of Lecture Notes in Computer Science, pages 292–310, Chapel Hill, North Carolina, USA, April 1989. Springer-Verlag.

[New42] Maxwell Herman Alexander Newman. On theories with a combinatorial definition of equivalence. Annals of Mathematics, 43(2):223–242, 1942.

[OG89a] Mitsuhiro Okada and Peter Grogono. New results in term rewriting theory. In ???, editor, Proc. of the Int. Conf. on Symbolic and Logic Computation, ???, page ???, ???, ??? 1989. ???

[OG89b] Mitsuhiro Okada and Peter Grogono. Practical application of conditional term rewriting systems. In ???, editor, Proc. IX Conf. of the Chilean Computer Sceince Society / XV Latin American Conf. on Informatics, ???, page ???, ???, ??? 1989. ???

[Ros73] Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20:160–187, 1973.

[Siv89] G. Sivakumar. Proofs and Computations in Conditional Equational Theories. PhD thesis, University of Illinois at Urbana-Champaign, 1989.

[SMI95] Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In J. Hsiang, editor, Proc. 6th Int. Conf. on Rewriting Techniques and Applications (RTA’95), volume 914 of Lecture Notes in Computer Science, pages 179–193, Kaiserslautern, Germany, April 1995. Springer-Verlag.

[Toy88] Yoshihito Toyama. Confluent term rewriting systems with membership conditions. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 228–241, Orsay, France, 1988. Springer-Verlag.

[WG94] Claus-Peter Wirth and Bernhard Gramlich. A constructor-based approach for positive/negative conditional equational specifications. Journal of Symbolic Computation, 17:51–90, 1994.

[Wir95] Claus-Peter Wirth. Syntactic confluence criteria for constructor-based positive/negative-conditional term rewriting systems. SEKI-Report SR-95-09, Fachbereich Informatik, Universität Kaiserslautern, 1995.

[Wir97] Claus-Peter Wirth. Positive/Negative-Conditional Equations. PhD thesis, Fachbereich Informatik, Universität Kaiserslautern, Verlag, Dr. Kovač, Hamburg, 1997.

[YALSM97] Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. In Max Dauchet, editor, Proc. Coll. on Trees in Algebra and Programming (CAAP’97), volume 1214 of Lecture Notes in Computer Science, pages 141–152, Lille, France, April 1997. Springer-Verlag.

[YALSM00] Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. Theoretical Computer Science, 236(1,2):209–232, 2000.