Constructor-Based Inductive Validity in Positive/Negative-Conditional Equational Specifications

Claus-Peter Wirth, Bernhard Gramlich, Ulrich Kühler, Horst Prote

Fachbereich Informatik, Universität Kaiserslautern, D-67663 Kaiserslautern, Germany

                            wirth@informatik.uni-kl.de

June 12, 1993

Abstract: We study algebraic specifications given by finite sets R of positive/negative-conditional equations (i.e. universally quantified first-order implications with a single equation in the succedent and a conjunction of positive and negative (i.e. negated) equations in the antecedent). The class of models of such a specification R does not contain in general a minimum model in the sense that it can be mapped to any other model by some homomorphism. We present a constructor-based approach for assigning appropriate semantics to such specifications. We introduce two syntactic restrictions: firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative equations to be in the constructor sub-universe which contains the set of evaluation values of all constructor ground terms; secondly, we restrict the constructor equations to have “Horn”-form and to be “constructor-preserving”. A reduction relation for R is defined, which allows to generalize the fundamental results for positive-conditional rewrite systems, which does not need to be noetherian or restricted to ground terms, and which is monotonic w.r.t. consistent extension of the specification. Under the assumption of confluence, the factor algebra of the term algebra modulo the congruence of the reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more objects of the constructor sub-universe than necessary and which establishes one of the four notions of inductive validity of Gentzen clauses we discuss. To achieve decidability of reducibility we define several kinds of compatibility of R with a reduction ordering and present a complete critical-pair test for the confluence of the reduction relation. Keywords: Positive/negative-conditional specification, partial specification, constructor-based semantics, initial model, free model, inductive validity, constructor variables, order-sorted algebra, consistent extension, positive/negative-conditional rewriting, confluence, termination.

This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)

Contents

1 Introduction and Overview 1 2 Basic Notions and Notations 3

2.1 Sets and Classes, Multi-sets . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Motivation 9 4 More Basic Notions and Notations 23

4.1 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2 Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.3 Orderings and other (binary) Relations . . . . . . . . . . . . . . . . . . . 28 4.4 ⟶ , Confluence, andChurch − Rosser − P roperty . . . . . . . . . . . 29

5 Syntax and Semantics of Specifications 30 6 The Reduction Relation 34 7 How to Test for Confluence 41 8 Compatible CRSs 45

8.1 The Use of Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 8.2 Several kinds of Compatibility of CRSs . . . . . . . . . . . . . . . . . . . 52 8.3 Results for Compatible CRSs . . . . . . . . . . . . . . . . . . . . . . . . 55

9 Inductive Validity 59 10 Conclusion 72 A The Proofs 74 B Unification 101 References 107

1 Introduction and Overview

We present a constructor-based approach for assigning semantics to algebraic specifications with finite sets of positive/negative-conditional equations. In this approach, the nonconstructor function symbols can be used for (possibly partially) specifying functions on a domain of discourse supplied by the constructor terms and called the constructor subuniverse. For such partial specifications of functions, variables ranging over the constructor terms (or the constructor sub-universe) are likely to be more convenient than variables ranging over all terms (including “junk” terms) (or the whole universe), because the specifier usually^{1} does not intend to tell how the functions behave on objects that are “undefined” in the sense that they do not belong to the domain of discourse. Therefore we generalize unconditional equations not only by adding positive and negative conditions but also by allowing constructor variables in addition to the usual general variables.

In general, specifications with positive/negative-conditional equations lack an initial model. The most promising attempt in literature to overcome this problem has been that in Kaplan[28]. There, one of the quasi-initial models is distinguished from the other models by means of control information extracted from the rules, which must be compatible with a noetherian ordering. In addition, Kaplan gives a straightforward ground term reduction relation. However, his approach violates the paradigm of separation of logic and control and does not allow to express the distinction of his quasi-initial model without the control part of the specification. For this reason (among others), we choose a new different approach. Instead of using control information we introduce two syntactic restrictions:

A. For a condition to be fulfilled, the terms of its negative equations must be “defined” in the sense that their evaluations fall into the constructor sub-universe. This requirement is achieved by adding condition literals expressing this property and goes well with our intention of taking the constructor sub-universe as the domain of discourse.

B. We restrict the constructor rules (which express equalities among the constructor terms) to have “Horn”-form and to be “constructor-preserving”.

We then obtain the results of Kaplan[28] without using control information or noetherian orderings anymore. As a consequence, our reduction relation does not need to be noetherian or to be restricted to ground terms. Contrary to [28], we can show the monotonicity of this reduction relation w.r.t. consistent extension of the specification. As in [28], assuming confluence of our reduction relation, the factor algebra of the ground term algebra modulo the congruence of our reduction relation is a quasi-initial model for our specification. Unlike [28], however, it is also initial in the class of all models which do not identify more constructor ground terms than necessary.

To achieve decidability of reducibility and to enhance our means of testing for confluence, we define several kinds of compatibility of R with a reduction ordering, which enable us to present a complete critical-pair test for confluence of our reduction relation.

Finally, we define and disambiguate four notions of inductive validity of Gentzen clauses, compare them with notions found in literature, and show their monotonicity w.r.t. consistent extension of the specification.

The more difficult proofs of presented results can be found in appendix A.

1unless he wants to specify error-recovery or non-strict functions

2 Basic Notions and Notations

In this section we describe our non-standard basic notions and notations for sets and terms. More basic notions and notations (for substitutions, algebras, orderings, and reduction relations) can be found in Section 4.

2.1 Sets and Classes, Multi-sets

We use the following non-standard notation for classes A, B:

N_{+} := { n ∈ N | n ≠ 0 }
dom(A) := { a | ∃b : (a, b) ∈ A }  (domain)
ran(A) := { b | ∃a : (a, b) ∈ A }  (range)
field(A) := dom(A) ∪ ran(A)
B(A) := ⋂_{(A,C)∈B} C  (function application of B)^{2}
B[A] := { b | ∃a ∈ A : (a, b) ∈ B }  (relation application of B)
𝔓_{N}(A) := { S | S ⊆ A ∧ (S is finite) }
A^{∗} := { w : {0, 1, …, n − 1} → A | n ∈ N }  (set of words)
A^{+} := { w : {0, 1, …, n − 1} → A | n ∈ N_{+} }  (set of nonempty words)
id := { (a, a) | a is a set }  (identity-function)
V := dom(id)  (class of all sets)
A^{−1} := { (b, a) | (a, b) ∈ A }  (reverse of a relation)
A ∘ B := { (a, c) | ∃b : ((a, b) ∈ A ∧ (b, c) ∈ B) }  (product of relations)^{3}
A^{∘(0)} := id
A^{∘(i+1)} := A^{∘(i)} ∘ A for i ∈ N  (power of a relation)
A := ⋃_{i∈N} A^{∘(i)}  ( \begin{matrix}V-reflexive, transitive \\ closure of a relation \end{matrix} )
A^{⊕} := ⋃_{i∈N_{+}} A^{∘(i)}  ( \begin{matrix}transitive \\ closure of a relation \end{matrix} )

We use ∅ both for the empty set and the empty word. For application of the function f to i we write f_{i} besides f(i), such that w_{i} denotes the^{4} i^{th} “letter” of a word w. Speaking of a relation we always think of a binary relation unless indicated otherwise. We use ⊎ for the union of disjoint classes.

B(A) = { ; C  if A ∈ dom(B) ∧ ∀D : ((A, D) ∈ B ⇒ D = C) V  if A ∉ dom(B) “rubbish” otherwise

2As this set-theoretic definition might be difficult to understand, here is an equivalent one:

3This is very convenient for relations because a A b B c implies a (A ∘ B) c. It is, however, not generally considered the most convenient definition when A and B are used as functions because B(A(a)) = b (and not A(B(a)) = b) implies (A ∘ B)(a) = b, provided that a ∈ dom(A) and A(a) ∈ dom(B) .

4Notice that we start with 0 instead of 1

Multi-sets differ from sets only in their possibility to contain an element more than once. We denote them very similar to sets: ∅ denotes the empty multi-set as well as the empty set. We use ‘⟨’ instead of ‘{’, ‘⟩’ instead of ‘}’, ‘⊑’ instead^{5} of ‘⊆’, and ‘ ⊔ ’ instead^{6} of ‘∪’.

5A ⊑ B if each element occurring n-times in A occurs at least n-times in B

6Each element occurring exactly n-times in A and exactly m-times in B occurs exactly (n + m)-times in A ⊔ B.

⟨ f(i) | i ∈ I ⟩ denotes the multi-set containing an element ‘a’ exactly |{ i ∈ I | f(i) = a }| - times. FMul(S) denotes the set of finite multi-sets whose elements are in the set S.

It would be nice to keep the multi-sets as abstract as they are now. But as we do not want to introduce a duplicate of set-theoretic mathematics for multi-sets we have to be more concrete: We assume a multi-set to be a set that contains for each multi-set-element a occurring n-times in it n different representation set-elements^{7} â_{0}, …, â_{n−1} with ∀i < n : a = set(â_{i}) . To avoid confusion we don’t introduce an analogue of ‘… ∈ …’ for multi-sets, but write ‘… ∈ set[…]’ instead.

2.2 Terms

We will consider terms of fixed arity over many-sorted signatures. A signature

sig = (𝔽, 𝕊, α)

consists of an enumerable set of function symbols 𝔽, a finite set of sorts 𝕊 (disjoint from 𝔽), and a computable arity-function α : 𝔽 → 𝕊^{+}. For f ∈ 𝔽 : α(f) is the list of argument sorts augmented by the sort of the result of f; to ease reading we will add a ‘ → ’ after a nonempty list of argument sorts. A constructor sub-signature of the signature sig is a signature

cons = (ℂ , 𝕊, αℂ)

such that the set ℂ is a decidable subset of 𝔽. ℂ is called the set of constructor symbols; the complement ℕ = 𝔽 \ ℂ is called the set of non-constructor symbols.

[Signature with Constructor Sub-signature]

ℂ = {0, s, false, true, nil, cons}
ℕ = {, memberp}
𝕊 = {nat, bool, list}
α(0) =  nat
α(s) = nat  → nat
α(false) =  bool
α(true) =  bool
α(nil) =  list
α(cons) = nat list → list
α() = nat nat → nat
α(memberp) = nat list → bool

A variable-system for a signature sig is an 𝕊-sorted family of decidable sets of variable symbols which are mutually disjoint and disjoint from 𝔽. As the basis for our terms throughout the whole paper we assume two fixed disjoint variable-systems V_{SIG} of general variables and V_{CONS} of constructor variables such that for each s ∈ 𝕊 we have |V_{SIG,s}| , |V_{CONS,s}| ∉ N . By abuse of notation we will use the symbol ‘X’ for an 𝕊-sorted family not only to denote the family X = (X_{s})_{s∈𝕊} itself, but also the union of its ranges: ⋃_{s∈𝕊} X_{s} . T (sig, V_{SIG}⊎V_{CONS}) denotes the 𝕊-sorted family of all well-sorted (variable-mixed) terms over sig/V_{SIG}⊎V_{CONS}, while GT (sig) denotes the 𝕊-sorted family of all well-sorted ground terms over sig. Similarly, T (cons, V_{SIG}⊎V_{CONS}) denotes the 𝕊-sorted family of all (variable-mixed) constructor terms, T (cons, V_{CONS}) denotes the 𝕊-sorted family of all pure constructor terms, while GT (cons) denotes the 𝕊-sorted family of all constructor ground terms. To avoid problems with empty sorts, we assume GT (cons) to have nonempty ranges only. We will denote all terms in prefix-form without any confusing notational sugar (such as parentheses or commas).

7generated in some fixed manner (e.g. â_{i} := (a, i)) for intensional equality of multi-sets to imply extensional equality.

As exhibited in enhaus&Becker[1], its is adequate to describe our terms, substitutions, and algebras within the order-sorted framework in the style of Gogolla[22] or Smolka[40]: Take {SIG, CONS}×𝕊 for the sorts with the sort declaration that for each s ∈ 𝕊 the sort (CONS, s) is a sub-sort of the sort (SIG, s); and replace each arity declaration of the form α(f) = s_{0} … s_{n−1} → s_{n} with the arity declaration

α(f) ∋ (SIG, s_{0}) … (SIG, s_{n−1}) → (SIG, s_{n});

moreover, for f ∈ ℂ add the arity declaration α(f) ∋ (CONS, s_{0}) … (CONS, s_{n−1}) → (CONS, s_{n}).

A variable-system for a signature sig with sub-signature cons is defined to be a {SIG, CONS}×𝕊-sorted family V = (V_{ς,s})_{(ς,s)∈{SIG,CONS}×𝕊} of decidable sets which are mutually disjoint and disjoint from 𝔽. For denoting the {SIG, CONS}×𝕊-sorted family of variables occurring in a structure A (which might be a term or a list of terms, e.g.) we will use V(A). For denoting the 𝕊-sorted family of general (resp. constructor) variables occurring in A we will use V_{SIG}(A) (resp. V_{CONS}(A)).

Now the order-sorted notation for our sets of terms are the {SIG, CONS}×𝕊-sorted families T = (T_{ς,s})_{(ς,s)∈{SIG,CONS}×𝕊} and GT = (GT_{ς,s})_{(ς,s)∈{SIG,CONS}×𝕊} given by (s∈ 𝕊) T_{SIG,s} := T (sig, V_{SIG}⊎V_{CONS})_{s} , T_{CONS,s} := T (cons, V_{CONS})_{s} , GT_{SIG,s} := GT (sig)_{s} , and GT_{CONS,s} := GT (cons)_{s} .T oavoidconfusion : Notethat T_{CONS,s} ⊆ T_{SIG,s} fors ∈ 𝕊, whereas V_{CONS,s} ∩ V_{SIG,s} = ∅ .Ourcustomofreusingthesymbolofafamilyfortheunionofitsrangesnowallowstowrite T asashorthandfor T (sig, V_{SIG}⊎V_{CONS}) .

An occurrence (or position) is an element of N_{+}^{∗}. For a term t ∈ T we define the set of its occurrences (or positions) t recursively by: x = {∅} (x ∈ V) and

ft_{1} … t_{n} = {∅} ∪ ⋃_{1≤i≤n} { iq | q ∈ t_{i} } (f ∈ 𝔽; t_{1}, …, t_{n} ∈ T ) .

For a term t we denote by t/p the subterm of t at occurrence p and by t[ p ← t′] the result of replacing t/p with t′ at occurrence p in t. We write p ∥ q to express that neither p is a prefix of q, nor q a prefix of p. For P ⊆ t, ∀p, q ∈ P : (p ≠ q ⇒ p ∥ q), we denote by t [ p ← t′_{p} | p ∈ P ] the result of replacing for each p ∈ P the subterm at occurrence p in the term t with the term t′_{p}. A term t ∈ T is linear if ∀p, q ∈ t : (t/p=t/q ∈V ⇒ p=q) ; it is reducible w.r.t. a relation ⟶ if t ∈ dom(⟶).

We define the following sets of equations:

Eq(sig, X) := { ⟨t, t′⟩ | ∃s ∈ 𝕊 : t, t′ ∈ T (sig, X)_{s} } “set of undirected equations”
DEq(sig, X) := { (t, t′) | ∃s ∈ 𝕊 : t, t′ ∈ T (sig, X)_{s} } “set of directed equations”

3 Motivation

Just as with unconditional equations, the class of algebras satisfying a set R of positiveconditional equations^{8} contains an initial algebra, whereas reduction is more difficult because the equations only have to hold if their condition holds^{9}: The replacement of the left-hand side of an instantiated rule by its right-hand side is not known to be correct until the condition of the instantiated rule has been shown to hold in the initial model of R. Further problems occur when one allows negated equations among the equations of the conjunction that forms the condition. Kaplan[28] defines a [negated] equation in the condition to hold if its terms [do not] have a common reduct (w.r.t. ⟶^{∗}). If the resulting reduction relation is confluent and the rules are decreasing (cf. [16]) w.r.t. some ordering ▷, then its congruence closure is minimal (but not a minimum!) w.r.t. set-inclusion among the congruence relations whose factor algebra (w.r.t. the ground term algebra GT ) is a model^{10} of R. Despite of the lack of an initial model even in this restricted case, positive/negativeconditional equations are really necessary for convenient specification, as can be seen by the following example, where ‘⟵’ precedes the condition of an equation.

(continuing Example 2.2)

R: ⟵ ⟵ subsetp nil l  = true subsetp cons x k l = false  ⟵ memberp x l ≠ true subsetp cons x k l = subsetp k l ⟵ memberp x l = true

The Importance of Confluence

Why is confluence essential for reduction with positive/negative-conditional rules? Firstly (even without negative equations), confluence is needed for the completeness of testing semantic equality of two condition terms by looking for a common reduct^{11}. This means: We need confluence for the congruence defined in Kaplan[28] to yield a model of R. Secondly, it is needed for guaranteeing the congruence to be minimal, as can be seen from:

Let a, b, c, d, e be constants of the same sort, a ▷ b ▷ c ▷ d ▷ e.

R: \begin{matrix}c = d \\ c = e \\ a = b & ⟵ & e ≠ d \end{matrix}

Then, for the reduction relation of Kaplan[28]:

⟶ = { (c, d), (c, e), (a, b) } , whose congruence closure ⟷^{∗} is not minimal.

8By a positive-conditional equation we mean an equation that has associated with it a condition that consisting of a (possibly empty) conjunction of positive (i.e. not negated) equations. For a detailed treatment of positive-conditional equations cf. Kaplan[27].

9i.e. ∀x⃗ : (equation(x⃗) ⇐ condition(x⃗))

10taking the conditional equations as universally quantified formulas of first order equational logic (as indicated in footnote 9) and using standard algebra model semantics

11w.r.t. the reflexive and transitive closure ⟶^{∗} of ⟶

While confluence can be dropped for merely positive conditional equations by testing for congruence instead of testing for the existence of a common reduct of two condition terms, the situation is worse for positive/negative-conditional equations: It does not suffice to test non-congruence for inequality of two condition terms if confluence is not provided, as can be seen from:

Let the signature and the ordering be as in the previous example.

R: \begin{aligned}a = d \\ a = e & ⟵ & b ≠ c \\ b = c & ⟵ & d = e \end{aligned}

Any congruence yielding a model of R must contain (b, c): If it did not, it would contain (a, e) by the second rule, then by the first rule (d, e), and hence by the last rule (b, c). Therefore, no matter which congruence we actually use for condition-testing, the test of b≠c with such a (model-yielding) congruence will always fail, such that we cannot establish a⟷^{∗}e by testing the condition of the second rule, and hence cannot establish b⟷^{∗}c by testing the condition of the last rule. But R has the minimum model ‘a=d; b=c’, which cannot be obtained by the simple method of condition-testing anymore, but only by paramodulation and factoring instead, which in our opinion are too complicated for establishing just a simple reduction step.

By this we conclude that in case of negative equations in the condition, computation of a correct reduct by the method of condition-testing is only possible if confluence is provided.

Criticism of Kaplan[28]

The major shortcoming of the reduction relation in [28], however, is (as noted above) that its congruence closure is not a minimum^{12} but only minimal^{13} among the congruences yielding a model of R. There might be reductions s⟶t with s=t not holding in all models logically specified by R.

Kaplan[28] argues as follows: By writing ‘ c=d ⟵ d≠e ’ instead of the logically equivalent ‘ c=d ∨ d=e ’ the specifier adds some “operational” information to control the choice of the intended minimal congruence ‘c=d’ of the congruences yielding a model of R (‘c=d’, ‘d=e’, and ‘c=d=e’).

However, if the ordering context given by other rules does not allow e ▷ c , then the specifier is forced to write ‘ c=d ∨ d=e ’ in the form of ‘ c=d ⟵ d≠e ’. But even if he is allowed to specify his intended control information, he is likely to be unable to keep track of all consequences of his pieces of “operational” information. Moreover, the specifier must include some operational information into each rule he writes. All this would not be crucial, if the operational information were used only for admissibility of a specification, as is the case with our approach. But in Kaplan’s approach not only admissibility of a specification, but also its semantics itself is given by control and not expressible without; thereby violating the paradigm of separation of logic and control: R is not a logical specification (suitable for computation) anymore (as was the case with positive-conditional equations), but a program with none but operational semantics.

This loss of the pure logic view on a (admissible) specification has a consequence which is very important in practice: The monotonicity of logic is lost: (continuing Example 3) mbp 0 cons – 0 s 0 nil ⟶^{∗} false no longer holds after adding the rule – 0 s x 0. This shows that the completion of a partially specified function^{14} (here: ‘– ’) (even in a way that does not confuse different constructor terms) might destroy some reductions and congruences^{15} which were possible before.

12i.e. being smaller than anything else

13i.e. there is nothing smaller

Similarly, reduction of non-ground terms is of no use because the reduction relation is not stable:

As X ∈ V_{SIG} does not reduce to 0 , one might say

mbp 0 cons X nil ⟶^{∗} false.

But for X ↦ 0 this does not make any sense.

——————————————————————— The perfect model semantics approach of Bachmair&Ganzinger[5], which also includes a completion procedure, generalizes Kaplan’s approach [28] by abstracting the control information hidden in the syntactic form of rules into a reduction ordering which must be total on ground terms and which determines the construction process of perfect models. With our approach, however, reduction orderings are not at all needed for defining semantics. Cf. Becker[8] for the exact interrelation between the three approaches of Kaplan[28], Bachmair&Ganzinger[5], and us. Looking

for Remedy

One could think that the problem of a minimal congruence not being a minimum hardly arises or is avoidable by convenient purely syntactic restrictions on the defining rules. The following example will exhibit that such restrictions for the congruence of [28] cannot be reasonable in practice of specification:

(continuing Example 3) We exclude^{16} the function symbols 0, s, and (together with their respective rules), and enrich the signature with the following two constants: α(a) = α(b) = nat . The reduction relation ⟶ of [28] is confluent^{17} and noetherian^{18} in this case.

Consider the following two congruence relations on ground terms, given by their congruence classes for the sorts nat and bool:

\underline{⟷^{∗} :} \{a\}

{b}

{} ∪ { mbp x l | (x ∈ {a, b} ∧ (x does not occur in l)) } {} ∪ { mbp x l | (x ∈ {a, b} ∧ (x does occur in l)) }

\underline{∼ :} \{ a, b \}

{ , mbp a nil , mbp b nil }

{ } ∪ { mbp x l | (x ∈ {a, b} ∧ l ≠) }

Now, both ⟷^{∗} and ∼ yield a model of R. By a ∼ b ; a↚→^{∗}b ; we know that ∼ is not a minimum. By a b ⟷^{∗} and a b ≁ we know that ⟷^{∗} is no minimum either. But both ⟷^{∗} and ∼ are minimal among the congruences that yield a model of R. Hence their intersection does not yield a model of R.

14And partially specified functions are very useful in expressing exactly what is required by the specifier!

15by this we mean elements of ⟷^{∗}

16It’s not that they make trouble. We just omit them to make the example simpler.

17There are no feasible critical pairs

18Use the lexicographic path ordering given by ≻,

Notice that the example is really a standard specification example and not a sophisticated one. Therefore, restrictions on the structure of the rules for avoiding minimal non-minimum models would necessarily forbid such basic and essential specifications as the mbp-example above.

Thus, we have to choose between a ≠ b and mbp a cons b nil ≠ . As ⟷^{∗} is somehow more appealing than ∼ , one may argue that a ≠ b is somewhat more important than mbp a cons b nil ≠ by stating a, b to be constructors and thinking freeness of constructors to be more important than that of non-constructors. But this treatment does not solve the problem in general: If

1. a or b is changed into a (composite) non-constructor term, or (less likely)

2. mbp is stated to be a constructor symbol too, then the very same problem arises again.

Our Solution

Now, while the simple attempt above fails, the intended bias towards freeness of constructor terms can be achieved with the help of a new^{19} unary predicate ‘Def ’ (in addition to the binary predicate ‘=’) (cf. sect. 4) in the fol. way:

A. Adding condition literals expressing definedness for all terms of negative equations in the condition. In essence (cf. Definition 5), a term t is defined if ‘Def t’ holds if t has a congruent constructor ground term. For our example above this means that the last -rule is not applicable if a or b is undefined, thereby avoiding the problem of (1) above.

B. Forcing the constructor rules (which are the rules whose left-hand sides are constructor terms) to have no negative equations in their conditions and to be constructorpreserving, which means that all its terms are constructor terms and all its variables occur in its left-hand side. For our example above, this means that ‘mbp’ cannot be a constructor symbol, thereby avoiding the problem of (2) above.

(B) is purely syntactic and not very restrictive in practice as it only limits congruences between constructor terms (and this even less restrictively than usual). (A) is not a usage of control information as before. It just means that ‘≠’ is syntactically restricted to defined terms.

Undefined terms are due to incomplete knowledge about the model world or some partially specified function, by which we mean a function with symbol say ‘f’ for which the application “f(t_{0}, …, t_{n−1})′′tosomeconstructorgroundtermst_{0}, …, t_{n−1} is an undefined term. In the context of our specifications, functions are partially specified not because the specifier has explicitly stated their partiality as a property of importance, but because he has partially left open their definition, maybe due to partial information, due to irrelevance of the functions’ further behaviour for the specification in the current state of development, or even due to partiality being actually intended. Thus, partiality and undefinedness are not part of the specification but a result from its incompleteness. For this reason, the undefined terms are often thought to be equal to some unknown constructor ground terms:

Kapur&Musser[30, 31] consider those congruences which are maximally enlarged by random identification of undefined terms with constructor ground terms, as long as this identification does not identify two distinct constructor ground terms. Their intended congruence is then the intersection of all those maximally enlarged congruences. In Kapur&Musser[30] the maximal congruences are allowed to have some undefined terms left; this causes the problem that one cannot describe the intended congruence by model semantics^{20}. Therefore in Kapur&Musser[31] the intersection is done only over those congruences that have no undefined terms left: These congruences can easily be described in terms of model semantics: A model A is required to satisfy the following (besides making true the universally quantified equations of R): Let ⟷^{∗} denote the initial congruence of R (which exists because they consider unconditional equations only) and k its canonical consepimorphism from GT (cons) to GT (cons)/⟷^{∗} . Now the unique cons-homomorphism h from GT (cons)/⟷^{∗} to A given by kh = (AGT (cons)_{s})_{s∈𝕊} (cf. the Homomorphism-Theorem) is required to be an isomorphism. A third way of removing the undefined terms is to require h to be epimorphic instead of isomorphic, i.e. A is required to be cons-term-generated. While the theory of the last two approaches is beautiful, the resulting congruences may be very difficult to understand: One needs a sophisticated way of argumentation for showing two terms equal — even for some very simple examples.

19which is also necessary for sufficient expressibility for inductive theorem proving: Lemmas of the form “Def f(x_{0}, …, x_{n−1})” (with the x_{i} being different constructor variables), expressing that the symbol ‘f’ denotes a totally specified function, are very important for inductive theorem proving. Cf. Wirth[43].

Based on this tradition of thinking undefined terms to be possibly equal to constructor ground terms, the above item (A) of our approach can be justified the fol. way:

Considering dynamic extension of specifications: If two terms can be shown equal by ⟷^{∗}, they will keep being equal even if an undefined term will be identified with a defined term later on (cf. Theorem 6). On the other hand might an undefined term become equal to a previously unequal term when identifying an undefined term with a defined term. Thus, we had better be cautious: We should not pretend to be able to distinguish something undefined from anything else (as the former might in the sequel be defined to be the latter).

From a static point of view on the specification: Two distinct terms may be equal or unequal, no matter whether they are defined or undefined. In particular may an undefined term be both unequal to some distinct undefined term and equal to some other. This inequality between undefined terms, however, differs from the inequality between defined terms in that it is not considered sufficient for the fulfilledness of an inequality literal in the condition of an equation. This means that we have a “closed world assumption” which is restricted to the constructor ground terms, saying that two constructor ground terms are meant to be unequal unless their equality is specified by the constructor rules. According to this, we use “negation as failure” on the defined terms only, and not on the undefined terms where the specification is allowed to be incomplete and open.

20Of course, this is tried to be done in Kapur&Musser[30]. But their “inductive model” (which is defined to be a model with free constructors whose proper epimorphic images are no models with free constructors)

is a nasty thing: Normally, a model uses to keep being a model when one throws away some equations of the specification, thereby establishing the monotonicity of logic. The “inductive models” do not have this property. To see this take ℂ = {false, true, 0} ; ℕ = {s, zerop} ; R = { zerop 0 true , zerop s x false } . Now the following A is an “inductive model” for R but not for ∅ (where we need |A(nat)| = 1 ):

A(bool) = {FALSE, TRUE} ; A(nat) = {0, 1} ; true^{A} = TRUE ; false^{A} = FALSE ; 0^{A} = 0 ; s^{A}(x) = 1 ; zerop^{A}(0) = TRUE ; zerop^{A}(1) = FALSE .

We can also see by this that we indeed have no monotonic logic here: ∅ ⊢ 0 s 0 ; but (as seen by A):

R ⊬ 0 s 0 .

In the fol. sections we will show that by the little changes of (A), (B), we get a straightforward reduction relation ⟶ that has the following advantages (compared to the one of Kaplan[28]) (cf. sect. 6):

1. Its congruence closure ⟷^{∗} yields a model that is not only minimal but also the (up to isomorphism) uniquely determined minimum among those sig-term-generated models of R that do not identify more constructor ground terms than necessary (provided (as also required for Kaplan’s ⟷^{∗} to be minimal) that ⟶ is confluent).

2. ⟶ is monotonic w.r.t. the addition of new rules that do not have left-hand sides which are old constructor terms.

3. ⟶ is stable when defined also on non-ground terms.

As shown in the examples above, the reduction relation of Kaplan[28] has none of these properties. We will now revisit these examples to illustrate how our restrictions solve their problems.

1. (Example 3). If a and b are defined terms, then ⟷^{∗} becomes the minimum among those congruences which do not identify more constructor ground terms than necessary. Contrariwise, if a or b is undefined, then the intersection of ⟷^{∗} and ∼ becomes a model of R because the last mbp-rule now reads

mbp x cons y l mbp x l ⟵ , Def , Def ;

thus, mbp a cons b nil is neither nor now, but undefined instead.

2. (Example 3). We do not have mbp 0 cons – 0 s 0 nil ⟶^{∗} false anymore: mbp 0 cons – 0 s 0 nil is irreducible because – 0 s 0 is undefined.

3. (Example 3). As X is undefined: mbp 0 cons X nil −̸→^{∗} false .

Moreover, we are not only able to specify our semantics without using control information, but also able to remove the control aspect of requiring the rules to be decreasing for a specification to be admissible. As a consequence, our reduction relation does not need to be noetherian.

For a further comparison between the reduction relation of Kaplan[28] and the ground term restriction of our reduction relation, suppose that the rules in R are decreasing w.r.t. ▷. By induction over ▷ one can easily show the following: The two relations do not differ on constructor terms. If the reflexive & transitive closure of Kaplan’s relation is sufficiently complete, then ours contains Kaplan’s. If Kaplan’s relation is confluent, then ours is contained in Kaplan’s. If the reflexive & transitive closure of one of the relations is sufficiently complete and one of the relations is confluent, then there is no difference between our ground reduction relation and that of Kaplan[28]. Therefore in this important case, where all functions are totally specified and no undefined ground terms exist, we offer semantics for the reduction relation of Kaplan without using control information.

The perfect model semantics approach of Bachmair&Ganzinger[5], which also includes a completion procedure, generalizes Kaplan’s approach by abstracting the control information hidden in the syntactic form of rules into a reduction ordering which must be total on ground terms and which determines the construction process of perfect models. The perfect model semantics is very similar to Kaplan’s in that it still does not provide a pure logic view on specifications and in that it is still not monotonic w.r.t. consistent extensions of the specification. Cf. also Becker[8] for the interrelation between the three approaches of Kaplan[28], Bachmair&Ganzinger[5], and us.

Two types of variables

An additional feature of our presentation here, is our distinction between two kinds of variables. While the distinction between constructor terms and general terms is commonly accepted and considered fruitful, our distinction between constructor variables and general variables may require some explanation: General variables may be substituted by any term of the whole signature. Constructor variables, however, may only be substituted by pure constructor terms consisting of constructor function and constructor variable symbols. In the field of model semantics, this distinction is mirrored by the possible valuations: While a general variable can take the value of any object in the universe of its sort, a constructor variable can take the value of an object of the constructor sub-universe only.

General variables are the common ones in the field of term rewriting. They allow to express semantic properties that cannot be expressed by constructor variables.^{21} Furthermore, the general variables allow a higher abstraction from evaluation strategies than constructor variables which result in an innermost rewriting strategy in case of free constructors.

21Consider equations for error recovery or for non-strict functions whose meaning does not depend on the definedness of all its variables, e.g. “ or true Y true ”

Constructor variables are convenient in the field^{22} of inductive theorem proving for expressing important lemmas that do not hold for undefined terms^{23}. Semantically we could remove the whole order-sorted frame by considering ‘Def ’ to be an interpreted first-order predicate, stating for each c ∈ ℂ with α(c) = s_{0} … s_{n} that Def x_{0}x_{n−1} holds for ∀i < n : x_{i} ∈ V_{CONS,s_{i}} , and then by replacing each formula A containing a variable x ∈ V_{CONS} with the formula “ A{x↦X} ⟵ Def X ” for a new variable X ∈ V_{SIG}. While the order-sorted frame can therefore be considered to be syntactical, it is not just syntactical sugar, since it deeply influences termination and confluence of reduction relations. E.g., the means for automatically showing termination of the functions of classic inductive theorem proving (cf. Boyer&Moore[12], Walther[41]) depend on the variables in the function definitions being bound to constructor terms only. This dependence, however, and the intended meaning of the variables at all, are usually hidden in the formalism and not made as explicit as in enhaus&Becker[1] where it is shown that the restriction to constructor variables only, is beneficial to confluence (cf. also our Theorem 8.3) and termination of rewriting systems.

All in all, both kinds of variables have their benefits for specification with positive/negative-conditional equations and for expressing (inductive) properties with firstorder/Gentzen clauses, as well as for rewriting and (inductive) theorem proving. Since the technical treatment of both kinds of variables can be achieved by simple means, we have decided to include both of them in our constructor-based approach for positive/negativeconditional equations here. Together with our generalization to positive- and negativeconditional equations, the addition of constructor variables to classic term rewriting provides us with a unifying approach to the function specification style of classic inductive theorem proving on the one hand and to term rewriting on the other.

Comparison with Constructor based Models

Let us compare our semantics with that the models of Boyer&Moore[12] (forgetting about the type restriction axioms and thinking the language to be many-sorted instead) and INKA[10]. Those models are specified up to isomorphism by three kinds of axioms:

1. Explicitly stated recursive function definitions

2. Implicitly assumed first order axioms for expressing constructor-minimality. E.g.: ‘ ⟵s x = 0 ’, (which is ‘(NOT (EQUAL (ADD1 X) (ZERO))))’ in Boyer&Moore’s notation) and ‘ x = y⟵s x = s y ’ (where Boyer&Moore take ‘(EQUAL (SUB1 (ADD1 X)) X)’ instead).

3. Implicitly assumed second order generalized Peano axiom.

If we consider the recursive function definitions of (1) as (moderate) positive/negativeconditional rules and find an ordering that is compatible with these rules (which is an open problem (cf. then all critical peaks are

22Walther[42], Biundo[10], Boyer&Moore[12], Zhang[48], Wirth[43].

23E.g., one certainly should be able to express a commutativity lemma for addition of rational numbers, but one cannot expect it hold for ‘1/0’ or other undefined terms.

4 More Basic Notions and Notations

4.1 Substitutions

The set of substitutions from a variable-system X = (X_{ς,s})_{(ς,s)∈{SIG,CONS}×𝕊} to a {SIG, CONS}×𝕊-sorted family of sets T = (T_{ς,s})_{(ς,s)∈{SIG,CONS}×𝕊} is defined to be

SUB(X, T) := { σ : X → T | ∀(ς, s) ∈ {SIG, CONS}×𝕊 : ∀x ∈ X_{ς,s} : σ(x) ∈ T_{ς,s} } .

The most important sets of substitutions are SUB(V, T ) and SUB(V, GT ).

For the application of the homomorphic extension of a substitution σ ∈ SUB(V, T ) to a term t ∈ T we use postfix-notation: tσ . Notice that for σ ∈ SUB(V, GT ) : V(tσ) = ∅ 24.

Our definition of substitutions is consistent with the notion of order-sorted substitutions if one prefers the order-sorted view^{25} on our approach. A fortiori we get ∀σ ∈ SUB(V, T ) : ∀(ς, s) ∈ {SIG, CONS}×𝕊 : ∀t ∈ T_{ς,s}: tσ ∈ T_{ς,s} .

We use separations instead of the usual phrase “we always assume … to have no variables in common”. The set of separations for X, Y is defined for X, Y ⊆ V by:

Sep(X, Y) := { ξ ∈ SUB(V, V) | ξ bijective on V ∧ ξ[X] ∩ Y = ∅ }

For finite X, Y we always have Sep(X, Y) ≠ ∅ ^{26} and w.l.o.g.^{27} we think ‘min Sep(X, Y)’ to denote some element chosen from Sep(X, Y), because for our purposes all its elements are equivalent.

The set of most general unifiers for E on X is defined for E ∈ FMul(DEq(sig, V_{SIG}⊎V_{CONS})) and X ∈ 𝔓_{N}(V) by:

Mgu(E, X) := \{ \begin{matrix}σ ∈ SUB(V, T ) | set[E]σ ⊆ id ∧ ^{28} \\ ∀μ ∈ SUB(V, T ) : (set[E]μ ⊆ id ⇒ ∃τ ∈ SUB(V, T ) : (στ)X = μX) \} \end{matrix}

For unifiable E, i.e. for ∃μ ∈ SUB(V, T ) : set[E]μ ⊆ id , we always have Mgu(E, X) ≠ ∅ and w.l.o.g. we think ‘min Mgu(E, X)’ to denote some element chosen from Mgu(E, X), because for our purposes all its elements are equivalent. A unification algorithm can be found in appendix B.

24This is an application of the abuse of notation for families mentioned in Section 2.2. A proper notation would be V(tσ) = (∅)_{(s,ς)∈{SIG,CONS}×𝕊}

25As indicated above and described in [1].

26since ∀(ς, s) ∈ {SIG, CONS}×𝕊 : |V_{ς,s}| ∉ N

27without loss of generality

28We could enlarge the conjunction by σσ = σ but not^{29} by V(σ[V(E)]) ⊆ V(E) , for which we have to choose either V_{SIG} (as in [43, 45]) or V_{CONS} (as in [1]) but cannot allow all variables of V_{SIG}⊎V_{CONS} in our terms.

29To see this, consider x, y ∈ V_{CONS,nat} ; Y ∈ V_{SIG,nat} ; a most general unifier for ⟨(x, s Y)⟩ must be something like { x ↦ s y, Y ↦ y } .

4.2 Algebras

We define a sig/cons-algebra A over the signature sig = (𝔽, 𝕊, α) with constructor subsignature cons = (ℂ , 𝕊, αℂ) to be a function A : (𝔽 ⊎ ({SIG, CONS}×𝕊)) → V with ∀s ∈ 𝕊 : (∅ ≠ A(CONS, s) ⊆ A(SIG, s)) and

f^{A} : A(SIG, s_{0}) ×⋯×A(SIG, s_{n−1}) → A (SIG, s_{n}) for f ∈ 𝔽 with α(f)= s_{0} … s_{n−1}s_{n},
c^{A}[A(CONS, s_{0})×⋯×A(CONS, s_{n−1})] ⊆ A (CONS, s_{n}) for c ∈ ℂ with α(c) = s_{0} … s_{n−1}s_{n}.

We write f^{A} instead of A(f) for f ∈ 𝔽 . A(ς, s) is called the universe of A for (ς, s) ∈ {SIG, CONS}×𝕊.

The sig/cons-algebras of this definition are nothing but the order-sorted algebras over the order-sorted signature exhibited in Section 2.2.

A sig/cons-algebra A is called trivial if ∀(ς, s) ∈ {SIG, CONS}×𝕊 : |A(ς, s)| = 1 . The differences between two trivial sig/cons-algebras not being too interesting we speak of the trivial sig/cons-algebra if we mean any.

A (total) sig/cons-homomorphism h::A→B from a sig/cons-algebra A to a sig/cons-algebra B is an 𝕊-sorted family h = (h_{s})_{s∈𝕊} of functions h_{s} : A(SIG, s) → B(SIG, s) which are compatible with sig and cons: For f ∈ 𝔽 ; α(f) = s_{0} … s_{n−1}s_{n} ; ∀i < n : a_{i} ∈ A(SIG, s_{i}) :

h_{s_{n}}(f^{A}(a_{0}, …, a_{n−1})) = f^{B}(h_{s_{0}}(a_{0}), …, h_{s_{n−1}}(a_{n−1}))

and for all s ∈ 𝕊: h_{s}[A(CONS, s)] ⊆ B(CONS, s)

Taking the class of sig/cons-algebras for the class of objects and the class of sig/conshomomorphisms for the class of arrows, we get the sig/cons-homomorphism category of sig/cons-algebras. The composition hk::A→C of h::A→B and k::B→C is defined as usual by hk := (h_{s}∘k_{s})_{s∈𝕊} and the identity homomorphism for A is given as (idA(SIG, s))_{s∈𝕊}::A→A .

Let X⊆V.W euseT (X) todenotethetermalgebraoverXandsig/cons/V.T histermalgebrahasT_{ς,s}∩T (sig, X) as the universe for each (ς, s) ∈ {SIG, CONS}×𝕊 and works on function symbols as follows:

f^{T (X)}(t_{0}, …, t_{n−1}) = ft_{0} … t_{n−1}  for f ∈ 𝔽 with α(f) = s_{0} … s_{n−1}s_{n} and ∀i < n : t_{i} ∈ T (sig, X)_{s_{i}}

Similarly, (by abuse of notation) we sometimes use GT for the ground term algebra T (∅) over sig/cons instead of the family of ground terms. An A-valuation κ of X is an element of SUB(X, A) := SUB((V_{ς,s} ∩ X)_{(ς,s)∈{SIG,CONS}×𝕊}, (A(ς, s))_{(ς,s)∈{SIG,CONS}×𝕊}) ^{30}. The evaluation homomorphism A_{κ}::T (X)→A is recursively defined as follows (𝕊-index of A_{κ} omitted):

A_{κ}(x) = κ(x)  for x ∈ X
A_{κ}(ft_{0} … t_{n−1}) = f^{A}(A_{κ}(t_{0}), …, A_{κ}(t_{n−1})) for f ∈ 𝔽; t_{0}, …, t_{n−1} ∈ T (sig, X)

For getting acquainted with this notation, here is a well-known lemma: [Substitution-Lemma] Let A be a sig/cons-algebra and κ an A-valuation of X. For t∈ T andσ ∈ SUB(V, T (X)) :

A_{κ}(tσ) = A_{σ∘A_{κ}}(t)

30One would not call κ a substitution, however, unless A is a term algebra.

For ς  ∈  {SIG, CONS}; sc ∈ {sig, cons}; asig/cons − algebra A iscalled

ς:sc-term-generated if ∀s ∈ 𝕊 : ∀a ∈ A(ς, s) : ∃t ∈ GT (sc)_{s} : A(t) = a . It is called sc-term-generated if it is SIG:sc-term-generated.

A sig/cons-congruence ∼ on A is very similar to a sig-congruence in the multi-sorted case, namely an 𝕊-sorted family ∼ = (∼_{s})_{s∈𝕊} of equivalences ∼_{s} on A(SIG, s) being compatible with sig, i.e. satisfying for f ∈ 𝔽 ; α(f) = s_{0} … s_{n}s_{n+1} ; ∀i ≤ n : a_{i} ∈ A(SIG, s_{i}) : If a_{j} ∼_{s_{j}} b for some j≤ n, then f^{A}(a_{0}, …, a_{n}) ∼_{s_{n+1}} f^{A}(a_{0}, …, a_{j−1}, b, a_{j+1}, …, a_{n}) .

The factor algebra of A modulo ∼ is the sig/cons-algebra B (denoted by A/∼) given by:

B(ς, s) := { ∼_{s}[{a}] | a ∈ A(ς, s) } ( (ς, s) ∈ {SIG, CONS}×𝕊 )

f^{B}(∼_{s_{0}}[{a_{0}}], …, ∼_{s_{n−1}}[{a_{n−1}}]) := ∼_{s_{n}}[{f^{A}(a_{0}, …, a_{n−1})}]
(f ∈ 𝔽; α(f) = s_{0} … s_{n−1}s_{n}; ∀i < n : a_{i} ∈ A(SIG, s_{i}))

The canonical^{31} sig/cons-epimorphism of A modulo ∼ is the sig/cons-homomorphism k::A→A/∼ given by (s ∈ 𝕊; a ∈ A(SIG, s)): k_{s}(a) := ∼_{s}[{a}].

For a sig/cons-homomorphism h::A→B we define its kernel to be the sig/cons-congruence ker(h) given by (s ∈ 𝕊; a, b ∈ A(SIG, s)): (a, b) ∈ ker(h)_{s} if h_{s}(a) = h_{s}(b).

The following trivial result is called a “theorem” due to its widespread area of application:[Homomorphism-Theorem] Let h::A→C be a sig/cons-homomorphism. Let ∼ be a sig/cons-congruence on A with ∀s ∈ 𝕊: ∼_{s} ⊆ ker(h)_{s} . Define B := A/∼. Let k be the canonical sig/cons-epimorphism of A modulo ∼. Now h = kl uniquely defines an 𝕊-sorted family of functions l = (l_{s})_{s∈𝕊} with l_{s} : B(SIG, s) → C(SIG, s) for s ∈ 𝕊. Furthermore, this l is a sig/cons-homomorphism l::B→C. Moreover, if ∼ = ker(h) holds, then l_{s} is injective for each s ∈ 𝕊, i.e. l::B→C is monic in the sig/cons-homomorphism category of sig/cons-algebras.

By specialization of notions of category theory to full sub-categories of the sig/cons-homo-morphism category of sig/cons-algebras and to the forgetful functor we define for a class K of sig/cons-algebras; a sig/cons-algebra A; X⊆V; and κ ∈ SUB(X, A) : A isinitialinK if A ∈ K andforallB ∈ Kthereisauniqueh::A→B. A isfreeforKoverXw.r.t. κ if ∀B ∈ K : ∀μ ∈ SUB(X, B) : ∃!h::A→B : μ = κh . A is free in K over X w.r.t. κ if A ∈ K and A is free for K over X w.r.t. κ.

4.3 Orderings and other (binary) Relations

By an irreflexive ordering < we mean an irreflexive and transitive relation, sometimes called “strict partial ordering” by other authors. As with all our asymmetric relation symbols: a > b if b < a. Speaking of an ordering we always think of an irreflexive ordering. A relation R is A-reflexive if idA ⊆ R . Simply speaking of a reflexive relation we mean the biggest A that is appropriate in the local context. A quasi-ordering ≲ on A is an A-reflexive and transitive relation. An equivalence on A is an A-reflexive, symmetric, and transitive relation. The equivalence ≈ (on A) of a quasi-ordering ≲ (on A) is ≲ ∩ ≳. The ordering < of a quasi-ordering ≲ is ≲ \ ≳. A reflexive ordering ≤ on A is an A-reflexive, antisymmetric, and transitive relation. The ordering < of a reflexive ordering ≤ is ≤ \id. The A-reflexive ordering ≤ of an ordering < is <∪ idA.

31also called natural instead

Let X⊆V. A relation R on T is called:

X-stable^{32} (w.r.t. substitution) if ∀(t, t′) ∈R: ∀σ ∈ SUB(V, T (X)): (tσ, t′σ) ∈ R

T (sig, X)-monotonic (w.r.t. replacement) if ∀(t′, t′′) ∈ R : ∀t ∈ T (sig, X) : ∀p ∈ t : ∀s ∈ 𝕊 :

(t/p, t′, t′′ ∈ T_{SIG,s} ⇒ (t[ p ← t′], t[ p ← t′′]) ∈ R)

sort-invariant if ∀(t, t′) ∈ R : ∃s ∈ 𝕊 : t, t′ ∈ T_{SIG,s}

sufficiently complete (w.r.t. GT (cons)) if ∀t∈GT (sig): ∃t′ ∈GT (cons): (t, t′)∈R

A relation R is called:

total on A if A × A ⊆ (idA ∪ R ∪ R^{−1})
noetherian if there is no a : N → field(R) with ∀i ∈ N : (a_{i}, a_{i+1}) ∈ R
normalizing if ∀t : ∃t′ : ((t, t′) ∈ R ∧ t′ ∉ dom(R))

An ordering < or > is called well-founded if > is noetherian. A quasi-ordering or a reflexive ordering is called well-founded if its ordering is well-founded.

A reduction ordering on T is a T -monotonic, V-stable, and well-founded ordering.

The (proper) subterm ordering ◁_{ST} on T is the V-stable and well-founded ordering defined by (t, t′ ∈ T ):

t⊴_{ST}t′ if ∃p ∈ t′ : t = t′/p

A simplification ordering on T is a reduction ordering on T containing ◁_{ST}.

For further information on orderings see [15].

4.4 ⟶, Confluence, and Church-Rosser-Property

The symmetric closure of a relation ⟶ will be denoted by ⟷. Two terms v, w are called joinable w.r.t. ⟶ if v ↓ w if v⟶^{∗} ∘ ⟵^{∗}w. A relation ⟶ is called confluent below u if ∀v, w : ((v⟵^{+}u⟶^{+}w) ⇒ (v ↓ w)) . A relation ⟶ is called locally confluent below u if ∀v, w : ((v⟵u⟶w) ⇒ (v ↓ w)) ; it is called [locally] confluent if it is [locally] confluent below all u. A relation ⟶ is said to have the Church-Rosser-property if ⟷^{∗} ⊆ ↓ .

A noetherian relation ⟶ is confluent iff it is locally confluent.

A relation ⟶ is confluent iff it has the Church-Rosser-property.

32Similarly a predicate P on T is X-stable if ∀t ∈P: ∀σ ∈ SUB(V, T (X)): tσ ∈ P

5 Syntax and Semantics of Specifications

[Syntax of CRS] A (positive/negative-)conditional rule system (CRS) R over sig/cons/V is a finite subset of the set of rules over sig/cons/V, which will be defined in Definition 6. The only thing we have to know about it now is: ⊆ DEq(sig, V_{SIG}⊎V_{CONS}) × (CONDLIT (sig, V))^{∗} , where DEq(sig, V_{SIG}⊎V_{CONS}) is the set of directed equations and CONDLIT (sig, V) is the set of condition literals over the following predicate symbols on terms from T (sig, V_{SIG}⊎V_{CONS}): ‘=’, ‘≠’ (binary, symmetric, sort-invariant), and ‘Def’ (unary). A rule ((l, r), ∅) with an empty condition will be written l=r. A rule ((l, r), C) with condition C will be written l=r⟵C. We call l the left-hand side and r the right-hand side of the rule ((l, r), C); the terms^{33} of the condition literals in C are called condition terms and their set is denoted by TERMS(C). The set of all left-hand sides of rules in R is denoted by lhs(R). R is left-linear if all elements of lhs(R) are linear terms. A rule ((l, r), C) is said to be extra-variable free if V(r, TERMS(C)) ⊆ V(l). R is extra-variable free if all its rules ((l, r), C) ∈ R are extra-variable free.

A rule l=r⟵C expresses a universally quantified implication with the conjunction of the literals in C as the condition and with ‘l=r’ as the conclusion^{34}. The meaning of the predicate symbols ‘=’ and ‘≠’ is not open to interpretation. The fixed meaning of ‘=’ is standard; ‘≠’ is its negation. ‘Def ’, however, is the “definedness” predicate which states that the evaluation of its argument belongs (with sort invariant) to the constructor subuniverse of A which contains the set of evaluation values of constructor ground terms and which is intended to supply a domain for (possibly partially) specifying functions on it. We speak of our new kind of model just as a “sig/cons-model” (without any further attributes), because if we removed the new predicate symbol ‘Def ’ and the constructor sub-universes, we would just get the usual model concept of algebra; i.e., our sig/cons-model is an upwardcompatible extension.

[Semantics of CRS] Let R be a CRS over sig/cons/V; let A be a sig/cons-algebra. Now A is a sig/cons-model of R if

∀((l, r), C) ∈ R : ∀κ ∈ SUB(V, A) : ((C is true w.r.t. A_{κ}) ⇒ A_{κ}(l) = A_{κ}(r)) ,

where C is true w.r.t. A_{κ} if

∀s ∈ 𝕊: ∀u, v ∈ T_{SIG,s} : (\begin{matrix}(( (u=v ) in C) ⇒ & A_{κ}(u) = A_{κ}(v) ) & ∧ \\ (( (u≠v ) in C) ⇒ & A_{κ}(u) ≠ A_{κ}(v) ) & ∧ \\ (( (Def u) in C) ⇒ & A_{κ}(u) ∈ A(CONS, s) ) \end{matrix})

33To avoid misunderstanding: For a condition, say “ s=t, u≠v, Def w ”, we mean the top level terms s, t, u, v, w ∈ T (sig, V_{SIG}⊎V_{CONS}) , but neither their proper subterms nor the literals “s=t”, “u≠v”, “Def w”

themselves.

34Notice that we don’t make any use of the fact that we have (l, r) ∈ DEq(sig, V_{SIG}⊎V_{CONS}) beyond ⟨l, r⟩ ∈ Eq(sig, V_{SIG}⊎V_{CONS}) here; this ordering-property will be used for reduction only.

As we have negative equations in our conditions, we cannot hope to get a minimum model because we can express things like ‘ a=b ∨ b=c ’, which has the incomparable minimal models ‘a=b≠c’ and ‘a≠b=c’. What we will get instead is a model that is the (up to isomorphism) uniquely determined minimum of all sig-term-generated models that are minimal w.r.t. the identification of constructor ground terms (cf. Corollary 6). For formally expressing these minimality-properties, we need the following definition.

1. Define ≲_{H} and ≲_{CONS} as (proper class) relations on sig/cons-algebras by (A, B sig/cons-algebras): A ≲_{H}B if there is a sig/cons-homomorphism from A to B. A ≲_{CONS}B if there is a cons-homomorphism from the cons-algebra Aℂ ⊎ ({CONS}× 𝕊) to Bℂ ⊎ ({CONS}× 𝕊) .

We trivially get ≲_{H} ⊆ ≲_{CONS} (by restriction of the homomorphism); and ≲_{H}, ≲_{CONS} are quasi-orderings. The corresponding equivalences, orderings, and reflexive orderings will be denoted by ≈, <, ≤, resp., with the corresponding subscript.

2. A sig/cons-algebra A will be called a minimum model (or else a constructor-minimum model) of a CRS R over sig/cons/V if A is a ≲_{H}-minimum (or else ≲_{CONS}) of the class of all sig/cons-models of R. Similarly, a sig/cons-algebra A will be called a minimal model (or else a constructorminimal model) of a CRS R over sig/cons/V if A is a sig/cons-model of R and there is no sig/cons-model B of R with B <_{H}A (or else B <_{CONS}A ).

The following lemma tells us that, considering minimum models, we can think in terms of sig/cons-congruences on GT instead of algebras:

Let B be a sig/cons-model of the CRS R over sig/cons/V. Define the factor algebra A := GT /ker(B) . Now:

1. A is a sig/cons-model of R.

2. A ≲_{H}B . Moreover, there is a unique sig/cons-homomorphism l::A→B (, which is monic in the sig/cons-homomorphism category of sig/cons-algebras).

3. A ≲_{CONS}B .^{35}

The following lemma^{36} of theoretical nature ensures the existence of minimal models: Let R be a CRS over sig/cons/V.

1. The trivial sig/cons-algebra is a sig/cons-model of R.

2. If B is a sig/cons-model of R, then there is a minimal model A of R with A ≤_{H}B.

3. R has a minimal model.

35However, we do not have A ≈_{CONS}B in general, because Bℂ ⊎ ({CONS}× 𝕊) need not be cons-term-generated.

36The lemma resembles Theorem 2.1 in Kaplan[28]. Our ≲_{H} and ≲_{CONS}, however, are reflexive and therefore different from the relation ≤ in [28], where the homomorphism is additionally required to be unique.

6 The Reduction Relation

In this section we are going to define a reduction relation ⟶ which is convenient for the semantics defined in the previous section. The overall idea is to reduce a left-hand side of a rule to its right-hand side only if the condition of this rule can somehow be shown valid by means of the same reduction relation again.

Many authors impose rather strong restrictions on constructor equations, such as “no equations between constructors” (“free constructors”) or “unconditional equations between constructors only”. Compared to these, our restrictions are very weak. They serve to guarantee a constructor-minimum model for the constructor equations that is unique modulo ≈_{CONS}, by requiring the constructor equations to have “Horn”-form and to be “constructorpreserving”^{37}.

[Set of Rules] (continuing Definition 5 by adding the restrictions on constructor equations) The set of rules over sig/cons/V is defined to be: :=

{ ((l, r), C) ∈ (DEq(sig, V_{SIG}⊎V_{CONS}) × (CONDLIT (sig, V))^{∗})

( l ∈ T (cons, V_{SIG}⊎V_{CONS}) ⇒ ( \begin{matrix}∀L in C : ∀u, v : L ≠ (u≠v) & ∧ \\ V(r, TERMS(C)) ⊆ V(l) & ∧ \\ r ∈ T (cons, V_{SIG}⊎V_{CONS}) & ∧ \\ TERMS(C) ⊆ T (cons, V_{SIG}⊎V_{CONS}) \end{matrix} ))\}

We are now going to define our reduction relation, having in mind to require it to be confluent in the sequel, whereas we do not require confluence for the definition because we cannot prove confluence criteria if the non-confluent case is undefined. Therefore, we have to be explicit about how we test the condition literals — even if this testing is not straightforward when confluence is not provided. Our “operational” semantics for testing condition literals is the following: ‘u=v’ is true if u, v have reducts û, v̂, resp., which are syntactically equal. ‘Def u’ is true if u has a constructor ground reduct, which means that our reduction relation depends on the constructor sub-signature ‘cons’ beyond the signature ‘sig’ — just as our notion of “sig/cons-model” does. Finally, ‘u≠v’ is true if u, v have constructor ground reducts û, v̂, resp., which are not joinable. Thus, two terms in a condition literal are “operationally” equal if they are joinable, whereas they are unequal if they are not joinable after some reduction to constructor ground terms. The non-joinability alone of two terms is not sufficient for regarding them as unequal because we are never sure about the inequality of “undefined” terms (cf. Section 3). As it often occurs, our operational logic is four-valued, i.e. ‘=’ and ‘≠’ can independently be true or false. In case of confluence, however, it is impossible that both ‘u=v’ and ‘u≠v’ are simultaneously true; in case of free or confluent constructors, this would mean we have something like an ambiguous function definition.

37The constructor-preservation is really necessary here for guaranteeing the existence of a a minimal constructor-minimum model as in Theorem 6: Let 0, 1, true, false be constructor constants, let weirdp be a non-constructor constant, and take R: 1=0 ⟵ weirdp=true ; weirdp=true ⟵ true≠false .

Now there are sig/cons-models of R with 0≠1 and models with true≠false but no models with ‘ 0≠1 ∧ true≠false ’. Also notice, that the constructor-preservation has some additional advantages, e.g.:

1. The rules become sort-decreasing w.r.t. to the order-sorted signature exhibited in Section 2.2, i.e.

the right-hand side and the condition terms are from T (cons, V_{CONS}) if the left-hand side is.

2. For u ∈ GT with computable and unique normal form NF(u) we can test

“ ∃û ∈ GT (cons) : u⟶^{∗}û ” by “ NF(u) ∈ GT (cons) ”.

3. Theorem 6 has no reasonable analogue for CRSs which are not constructor-preserving.

[Our Reduction Relation ⟶] Let R be a CRS over sig/cons/V. Let X⊆V. The reduction relation ⟶_{R,X} on T (sig, X) (⟶ for short) is defined to be the smallest relation satisfying the fol. requirement (:#): s⟶t \underline{if} s, t ∈ T (sig, X) ∧

∃((l, r), C)∈R: ∃σ ∈SUB(V, T (X)): ∃p∈s:(\begin{matrix}s/p = lσ & ∧ \\ t = s[ p ← rσ] & ∧ \\ Cσ is fulfilled w.r.t. ⟶ \end{matrix}) ,

where (for D ∈ CONDLIT (sig, X)^{∗}) “ D is fulfilled w.r.t. ⟹” is a shorthand for

∀u, v ∈ T : ( \begin{matrix}( ( (u=v ) in D) ⇒ & u ↓ v ) & ∧ \\ ( ( (Def u) in D) ⇒ & ∃û ∈ GT (cons) : & u⟶^{∗}û ) & ∧ \\ ( ( (u≠v ) in D) ⇒ & ∃û, v̂ ∈ GT (cons) : & u⟶^{∗}û∤↓v̂⟵^{∗}v )^{38} \end{matrix} )

Usually one tries to find a minimal reduction relation by taking the closure over a finitary generating relation. This is not possible here, because we have a negative condition (∤↓). By the “Horn”-form of our constructor equations (and the constructor-preservation), however, we know that this negative condition does not influence the reduction of constructor terms; and (in the definition) ‘∤↓’ is applied to constructor (ground) terms only. Thus, we can get our minimal reduction relation by a double closure: first for constructor rules only; second for general rules knowing the constructor reduction to remain unchanged. This two step construction does not destroy the uniformity of the defining requirement(#), which allows to write uniform normal form procedures.

Define ⟶_{R,X,0} := ∅ and ⟶_{R,X,i+1} to be the left-hand side^{39} of the requirement(#) of Definition 6 with ⟶_{R,X,i} substituted for ⟶ on the right-hand side and the additional restriction of l ∈ T (cons, V_{SIG}⊎V_{CONS}) ; formally: s⟶_{R,X,i+1}t if s, t ∈ T (sig, X) ∧

∃((l, r), C)∈R: ∃σ ∈SUB(V, T (X)): ∃p∈s:(\begin{matrix}l ∈ T (cons, V_{SIG}⊎V_{CONS}) & ∧ \\ s/p = lσ & ∧ \\ t = s[ p ← rσ] & ∧ \\ Cσ is fulfilled w.r.t. ⟶_{R,X,i} \end{matrix}) .

Define ⟶_{R,X,ω} := ⋃_{i∈N} ⟶_{R,X,i} and ⟶_{R,X,ω+i+1} to be the union of ⟶_{R,X,ω} and the lefthand side^{39} of the requirement(#) of Definition 6 with ⟶_{R,X,ω+i} substituted for ⟶ on the right-hand side. Finally, define ⟶_{R,X,ω+ω} := ⋃_{i∈N} ⟶_{R,X,ω+i} . Now ⟶_{R,X,ω+ω} satisfies the requirement(#) of Definition 6, and every relation satisfying this requirement must contain ⟶_{R,X,ω+ω}. Hence ⟶_{R,X,ω+ω} is the intended smallest relation ⟶_{R,X}. A more detailed proof for all this can be found in appendix A. We drop “R, X” in ⟶_{R,X} and ⟶_{R,X,β} when referring to some fixed R and X. Let ≺ denote the ordering on the ordinal numbers. By induction over the above construction process it is trivial to verify the following corollaries.

38This formulation requires confluence and constructor-preservation to make sense in two-valued logic.

While other formulations (e.g. a universal instead of the existential quantification) might seem to be more satisfactory, this is the one required for a correct definition. One might have expected uv instead of ∃û, v̂ ∈ GT (cons) : u⟶^{∗}ûv̂⟵^{∗}v for “u≠v in D” here, but this modification would not allow the conclusion that ⟶ is uniquely defined as can be seen from:

Let c, d be constructor and a, b, e be non-constructor constants and take R: a=c ⟵ b≠d ; b=d ⟵ e≠c ; e=a . Now { (a, c), (e, a) } and { (b, d), (e, a) } would be ⊆-incomparable minimal relations satisfying the modified requirement(#) of Definition 6. Their intersection { (e, a) } , however, satisfies the nonmodified requirement only.

39the ‘ \underline{if} ’ replaced by ‘ if ’

[Monotonicity of ⟶ w.r.t. Replacement] ⟶_{R,X,β} (for β ⪯ ω+ω) and ⟶_{R,X} are T (sig, X)-monotonic. [Stability of ⟶] ⟶_{R,X,β} (for β ⪯ ω+ω), ⟶_{R,X}, and their respective fulfilledness-predicates are X-stable.

The fol. technical lemmas state constructor-preservation and that there is no need for a second closure for reduction of constructor terms. ∀n ∈ N: ∀s ∈ T (cons, V_{SIG}⊎V_{CONS}): ∀t: ( s⟶^{n}t ⇒ (s⟶^{n}_{ω}t ∈ T (cons, V_{SIG}⊎V_{CONS})) )

∀n ∈ N: ∀s ∈ T (cons, V_{CONS}): ∀t: (s⟶^{n}t ⇒ (s⟶^{n}_{ω}t ∈ T (cons, V_{CONS}))) ∀n ∈ N : ∀s ∈ GT (cons) : ∀t : ( s⟶^{n}t ⇒ (s⟶^{n}_{ω}t ∈ GT (cons)) ) ↓ ∩ ( T (cons, V_{SIG}⊎V_{CONS}) × T (cons, V_{SIG}⊎V_{CONS}) ) ⊆ ↓_{ω}

[Monotonicity of ⟶_{β} and of Fulfilledness w.r.t. ⟶_{β} in β] For β ⪯ γ ⪯ ω+ω: ⟶_{β} ⊆ ⟶_{γ} ⊆ ⟶ ; and if C is fulfilled w.r.t. ⟶_{β} and ω ⪯ β ∨ ∀u, v : ((u≠v) is not in C) , then C is fulfilled w.r.t. ⟶_{γ} and w.r.t. ⟶.

[Fulfilledness Test may be Simple] Let C ∈ (CONDLIT (sig, X))^{∗}. If for each element u ∈ TERMS(C):

1. u has a normal form NF(u) (i.e. u⟶^{∗}NF(u) ∉ dom(⟶) )

and

2. ⟶ is confluent below u,

then C is fulfilled w.r.t. ⟶ iff

∀u, v ∈T : (\begin{matrix}( ( (u=v ) in C) ⇒ & NF(u) = NF(v) ) & ∧ \\ ( ( (Def u) in C) ⇒ & NF(u) ∈ GT (cons) ) & ∧ \\ ( ( (u≠v ) in C) ⇒ & (NF(u), NF(v)∈GT (cons) ∧ NF(u)≠NF(v)) ) \end{matrix})

Let X⊆Y⊆V . Now: For all β ⪯ ω+ω : ∀n ∈ N_{+} : ⟶^{n}_{R,X,β} = ⟶^{n}_{R,Y,β} ∩ (T (sig, X)×T (sig, X)) ,

andforC ∈ CONDLIT (sig, X) :Cisfulfilledw.r.t. ⟶_{R,X,β} iff Cisfulfilledw.r.t. ⟶_{R,Y,β}.

F urthermore, dom(⟶_{R,X}) = dom(⟶_{R,Y}) ∩ T (sig, X) .

F inally, if⟶_{R,Y}isconfluent, then⟶_{R,X} isconfluent, too.

By Example 38 we know that (for guaranteeing a constructor-minimum model) we have to restrict the terms of the negated equations to be “defined”. This semantic restriction is made syntactically explicit in the fol. definition which specifies a “well-behaved” subclass of the class of CRSs, in which inequalities are founded on constructor objects. For a detailed motivation cf. item (A) in Section 3 (“Our Solution”).

[Def-Moderate Conditional Rule Systems (Def-MCRS)] A CRS R is a Def-moderate conditional rule system (Def-MCRS) if

∀((l, r), C) ∈ R : ∀(u≠v) in C : ( Def u, Def v are in C ) .

Now we are able to state the fundamental theorem about ⟶. Its corollary says that for Def-moderate CRSs R with confluent ⟶_{R,∅}, the factor algebra GT /⟷^{∗}_{R,∅} is an (up to isomorphism) uniquely determined sig/cons-model of R.

(Minimal Model being Free in the Constructor-Minimal Models) Let R be a Def-MCRS over sig/cons/V. Let X⊆V . Let K be the class of all constructorminimal^{40} models of R. Let κ be given by (x∈X): x ↦ ⟷^{∗}_{R,X}[{x}] . Now, if ⟶_{R,∅} is confluent^{41}, then T (X)/⟷^{∗}_{R,X} is free for K over X w.r.t. κ. Furthermore, if we assume ⟶_{R,X} to be confluent^{42} and X⊆V_{SIG} , then the fol. items hold:

1. T (X)/⟷^{∗}_{R,X} is a constructor-minimum^{40} model of R.

2. T (X)/⟷^{∗}_{R,X} is free in K over X w.r.t. κ.

3. T (X)/⟷^{∗}_{R,X} is a minimal^{40} model of R.

Let R be a Def-MCRS over sig/cons/V. Furthermore, assume ⟶_{R,∅} to be confluent. Now: GT /⟷^{∗}_{R,∅} is a minimal model of R, initial in the class of all constructor-minimal models of R, and the (up to isomorphism) unique ( ≲_{H}-) minimum of the sig-term-generated constructor-minimal models of R.

(Monotonicity of ⟶_{R,X} w.r.t. Consistent Extension of the Specification) Let R be a CRS over sig/cons/V. Let X⊆V. Let R′ be another CRS, but over sig′/cons′/V′;

and X’⊆V’ with sig′ = (𝔽′, 𝕊′, α′) cons′ = (ℂ′, 𝕊′, α′ℂ′) V′\{SIG, CONS\}×𝕊 = V \begin{matrix}𝔽 ⊆ & 𝔽′ \\ ℂ ⊆ & ℂ′ ⊆ 𝔽′ \\ 𝕊 ⊆ & 𝕊′ \\ α ⊆ & α′ \end{matrix} \begin{matrix}R ⊆ & R′ \\ X ⊆ & X′ \end{matrix}

Thus, sig′/cons′/V′ is an enrichment of sig/cons/V in the most general^{43} sense we can think of. Moreover, assume^{44}: ∀((l, r), C) ∈ (R′ \R) : l ∉ T (cons, V_{SIG}⊎V_{CONS}) (:$) Now we have^{45}:

1. ∀s∈T (cons, X): ∀t: ((s⟶^{∗}_{R,X}t) ⇔ (s⟶^{∗}_{R′,X′}t))

“no change on old constructor terms”

2. ⟶_{R,X} ⊆ ⟶_{R′,X′} “monotonicity”

3. ∀β ⪯ ω+ω : ⟶_{R,X,β} ⊆ ⟶_{R′,X′,β} “monotonicity”

40Cf. Definition 5

41The remark of footnote 42 with X := ∅ is applicable here.

42The fol. allows to apply the confluence criterion of Theorem 7: If we additionally require ∀((l, r), C) ∈ R : ∀(u=v) in C : ( Def u, Def v are in C ) , then we can weaken the confluence requirement to confluence of ⟶_{R,X} ∩ (D_{X}×D_{X}) for D_{X} := { u ∈ T (sig, X) | ∃û ∈ GT (cons) : u⟷^{∗}_{R,X} û } .

43One may even introduce new constructor symbols for the old sorts and take them from the old nonconstructor symbols. Since all V_{ς,s} are infinite, the restriction on V′ is not severe.

44This has to be required for keeping the negative conditions fulfilled: Having founded our inequalities on old constructor ground terms, all we have to take care of now is not to confuse these terms.

45While it is important that ⟶_{R,X} tests (u≠v) in a condition of an equation by ∃û, v̂ ∈ GT (\underline{\underline{cons}}) : u⟶^{∗}_{R,X} û_{R,X} v̂⟵^{∗}_{R,X}v instead of ∃û, v̂ ∈ GT (\underline{\underline{cons′}}) : u⟶^{∗}_{R,X} û_{R,X} v̂⟵^{∗}_{R,X}v , for the validity of the theorem it does not matter whether ⟶_{R,X} is defined on T (sig, X) or T (sig′, X′).

7 How to Test for Confluence

We are now going to define critical peaks that consist of the conditional critical pair, its peak, and the overlap position. The other notions we will use are standard, with the exception of “quasi overlay joinable” which is a slight weakening of “overlay joinable” in Dershowitz[16] (cf. below), in that it allows an identical non-overlay part in the critical pair.

[Critical Peaks and Joinability] The set of (non-trivial) critical peaks between two rules ((l_{k}, r_{k}), C_{k}) ∈ R ; k < 2 ; is defined as: Cp( ((l_{0}, r_{0}), C_{0}), ((l_{1}, r_{1}), C_{1}) ) :=

{ (((l_{1}[ p ← r_{0}ξ], r_{1}), C_{0}ξ C_{1})σ, l_{1}σ, p) |||||||| ξ = min Sep(V(((l_{0}, r_{0}), C_{0})), V(((l_{1}, r_{1}), C_{1})))  ∧ “no variables in common”

p ∈ l_{1} ∧ l_{1}/p ∉ V ∧ “non-variable position”
σ = min Mgu(⟨(l_{0}ξ, l_{1}/p)⟩, V(((l_{0}, r_{0}), C_{0})ξ, ((l_{1}, r_{1}), C_{1}))) ∧  “most general unifier”
l_{1}[ p ← r_{0}ξ]σ ≠ r_{1}σ  “non-trivial critical pair”

} And the set of all critical peaks of R is CP(R) := ⋃_{rule_{0}∈R} ⋃_{rule_{1}∈R} Cp(rule_{0}, rule_{1}) .

R is said to be overlapping if CP(R) ≠ ∅ . A critical peak (((t_{0}, t_{1}), D), t̂, p) is joinable w.r.t. R, X if

∀φ ∈ SUB(V, T (X)) : ((Dφ fulfilled w.r.t. ⟶_{R,X}) ⇒ t_{0}φ↓_{R,X}t_{1}φ) .

A critical peak (((t_{0}, t_{1}), D), t̂, p) is overlay joinable w.r.t. R, X if it is joinable w.r.t. R, X and p=∅. It is quasi overlay joinable w.r.t. R, X if

∀φ ∈ SUB(V, T (X)): ( ( \begin{matrix}Dφ fulfilled \\ w.r.t. & ⟶_{R,X} \end{matrix} ) ⇒ \binom{t_{1}φ = t_{0}φ[ p ← t_{1}φ/p] ∧}{(t_{0}/p)φ↓_{R,X}t_{1}φ/p⟵^{+}_{R,X}(t̂/p)φ} ) .

[Joinability of Critical Peaks is Necessary for Confluence] Let R be a CRS over sig/cons/V and X⊆V. If ⟶_{R,X} is confluent, then all critical peaks in CP(R) are joinable w.r.t. R, X.

[ Overlay Joinable ⇒ Quasi Overlay Joinable ⇒ Joinable ] Let R be a CRS over sig/cons/V; X⊆V; and (((t_{0}, t_{1}), D), t̂, p) ∈ CP(R). Now w.r.t. R, X the following holds:

1. If (((t_{0}, t_{1}), D), t̂, p) is overlay joinable, then it is quasi overlay joinable.

2. If (((t_{0}, t_{1}), D), t̂, p) is quasi overlay joinable, then it is joinable.

Sufficient criteria for confluence of reduction relations for merely positive conditional rule systems are studied in Dershowitz[16]. As counterexamples for suggested sufficient confluence criteria for merely positive conditional rule systems are counterexamples for Def-MCRSs too, we repeat the results of [16] here: There are (left-linear) non-overlapping positive-conditional rule systems whose reduction relations are not (locally) confluent^{46} (but necessarily non-noetherian then^{47}). Therefore, syntactic confluence criteria for nonnoetherian conditional rule systems must be very difficult to develop. Semantic confluence criteria (in the style of Plaisted[38]) seem to require noetherian (or at least normalizing) reduction relations because they rely on the irreducible reducts of the terms; furthermore irreducibility is not (semi-) decidable. Thus, for our confluence criteria we require ⟶ to be noetherian. Even then the situation is not very encouraging, because there are noetherian and non-confluent reduction relations of (left-linear, normal, and) positive-conditional rule systems with joinable critical peaks only.^{48} Moreover, semantic confluence criteria remain difficult because irreducibility is still not (semi-) decidable. However, for merely positive conditional rule systems there are two known syntactic solutions of major^{49} interest: One requires either more than joinability for the critical peaks (as, e.g., in Theorem 4 in [16]) or the condition terms to be somehow smaller than the left-hand side of the rule (as, e.g., in Theorem 3 in [16]). We will study the latter approach (which is the more important one in practice (cf. Example 7)) later^{50}. The following result is a generalization of Theorem 4 in Dershowitz[16] from positive-conditional to positive/negative-conditional rule systems and, moreover, from overlay joinability to quasi overlay joinability.

46Cf. [16], Example A, p. 36

47Cf. [16], Theorem 4, p. 39

[Syntactic Confluence Criterion] Let R be a CRS over sig/cons/V and X⊆V. If ⟶_{R,X} is noetherian and all critical peaks in CP(R) are quasi overlay joinable w.r.t. R, X, then ⟶_{R,X} is confluent.

While this theorem is very nice (theoretically) and has a pretty complicated proof, it may be difficult to apply even for merely positive conditional equations:

Let R: f s x = 0 ⟵ f x = 0 ; f s x = 1 ⟵ f x = 1 ; f … Assume 0 and 1 to be irreducible. Now for showing the critical peak between the first two rules to be quasi overlay joinable, one has to show that it is impossible that both conditions hold simultaneously for a substitution {x↦t}. However, in order to prove this, we need the confluence below ‘ f t’, which we are not allowed to assume for the joinability test here.

[Semantic Confluence Criterion] Let R be a CRS over sig/cons/V and X⊆V. Let A be a sig/cons-model of R and κ an A-valuation of X. Now:

1. If ∀s ∈ 𝕊 : ∀û, v̂ ∈ T (sig, X)_{s}\dom(⟶_{R,X}) : ( A_{κ}(û) = A_{κ}(v̂) ⇒ û = v̂ ) and ⟶_{R,X} is noetherian, then ⟶_{R,X} is confluent.

2. Define^{51} D_{X} := { u ∈ T (sig, X) | ∃û ∈ GT (cons) : u⟷^{∗}_{R,X} û } . If

∀s ∈ 𝕊 : ∀û ∈ GT (cons)_{s}\dom(⟶_{R,X}) : ∀v̂ ∈ T (sig, X)_{s}\dom(⟶_{R,X}) :

( A_{κ}(û) = A_{κ}(v̂) ⇒ û = v̂ )

and ⟶_{R,X} ∩ (D_{X}×D_{X}) is noetherian, then ⟶_{R,X} ∩ (D_{X}×D_{X}) is confluent.

48Cf. [16], Example B, p. 36

49We are not interested in the shallow-joinability of Dershowitz[16] here because there is a noetherian, shallow-joinable, left-linear, but not confluent, merely positive conditional rule system (cf. [16], Example C, p. 36) as well as a noetherian, shallow-joinable, normal, but not confluent, merely positive conditional rule system (cf. [16], Example D, p. 36), which means that shallow-joinability is only sufficient for confluence of rule systems which are both left-linear and normal. The combination of left-linearity and normality, however, is a too severe restriction to be of major interest for us here, because left-linearity forbids the positive part of the specification of an equality predicate by eq x x = ⊥ , which is the common trick for achieving normality by transformation of ‘v=v’ in a condition of a rule into ‘eq v u = ⊥’.

50Cf. theorems 8.3 and 8.3

51Cf. footnote 42

8 Compatible CRSs

Compatibility restrictions on rule systems w.r.t. well-founded orderings enhance our means of deciding reducibility and confluence. Such restrictions are necessary, as can be seen from:

[Reducibility of Ground Terms is Not Co-semi-decidable] There is a left-linear, non-overlapping, extra-variable free, merely positive conditional rule system R with noetherian and confluent reduction relation ⟶_{R,V} for which reducibility of ground terms is not co-semi-decidable.

[Reducibility of Ground Terms is Not Semi-decidable] There is a left-linear, non-overlapping, extra-variable free, Def-moderate CRS R with noetherian and confluent reduction relation ⟶_{R,V} for which reducibility of ground terms is not semi-decidable.

The fol. theorem is a generalization of Theorem 3.4 in Kaplan[27] in various directions. Let R be a CRS over sig/cons/V. Let X be an enumerable subset of V.

1. ⟶_{R,X}-reducibility of terms from T (sig, X) is co-semi-decidable if a ⟶_{R,X}-normal form for each term from T (sig, X) is computable (i.e. there is a computable (partial) function f with dom(f) = { s∈T (sig, X) | ∃t : (s⟶^{∗}_{R,X}t ∉ dom(⟶_{R,X})) } such that ∀s ∈ dom(f) : s⟶^{∗}_{R,X}f(s) ∉ dom(⟶_{R,X}) ).

2. A ⟶_{R,X}-normal form for each term from T (sig, X) is computable (cf. above) if ⟶_{R,X}- reducibility of terms from T (sig, X) is co-semi-decidable and ∀s ∈ GT (cons) : ∃t : s⟶^{∗}_{R,X}t ∉ dom(⟶_{R,X}) .

Let R be a CRS over sig/cons/V. Let X be an enumerable subset of V. Assume ⟶_{R,X} to be noetherian. Now, co-semi-decidability of ⟶_{R,X}-reducibility of terms from T (sig, X) is logically equivalent to computability of a ⟶_{R,X}-normal form for each term from T (sig, X).

8.1 The Use of Orderings

In this and the fol. section we just want to give minimal reasonable compatibility requirements for achieving additional decidability properties of our reduction relation. We start with a discussion of how to use orderings for reduction with conditional rules. This discussion mainly depends on the method of testing the conditions uniformly by the same reduction relation again, where well-founded orderings are needed for guaranteeing termination of condition-testing and reduction. Since this method does not depend on the concrete form of our rules, the situation under discussion does not differ from the case of merely positive conditional equations.

Let > be a well-founded ordering intended to contain the reduction relation ⟶_{R,X}. We require it to be sort-invariant, T -monotonic, and V-stable; which does not restrict applicability because the transitive, T -monotonic, and V-stable closure of ⟶_{R,X} is a sortinvariant, T -monotonic, and V-stable ordering itself, provided that ⟶_{R,X} is well-founded. Let ↪ be the relation intended to contain the step from a left-hand side’s superterm to the condition terms. Since a condition term, which can be tested for an attempt to reduce l, should also be testable for reduction of t[ p ← l] (otherwise ⟶^{+}_{R,X} wouldn’t be T (sig, X)- monotonic), we require the property ∘ ↪ ⊆ ↪ , — considering t[ p ← l]l ↪ u ⇒ t[ p ← l] ↪ u . As we test our conditions by reduction we must be allowed to switch from reduction to condition-testing, and then to reduction of the condition terms, and so on; hence we require the transitive closure ⇝ := (> ∪ ↪)^{⊕} of > and ↪ to be noetherian. For going on we need the following two lemmas: Let > be a T -monotonic ordering on T . Define ≻ := (> ∪▷_{ST})^{⊕} . Now the following holds:

1. If > is sort-invariant^{52} [, V-stable,] and well-founded, then ≻ is a well-founded [and V-stable] ordering, which doesn’t need to be sort-invariant or GT -monotonic.

2. (8.1) does not hold in general if > is not sort-invariant or not T -monotonic.

3. ▷_{ST}∘ > ⊆ > ∘▷_{ST}

4. ≻ = ▷_{ST} ∪ (> ∘⊵_{ST})

Let^{53} ▷_{ST}∘ > ⊆ > ∘▷_{ST} . Let^{54} ▷_{ST}∘ ↪ ⊆ ↪ . Define ⇝ := (> ∪ ↪)^{⊕} and assume it to be noetherian.^{55} Assume^{56} (> ∪▷_{ST})^{⊕} to be noetherian. [Assume ↪ and > to be X-stable.] Now: ▷ := (> ∪▷_{ST}∪ ↪)^{⊕} is noetherian [and X-stable], too.

Define s↠_{R,X}t if s∈ T (sig, X) ∧ ∃((l, r), C)∈R: ∃σ ∈SUB(V, T (X)): ∃p∈s:

( s/p=lσ ∧ ∃u ∈ TERMS(C) : t = uσ ∧ (Cσ is fulfilled w.r.t. ⟶_{R,X}) ) As we test our conditions by reduction we must be allowed to switch from reduction to condition-testing, and then to reduction of the condition terms, and so on. Hence we require (⟶_{R,X} ∪ ↠_{R,X}) to be noetherian. By the fol. lemma, this requirement can be expressed by means of relations ⇉, ↪ on T as follows: ⟶_{R,X} ⊆ ⇉ ; ↠_{R,X} ⊆ ↪ ; ⇉ is sort-invariant, T -monotonic, and V-stable; ↪ is V-stable; and (⇉ ∪ (⊵_{ST}∘ ↪)) is noetherian.

52The easiest way to achieve sort-invariance is to identify all sorts

53This matches Lemma 8.1(8.1).

54This was required for ↪ in our discussion above.

55This was required in our discussion above.

56This matches the conclusion of Lemma 8.1(8.1), (using Lemma 8.1(8.1)).

If (⟶_{R,X} ∪ ↠_{R,X}) is noetherian, then (⟶_{R,V} ∪ (⊵_{ST} ∘ ↠_{R,V})) is noetherian, too.

The fol. two lemmas show that w.l.o.g. we can require even (⇉ ∪▷_{ST}∪ ↪) to be noetherian:

Let ⇉ be a sort-invariant^{57} and T -monotonic relation on T . Define ≻:= (⇉ ∪▷_{ST})^{⊕}.Nowthefollowingholds : If ⇉ is noetherian [and V-stable], then ≻ is a well-founded [and V-stable] ordering, which doesn’t need to be sort-invariant or GT -monotonic.

(8.1) does not hold in general if ⇉ is not sort-invariant or not T -monotonic.

▷_{ST}∘ ⇉ ⊆ ⇉ ∘▷_{ST}

≻ = ▷_{ST} ∪ (⇉^{⊕} ∘⊵_{ST})

Let^{58} ▷_{ST}∘ ⇉ ⊆ ⇉ ∘▷_{ST} . Assume (⇉ ∪ (⊵_{ST}∘ ↪)) to be noetherian.^{59} Assume^{60} (⇉ ∪▷_{ST}) to be noetherian. [Assume ⇉ and ↪ to be V-stable.] Now: ▷ := (⇉ ∪ ↪ ∪▷_{ST})^{⊕} is a well-founded [and V-stable] ordering.

By these two lemmas we see the following: Instead of taking (in addition to >) two relations ↪ and ⇝ with the above requirements^{61}, we can take a single relation ▷ (without giving up the required well-foundedness) and require the stronger ▷_{ST} ⊆ ▷ instead of the weaker ▷_{ST}∘ ↪ ⊆ ↪ .

Finally, writing ‘>’ for ‘⇉^{⊕}’, this justifies the following definition:

[Termination-Pair] A termination-pair over sig/V is a pair (>, ▷) for which the following properties hold:

1. >, ▷ ⊆ T ×T

2. > is a T -monotonic and V-stable^{62} ordering^{63}.

3. ▷ is a V-stable^{62} and well-founded ordering.

4. > ⊆ ▷

5. ▷_{ST} ⊆ ▷ ^{64}

57The easiest way to achieve sort-invariance is to identify all sorts

58This matches Lemma 8.1(8.1).

59This matches the conclusion of Lemma 8.1.

60This matches the conclusion of Lemma 8.1(8.1).

61i.e. > sort-invariant, T (sig, X)-monotonic, well-founded [, and X-stable] ordering. ▷_{ST}∘ ↪ ⊆ ↪ . [↪ X-stable.] ⇝:= (> ∪ ↪)^{⊕} noetherian.

62V-stability is included because it can always be achieved (for ⇉ and ↪; and thereby for > and ▷, too)

by restriction to ground terms — and the non-ground part of an ordering ▷ whose V-stable closure is not noetherian anymore is of no use for showing termination anyway because then its ∅-stable closure is not noetherian, either.

63As discussed above, sort-invariance can be required here; but it is of no use for us and omitted for convenience. For the benefit from this cf. Example 3(3).

64Notice that for proving alignment (cf. Definition 3 below) in practice we only have to show ▷_{ST} ∘▷ ⊆ ▷ and then take (▷_{ST} ∪▷)^{⊕} instead of ▷, because then we know by Lemma 8.1 (applied to the sort-invariant restriction of >), and then by Lemma 3, that (▷_{ST} ∪ ▷)^{⊕} will do the job of ▷.

The standard examples for a termination-pair (>, ▷) are:

1. > some sort-invariant reduction ordering; ▷ := ▷_{ST} ∪ (> ∘⊵_{ST}). ^{65}

2. ▷ some V-stable and well-founded ordering containing ▷_{ST}; > :=

⋃_{s∈𝕊}{ (t′, t′′) | t′, t′′∈T_{SIG,s} ∧ ∀t∈T: ∀p∈t: (t/p∈T_{SIG,s} ⇒ t[ p ← t′]▷ t[ p ← t′′]) }.^{66}

3. > some simplification ordering; ▷ := >.

In the field of ordering restrictions for conditional rule systems the notions of “simplifying” and “reductive” are commonly used with diverse meanings. To avoid misunderstandings we use “aligned” for the local restriction on a single rule and “compatible” (with different prefixes) for the restrictions that involve the reduction relation of the whole rule system.

[Alignment of a Rule w.r.t. a Termination-Pair] Let (>, ▷) be a termination-pair over sig/V. A rule ((l, r), C) ∈ is called aligned with (>, ▷)

l > r ∧ ∀u ∈ TERMS(C) : l ▷ u

Now if we compare the use of orderings in the field of conditional equations (e.g., for the “decreasing”-property in Dershowitz[17, 16]), we find that there usually is a single noetherian ordering containing ▷_{ST}. This ordering corresponds^{67} to our ordering ▷ of a terminationpair (>, ▷). Our additional >, however, is very useful both in practice and for establishing theoretical properties as we will see in the sequel. Furthermore, our previous discussion reveals how to establish the properties required for ▷ and its interference with rules in practice.

While we require > to be a reduction ordering, we avoid the superfluous commonplace restriction of ▷ to be^{65} ▷ := ▷_{ST} ∪ ((> ∩ ⋃_{s∈𝕊}(T_{SIG,s} × T_{SIG,s})) ∘ ⊵_{ST}), because this may not be sufficient for alignment of given rules as in the fol. example of Dershowitz^{68}:

[▷ := ▷_{ST} ∪ ((> ∩ ⋃_{s∈𝕊}(T_{SIG,s} × T_{SIG,s})) ∘ ⊵_{ST}) is Too Restrictive]

b = c
f b = f a
a = c ⟵ b=c

Alignment of these rules requires a▷b which we cannot achieve by the above construction of ▷ : a > b isimpossiblesincealignmentofthesecondrulerequires f b > f a , whichalsoforbids a > f^{n+1} b , sincethenweget a > f^{(n+1)} a > f^{2(n+1)} a > · · · . Thus, for theoretical treatment, the procedure of (2) of Example 3 is to be preferred to that of (1) of Example 3, whereas (for practically guaranteeing alignment of rules) (2) of Example 3 lacks any hints on how to semi-decide > (even for decidable ▷).

All in all, there seems to be no proper reason for preferring one of >, ▷ to the other and we thus have introduced the notion of a termination-pair (>, ▷).

65Cf. Lemma 8.1(8.1)

66While irreflexivity, transitivity, sort-invariance and T -monotonicity of > are trivial, V-stability for t′ > t′′ ; t′, t′′ ∈ T_{SIG,s} w.r.t. a substitution σ ∈ SUB(V, T ) can be seen the fol. way: For arbitrary t ∈ T and p ∈ t with t/p ∈ T_{SIG,s} define ξ := min Sep(V(t), V(t′, t′′)) and then ϱ := σV(t′, t′′) ∪ ξ^{−1}V \ V(t′, t′′)

. Now by tξ[ p ← t′] ▷ tξ[ p ← t′′] we get t[ p ← t′σ] = tξ[ p ← t′]ϱ ▷ tξ[ p ← t′′]ϱ = t[ p ← t′′σ] .

67V-stability can always be achieved by restriction to ground terms

68Cf. p. 546 in [17]

8.2 Several kinds of Compatibility of CRSs

The following kind of compatibility is a generalization to negative conditions and also a slight weakening of the notion of “decreasingness” in Dershowitz[16].

[Compatibility of a CRS with a Termination-Pair] A CRS R over sig/cons/V is X-compatible with a termination-pair T = (>, ▷) over sig/V ∀((l, r), C) ∈ R : ∀τ ∈ SUB(V, T (X)) :

((Cτ fulfilled w.r.t. ⟶_{R,X}) ⇒ ( ((l, r), C)τ is aligned with T ))

Compatibility of a CRS R guarantees alignment of an instantiated rule of R when its condition is fulfilled. But, while this kind of compatibility is convenient for obtaining further theoretical properties of the reduction relation, we have a problem when using this kind of compatibility of R in practice of reduction: The terms in Cτ must be smaller than lτ only if Cτ is fulfilled; but for easily deciding whether Cτ is fulfilled we need its terms to be smaller than lτ and the analogous property for the other rules. That this need not be a vicious circle is shown by the following definition, which allows us to test the literals in the condition from left to right, using the old programming trick of a sequential “shortcircuiting” AND-operator^{69}. Notice that the difference to Definition 8.2 is in the quantified variable i occurring as an index which allows us to step inductively from (< i) to i.

[Left-Right-Compatibility] A CRS R over sig/cons/V is X-left-right-compatible with a termination-pair T = (>, ▷) over sig/V ∀((l, r), L_{0} … L_{n−1}) ∈ R : ∀τ ∈ SUB(V, T (X)) :

( \begin{matrix}∀i < n : ( & ((L_{0} … L_{i−1})τ fulfilled w.r.t. ⟶_{R,X}) ⇒ & ∀u ∈ TERMS(L_{i}) : lτ ▷ uτ ) \\ ∧  ( & ((L_{0} … L_{n−1})τ fulfilled w.r.t. ⟶_{R,X}) ⇒ & lτ > rτ  ) \end{matrix} )

[Don’t-Care-Compatibility] A CRS R over sig/cons/V is X-don’t-care-compatible with a termination-pair T = (>, ▷) over sig/V ∀((l, r), L_{0} … L_{n−1}) ∈ R : ∀τ ∈ SUB(V, T (X)) :

\binom{∀i < n :  ∀u ∈ TERMS(L_{i}) : lτ ▷ uτ}{∧  ( ((L_{0} … L_{n−1})τ fulfilled w.r.t. ⟶_{R,X}) ⇒ lτ > rτ  )}

Having a left-right-compatible CRS, we don’t have to test the instantiated rules for alignment anymore, provided that we test the literals of the instantiated conditions from left to right until one of them fails. Having a don’t-care-compatible CRS, we can even test the literals of the instantiated conditions in parallel and don’t have to care for the position of these equations in the condition list. The don’t-care-compatibility is conceptionally the same as the “decreasingness” in Dershowitz[16].

The “compatibility” of Definition 8.2 (which seems to be the least restrictive one tractable in theory) is intended to be an interface for generating logically stronger kinds of “compatibility” that are useful in practice (cf. definitions 8.2, 8.2), where the don’t-care-compatibility seems to be the most important one. For restrictions of ⟶_{R,X}, however, even weaker kinds of “compatibility” than the one of Definition 8.2 may be sufficient.

69E.g. ‘and then’ (instead of ‘and’) in SIMULA, ‘&&’ (instead of ‘&’) (or more accurately ‘ && ’ instead of ‘( !=0?1:0)&( !=0?1:0)’) in C, ‘AND’ in LISP.

[⟶_{R,normal}]

Let R be a CRS over sig/cons/V. We define the normal reduction relation ⟶_{R,normal} by

s⟶t if ∃((l, r), C)∈R: ∃σ ∈SUB(V, T ): ∃p∈s:(\begin{matrix}s/p = lσ & ∧ \\ t = sprσ \\ ∧σ is normal w.r.t. l, ⟶_{R,V}∧ \end{matrix} ,

where “σ is normal w.r.t. l, ⟶” if ∀x ∈ V(l)\{l} : xσ ∉ dom(⟶). Let R be a CRS over sig/cons/V. Now dom(⟶_{R,normal}) = dom(⟶_{R,V}) and dom(⟶_{R,normal} ∩ (GT × GT )) = dom(⟶_{R,V}) ∩ GT . While we could give more interesting sufficient confluence tests for ⟶_{R,normal}, the following is sufficient for our purposes: Let R be a CRS over sig/cons/V. If ⟶_{R,V} is [ground] confluent and ⟶_{R,norm} is [ground] normalizing, then ⟶_{R,norm} is [ground] confluent, too. Now, for ⟶_{R,normal} the following kind of compatibility is appropriate: [[Ground] Normal Compatibility] A CRS R over sig/cons/V is [ground] normal compatible with a termination-pair T = (>, ▷) over sig/V ∀((l, r), C) ∈ R : ∀τ ∈ SUB(V(((l, r), C)), [∩GT (sig)]) :

(( \begin{matrix}τ is normal w.r.t. l, ⟶_{R,V} \\ ∧ Cτ fulfilled w.r.t. ⟶_{R,V} \end{matrix} ) ⇒ ( ((l, r), C)τ is aligned with T ))

69We are not bold enough to test fulfilledness w.r.t. ⟶_{R,normal} here because we would need further restrictions to guarantee a minimal relation satisfying the definition.

8.3 Results for Compatible CRSs

Let R be a CRS over sig/cons/V; X⊆Y⊆V ; and T = (>, ▷) a termination-pair over sig/V.

Assume that R is Y-compatible with T. Now we have ⟶_{R,Y}⊆ > and⟶_{R,Y}∪ ↠_{R,Y}∪▷_{ST} ⊆ ▷, whichisnoetherian.F urthermore, R isX−

compatible with TandV−compatible withthetermination−pair ( ⟶^{+}_{R,V}, (⟶_{R,V} ∪ ↠_{R,V} ∪ ▷_{ST})^{⊕} ) over sig/V.

The following notion of “weakly joinable” weakens “joinable” by adding a confluence requirement to the premise.

A critical peak (((t_{0}, t_{1}), D), t̂, p) is ▷-weakly joinable w.r.t. R, X if ∀τ ∈ SUB(V, T (X)) :

(\binom{Dτ fulfilled w.r.t. ⟶_{R,X} ∧}{∀u : ( u ◁ t̂τ ⇒ ( ⟶_{R,X} is confluent below u ) )} ⇒ t_{0}τ↓_{R,X}t_{1}τ) .

For compatible CRSs we can now give a complete confluence test à la Knuth-Bendix:

[Syntactic Confluence Test] Let R be a CRS over sig/cons/V and X⊆V . Assume that R is X-compatible with a termination-pair T = (>, ▷) over sig/V. The following two are logically equivalent:

1. ⟶_{R,X} is confluent.

2. All critical peaks in CP(R) are (▷-weakly) joinable w.r.t. R, X.

The following theorem, which is similar to Theorem 5.1 in enhaus&Becker[1], drops the compatibility restriction of Theorem 8.3 for those condition literals which contain constructor variables only, while it does not require (quasi) overlay joinability as Theorem 7.

[Syntactic Confluence Test] Let R be a CRS over sig/cons/V; X⊆V ; and T = (>, ▷) a termination-pair over sig/V. Assume the constructors to be free, i.e. each left-hand side of R contains a non-constructor symbol. Furthermore, we require the fol. compatibility-property: ∀((l, r), C) ∈ R : ∀τ ∈ SUB(V, T (X)) :

((Cτ fulfilled w.r.t. ⟶_{R,X}) ⇒ ( \begin{matrix}lτ > rτ ∧ \\ ∀L in C : ( \begin{matrix}∀u ∈ TERMS(L) : lτ ▷ uτ \\ ∨ V(L) ⊆ V_{CONS} \end{matrix} ) \end{matrix})) .

Now, the following two are logically equivalent:

1. ⟶_{R,X} is confluent.

2. All critical peaks in CP(R) are (▷-weakly) joinable w.r.t. R, X.

Let R be a CRS over sig/cons/V and T = (>, ▷) a termination-pair over sig/V. Let X be an enumerable subset of V. Now, if^{70}

1. R is X-left-right-compatible with T, or

2. R is X-compatible with T, ▷ ∩ (T (sig, X)×T (sig, X)) is semi-decidable, and ▷ ∩ (GT (cons)×GT (cons)) is decidable,

then the fol. items hold:

70This condition is essential: Cf. Lemma 8

1. ⟶_{R,X}-reducibility of terms from T (sig, X) is semi-decidable.

2. { t | s⟶^{+}_{R,X}t } is a semi-decidable set for all s ∈ T (sig, X).

3. { t | s⟶^{+}_{R,X}t } is a finite computable set for all s ∈ GT (cons).

The fol. lemma, however, shows that compatibility does not imply decidability of reducibility as long as extra-variables are permitted.

[Reducibility of Ground Terms is Still Not Co-semi-decidable] There is a left-linear, non-overlapping, merely positive conditional rule system R with noetherian and confluent reduction relation ⟶_{R,V}, which is V-don’t-care-compatible with a termination-pair (▷, ▷) with decidable ▷, and for which reducibility of ground terms is not co-semi-decidable.

If we do not allow extra-variables, however, we get the following decidability result, which is important due to Corollary 8.

Let R be a CRS over sig/cons/V and T = (>, ▷) a termination-pair over sig/V. Let X be an enumerable subset of V. Now, if R is extra-variable free^{71} and if^{72}

1. R is X-left-right-compatible with T, or

2. R is X-compatible with T and ▷ ∩ (T (sig, X)×T (sig, X)) is decidable

then the fol. items hold:

1. ⟶_{R,X}-reducibility of terms from T (sig, X) is decidable.

2. { t | s⟶^{+}_{R,X}t } is a finite computable set for all s ∈ T (sig, X).

3. Confluence of ⟶_{R,X} is co-semi-decidable.

Confluence of ⟶_{R,∅} for extra-variable free, V-don’t-care-compatible Def-MCRSs R cannot be semi-decidable because it is not semi-decidable even for extra-variable free, noetherian, left-linear, monadic, unconditional rule systems^{73}. While confluence of ⟶_{R,V}, however, is decidable for noetherian, unconditional rule systems R, the fol. lemma does not give us a chance in general to decide confluence of ⟶_{R,V} for extra-variable free, don’t-care-compatible Def-MCRSs R.

[Confluence of ⟶_{R,V} is Not Semi-decidable] There is a signature sig with sub-signature cons and a termination-pair (▷, ▷) over sig/V with decidable ▷, such that confluence of ⟶_{R,V} is not semi-decidable in general for leftlinear, extra-variable free, merely positive conditional rule systems R over sig/cons/V which are V-don’t-care-compatible with (▷, ▷).

71This condition is essential: Cf. Lemma 8.3

72This condition is essential: Cf. the lemmas 8 and 8

73Cf. Kapur[32]

Let R be a CRS over sig/cons/V. Let T = (>, ▷) be a termination-pair over sig/V. Assume that R is [ground] normal-compatible with T. Now we have (⟶_{R,normal}[ ∩ (GT × GT )]) ⊆ >, and

∀s ∈ T [ ∩ GT ] : ∃t ∈ T [ ∩ GT ] : s⟶^{∗}_{R,V}t∉dom(⟶_{R,V}) .

Furthermore, if R is extra-variable free and if ▷[ ∩ (GT × GT )] is decidable and ⟶_{R,V} is [ground] confluent, then ⟶_{R,V}-reducibility [of ground terms] is decidable and ⟶^{+}_{R,normal}[{s}] is a finite computable set for all s ∈ T [ ∩ GT ].

9 Inductive Validity

[Syntax of Formulas] Let X⊆V. The set of formulas (or Gentzen clauses) over sig, X is defined to be

:= AT (sig, X)^{∗} × AT (sig, X)^{∗} ,

where AT (sig, X) ⊆ CONDLIT (sig, X) is the set of atoms over the following predicate symbols on terms from T (sig, X): ‘=’ (binary, symmetric, sort-invariant) and ‘Def’ (unary). A formula (Γ, Δ) will be written “ Γ ⟶ Δ ”. and (when we list Γ orΔ)themulti − setparentheses‘⟨′, ‘⟩′willbeomitted.

[Validity of Formulas in sig/cons-algebras] Let X⊆V; A be a sig/cons-algebra; and κ ∈ SUB(X, A) . An atom (u=v)∈ AT (sig, X)istruew.r.t. A_{κ} if A_{κ}(u) = A_{κ}(v) ; andanatom(Def u) ∈ AT (sig, X)(with u ∈ T (sig, X)_{s} ; s ∈ 𝕊 )istruew.r.t. A_{κ} if A_{κ}(u) ∈ A(CONS, s) .

A formula (Γ, Δ)∈ isvalidinA if ∀κ ∈ SUB(X, A) :

( ∀A in Γ : (A is true w.r.t. A_{κ}) ⇒ ∃A in Δ : (A is true w.r.t. A_{κ}) ) .

The following example illustrates why validity of a formula in all sig/cons-models may not be appropriate for our intended abstract notion of validity. Therefore, in the sequel we define and disambiguate four different conceivable abstract notions of validity, which we will call type-A/B/C/D-inductive validity.

(continuing Example 2.2) Let x, y ∈ V_{CONS,nat} and l ∈ V_{CONS,list}. Consider the following Def-MCRS:

R: \overleftarrow{⟵ , Def , Def}

Now we might have the intuition that the formula

⟶ , (:#)

should be inductively valid w.r.t. to R.

But this formula is not valid in all sig/cons-models of R because it is not even valid in the constructor-minimum model GT /⟷^{∗}_{R,∅} of R (cf. Corollary 6) when we add a new constructor constant of sort list (since ↚→^{∗}_{R,∅} and ↚→^{∗}_{R,∅} ).

This motivates the notions of inductive validity which are defined below and apply to this formula, in the sense that the formula (#) is type-A/B/C/D-inductively valid.

[Inductive Substitutions] Define the set of inductive substitutions by:

CGSUB(V, cons) := { τ ∈ SUB(V, T ) | τ[V_{CONS}] ⊆ GT (cons) ∧ τV_{SIG} = idV_{SIG} }

[Type-A/B/C-inductive Validity] Let R be a CRS over sig/cons/V. Let M be the class of all sig/cons-models of R. Let K be the class of all constructor-minimal models of R. Let (Γ, Δ)∈ .Now Γ ⟶ Δ iscalled … … type − A − inductivelyvalidw.r.t. R if

∀A ∈ M : ∀τ ∈ CGSUB(V, cons) : ((Γ, Δ)τ is valid in A).

… type-B-inductively valid w.r.t. R if

∀A ∈ K : ∀τ ∈ CGSUB(V, cons) : ((Γ, Δ)τ is valid in A).

… type-C-inductively valid w.r.t. R if ∀A ∈ K : ( (A is CONS:cons-term-generated) ⇒ ((Γ, Δ) is valid in A) ) .

Type-A- and Type-B-inductive validity reduce inductive validity of formulas to validity of their inductive instances. This disallows the constructor variables of formulas to range over objects of the constructor sub-universe which are not denoted by constructor ground terms (with sort invariant). While we restrict the constructor variables in the formulas by substituting them with constructor ground terms, we do not instantiate their general variables with (general) ground terms. This is because we do not want the general variables to range over the junk generated by ground terms only, but possibly over additional junk, e.g. of non-constructor symbols which might be introduced later on. Indeed, allowing this additional junk is necessary for the monotonicity of our logic w.r.t. consistent extensions (cf. Theorem 9).

Type-C-inductive validity requires a model A considered for inductive validity to satisfy that A is CONS:cons-term-generated, which is equivalent to

∀s ∈ 𝕊 : A(CONS, s) = A[GT (cons)_{s}] .

Because this means that there are no constructor objects unless they are syntactically specified by constructor ground terms (with sort invariant), this restriction can be viewed upon as another “closed world assumption” on the constructor part of the specification, besides the one on constructor ground equality used for motivating the notion of Defmoderate CRSs.

While our inductive validities of type-A/B/C do not change the “SIG-part of validity”, they differ from validity in all sig/cons-models due to their influence on the “CONSpart” of the models or of the evaluation of formulas: Inductive substitutions make the “junk” of the constructor sub-universes inaccessible to constructor variables; the constructor sub-universes of CONS:cons-term-generated sig/cons-models contain no “junk” at all; and constructor-minimal models have no “confusion” in their constructor sub-universes. Thus, regarding the constructor sub-universes, we can classify type-A as “junk and confusion”, type-B as “junk but no confusion”, and type-C as “no junk and no confusion”. À la carte, one could ask for “confusion but no junk” and define it like type-C with the ‘K’ replaced by an ‘M’, but we do not suggest this here because we think confusion to be even less digestible than junk and because understanding the dissection of the notion of inductive validity is even now difficult enough.

Before we are going to disambiguate our notions of inductive validity, we would like to emphasize that the dissection into different types of inductive validity does not require our two types of variables or the negative conditions in our rules, but instead is brought about alone by nonempty antecedents ‘Γ′informulasoftheform“ Γ ⟶ Δ ′′.

The fol. example shows the difference between type-A- and type-B-inductive validity:

[Type-A ≠ Type-B] (continuing Example 9)

We might have the intuition that and arenotthesame; i.e. that

⟶

shouldbeinductivelyvalid.T hisformula, however, isnotvalidinthetrivialsig/cons−algebra, andthereforenottype− A−inductivelyvalid(notevenforR = ∅).Asthetrivialsig/cons−algebra isnotconstructor− minimal, wecanexcludeitbyrequiringthemodelsunderconsiderationtobeconstructor−minimal.Indeed, theaboveformulaistype− B − inductivelyvalid.

That it is very difficult to conclude from type-B- to type-A-inductive validity, can be seen from the fol. formula which is type-B- but not type-A-inductively valid (since there are sig/cons-models of R which identify with butdonotidentify with) :

⟶

The above example is characteristic for the difference between type-A- and type-B-inductive validity in the following sense:

Let R be a CRS over sig/cons/V. Let (Γ, Δ) ∈. Now w.r.t. R the fol. holds:

1. Type-A-inductive validity of (Γ, Δ) implies type-B-inductive validity of (Γ, Δ).

2. If no rule in R has a negative^{74} condition, then type-B-inductive validity of “ ⟶ Δ ” implies type-A-inductive validity of “ ⟶ Δ ”.

The fol. example shows the difference between type-B- and type-C-inductive validity:

[Type-B ≠ Type-C] (continuing Example 2.2) Suppose that we enrich the signature of Example 2.2 with a new non-constructor constant dunno of sort bool . Since for type-B-inductive validity we also have to consider models A with |A(CONS, bool)| > 2 , the fol. formula is type-C- but not type-B-inductively valid (not even for R=∅) :

Def dunno ⟶ dunno , dunno .

The above example is characteristic for the difference between type-B- and type-C-inductive validity in the following sense:

Let R be a CRS over sig/cons/V. Let (Γ, Δ) ∈. Now w.r.t. R the fol. holds:

1. Type-B-inductive validity of (Γ, Δ) implies type-C-inductive validity of (Γ, Δ).

2. If for each atom (Def u) in Γ theformula“ ⟶ Def u′′istype−C−inductivelyvalid, thentype− C − inductivevalidityof(Γ, Δ) impliestype − B − inductivevalidityof(Γ, Δ).

74i.e. containing a literal of the form (u≠v)

[Type-C ≠ Type-D] (continuing Example 9) Suppose that we enrich the signature of Example 9 with a new non-constructor symbol and add the rule . One might have the intuition that is still undefined and thus the formulas

Def ⟶
⟶

should be inductively valid. They are not type-C-inductively valid, however, because they are not valid in the initial constructor-minimal model^{75} (cf. Corollary 6) of the Def-MCRS R augmented with the rule . They are type-D-inductively valid (defined below), though.

[Type-D-inductive Validity] Let R be a CRS over sig/cons/V. Let (Γ, Δ)∈ . Now“ Γ ⟶ Δ ′′iscalledtype − D − inductivelyvalidw.r.t. R if

(Γ, Δ) isvalidin T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} .

If ⟶_{R,V_{SIG}} is confluent and R is Def-moderate, then (by Theorem 6) T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} is a constructor-minimal model of R (i.e. T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} ∈ K ) which is obviously CONS:cons-term-generated, and thus belongs to the models considered for type-C-inductive validity. Furthermore, T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} is free in K over V_{SIG} and therefore distinguished from the other models having no “confusion” in their constructor sub-universes by also having no confusion in its (general) universes and by all its junk being generated by V_{SIG}.

Example 9 is characteristic for the difference between type-C- and type-D-inductive validity in the following sense:

Let R be a Def-MCRS over sig/cons/V. Let (Γ, Δ) ∈. Now w.r.t. R the following holds:

1. If ⟶_{R,V_{SIG}} is confluent^{76} Next thing to note about type-D-inductive validity is that it is rather close to operationalization:

75which has to be considered for type-C-inductive validity because it is CONS:cons-term-generated and constructor-minimal also w.r.t. the non-augmented rule system R

76The following allows to apply the confluence criterion of Theorem 7: If we additionally require ∀((l, r), C) ∈ R : ∀(u=v) in C : ( Def u, Def v are in C ) , then we can weaken the confluence requirement to confluence of ⟶_{R,V_{SIG}} ∩(D_{V_{SIG}}×D_{V_{SIG}} )forD_{V_{SIG}} := { u ∈ T (sig, V_{SIG}) | ∃û ∈ GT (cons): u⟷^{∗}_{R,V_{SIG}} û }., thentype− C − inductivevalidityof(Γ, Δ) impliestype − D − inductivevalidityof(Γ, Δ).

2. If ⟶_{R,∅} is confluent^{77}

Let R be a CRS over sig/cons/V. Let (Γ, Δ) ∈. Now the following two items are logically equivalent:

1. (Γ, Δ) is type-D-inductively valid.

2. ∀τ ∈ SUB(V, T (V_{SIG})) :

( ∀(u=v) in Γ: uτ⟷^{∗}_{R,V_{SIG}}vτ ∧ ∀(Def u) in Γ: ∃û ∈ GT (cons): uτ⟷^{∗}_{R,V_{SIG}} û )
⇒
( ∃(u=v) in Δ: uτ⟷^{∗}_{R,V_{SIG}}vτ ∨ ∃(Def u) in Δ: ∃û ∈ GT (cons): uτ⟷^{∗}_{R,V_{SIG}} û )

By the following corollaries we see that our notions of inductive validity specialize to the single well-known notion of inductive validity of equations w.r.t. merely positive conditional specifications.

(of Lemma 9) Let R be a CRS over sig/cons/V without negative conditions. Let Δ ∈ AT (sig, V)^{∗}. Now w.r.t. R the following items are logically equivalent:

1. “ ⟶ Δ ” is type-A-inductively valid.

2. “ ⟶ Δ ” is type-B-inductively valid.

(of Lemma 9) Let R be a CRS over sig/cons/V. Let Δ ∈ AT (sig, V)^{∗}. Now w.r.t. R the following items are logically equivalent:

1. “ ⟶ Δ ” is type-B-inductively valid.

2. “ ⟶ Δ ” is type-C-inductively valid.

(of Lemma 9) Let R be a Def-MCRS over sig/cons/V. Let Δ ∈ AT (sig, V)^{∗}. Furthermore, assume ⟶_{R,V_{SIG}} to be confluent. Now w.r.t. R the following items are logically equivalent:

1. “ ⟶ Δ ” is type-C-inductively valid.

2. “ ⟶ Δ ” is type-D-inductively valid.

Having established our notions of inductive validity, let us now have a brief look on notions of inductive validity in literature, most of which can be described as specializations of our notions of inductive validity. If we consider all symbols to be constructor symbols (and, a fortiori, drop our negative conditions in our rules), we find type-A-inductive validity in Kounalis&Rusinowitch[35] as well as in Bouhoula[11]. The notion of inductive validity of Zhang[48] can be described as type-A when we implicitly take all variables in rules for general variables and all variables in formulas for constructor variables. Considering again all symbols to be constructor symbols (but allowing an unrestricted set of Gentzen clauses over equality atoms for specification)^{78}, type-A-inductive validity had also been included in a preliminary version of Bachmair&Ganzinger[4]. In the final version, however, after developing their perfect model in Bachmair&Ganzinger[5], they have dropped it; instead, we now find in Ganzinger&Stuber[20] inductive validity defined to be validity in the perfect model,^{79} which is more similar to type-D with our free constructorminimal model (which their approach (allowing more general specifications) does not provide) replaced with the perfect model. In Padawitz[37] and Kounalis&Rusinowitch[34] (contrary to Kounalis&Rusinowitch[35] (cf. above)), we find the usual validity in the initial model which is like^{80} our type-D. Bevers&Lewi[9] also use initial model or type-D-inductive validity (without non-constructor symbols and without negative conditions in rules or formulas); however, they claim it to be equivalent to type-A-inductive validity, which is obviously not correct, even in their restricted context. We have already discussed the general ideas of Kapur&Musser[30, 31] in Section 3 (“Our Solution”; around footnote 20). We have no notion of inductive validity corresponding to their notion in [30]. However, if a constructor-minimum model A exists and we take a choice set of GT (cons)/(ker(A) ∩ (GT (cons)×GT (cons))) for their set of constructor terms, the notion of inductive validity of [31] coincides^{80} (at least for their restriction to formulas of the form “ ⟶ u v ”) with our type-C and (in the absence of ‘Def ’-literals equivalently) type-B-inductive validity.

78instead of our R, which is restricted to be a subset of our set of rules

Now it is difficult to conclude which notion of inductive validity is the appropriate one. We think that all our four types are of interest. Type-C and type-D are our favourites because they capture the intuition of our approach. (Reconsider the formulas of Example 9 as well as the formula of Example 9.) In particular, the permission of confusion in the constructor sub-universes of the models considered for type-A, conflicts with our treatment of negative conditions of rules by negation as failure restricted to the objects of the constructor sub-universes, which was justified in Section 3 by a closed world assumption on equality of these objects. The second formula of Example 9 illustrates this conflict: Since we have “ ⟷^{∗}_{R,∅} ” we really would like “ ⟶ ” to be inductively valid. A more objective criterion for convenience of a notion of inductive validity is its suitability for theorem proving. Type-D is rather close to operationalization (cf. Lemma 9) and a prover for it may be used (via Lemma 9(2)) for showing type-C-inductive validity. This procedure is not complete (cf. Example 9) for establishing type-C-inductive validity; but the type-C-inductively valid formulas we lose seem to be in general very difficult to prove. While the details of inductive theorem proving methods and techniques within our constructor-based approach are far beyond the scope of this paper, one important feature which a notion of inductive validity needs for being convenient for inductive theorem proving is its monotonicity w.r.t. consistent extension of the specification: Contrary to deductive first order theorem proving, inductive theorem proving often is only successful when one tries to show stronger theorems than one initially intended to show. This is because induction hypotheses are not only a task but also a tool for the inductive argumentation. Sometimes the required induction hypotheses or lemmas are not expressible by our formulas unless we extend the specification in a consistent manner. Consistent extensions also play an important role for incremental refinement and modular construction of specifications. Since then we do not want to lose the theorems already shown, we need some means to tell whether they are still valid in the extended specification. Thus a notion of inductive validity can be said to be more adequate the more monotonic w.r.t. consistent extension of the specification it is. Luckily, (contrary to perfect model validity) our four notions behave rather well:

79still considering all symbols to be constructor symbols and allowing an unrestricted set of Gentzen clauses over equality atoms for specification

80when we consider all symbols to be constructor symbols and drop our negative conditions in our rules

(Monotonicity of Inductive Validity of Formulas w.r.t. Consistent Extension of the Specification)

Let R be a CRS over sig/cons/V. Let R′ be another CRS, but over sig′/cons′/V′; with

sig′ = (𝔽′, 𝕊′, α′)
cons′ = (ℂ′, 𝕊′, α′ℂ′)
V′{SIG, CONS}×𝕊 = V

𝔽 ⊆ 𝔽′_{ℂ ⊆ ℂ′ ⊆ 𝔽′}_{𝕊 ⊆ 𝕊′}_{α ⊆ α′} R ⊆ R′

and for^{81} c ∈ ℂ′\ℂ ; α′(c) = s_{0} … s_{n−1} → s_{n} : s_{n} ∈ 𝕊′\𝕊 . Thus, sig′/cons′/V′ is an enrichment of sig/cons/ V in a very general^{82} sense.

Moreover, assume^{83}: ∀((l, r), C) ∈ R′ \ R : l ∉ T (cons, V_{SIG}⊎V_{CONS}) . (:$_{1}) Assume^{84} ⟶_{R′,∅} to be confluent^{85}. (:$_{2})

Now, for (Γ, Δ) ∈, we have:

A. (Even without the assumptions ($_{1}), ($_{2}):) If (Γ, Δ) is type-A-inductively valid w.r.t. R, then (Γ, Δ) is type-A-inductively valid w.r.t. R′, too.

B. If R′ is Def-moderate, and if (Γ, Δ) is type-B-inductively valid w.r.t. R, then (Γ, Δ) is type-B-inductively valid w.r.t. R′, too.

C. If R′ is Def-moderate, and if (Γ, Δ) is type-C-inductively valid w.r.t. R, then (Γ, Δ) is type-C-inductively valid w.r.t. R′, too.

D. Assume ⟶_{R,∅} and ⟶_{R′,V′_{SIG}} to be confluent^{86}. Now, if If for each u ∈ TERMS(Γ) the formula “ ⟶ Def u ” is type-D-inductively valid w.r.t. R,^{87} and if (Γ, Δ) is type-D-inductively valid w.r.t. R, then (Γ, Δ) is type-D-inductively valid w.r.t. R′, too.

81If we did not require this, we would get new constructor ground terms of old sorts and new inductive instances of old formulas, which clearly destroys type-A/B/C/D-inductive validity. E.g.: If we add the new constructor constant of sort list to the specification of Example 9, then the formula (#) becomes type-A/B/C/D-inductively invalid.

82Please notice that the last requirement is the only additional one on the signatures compared to Theorem 6.

83This has to be required for keeping the negative conditions of the instantiated rules being fulfilled: Having founded our inequalities on old constructor ground terms, all we have to take care of now is not to confuse these terms.

84Confluence is necessary of course: Consider the rule system

nicep ⟵ , Def , Def

and the type-B/C/D-inductively valid formulas \overrightarrow{⟶ nicep ,}

none of which keeps being type-B/C/D-inductively valid if we add the rules dunno ; dunno .

85The following allows to apply the confluence criterion of Theorem 7: If we additionally require ∀((l, r), C) ∈ R′ : ∀(u=v) in C : ( Def u, Def v are in C ) , then we can weaken the confluence requirement

to confluence of ⟶_{R′,∅} ∩ (D′_{∅}×D′_{∅}) for D′_{∅} := { u ∈ GT (sig′) | ∃û ∈ GT (cons′) : u⟷^{∗}_{R′,∅} û } .

86The fol. allows to apply the confluence criterion of Theorem 7: If we additionally require ∀((l, r), C) ∈ R′ : ∀(u=v) in C : ( Def u, Def v are in C ) , then we can weaken the confluence requirement to confluence of ⟶_{R,∅} ∩ (D_{∅}×D_{∅}) and ⟶_{R′,V′_{SIG}} ∩ (D′_{V′_{SIG}} ×D′_{V′_{SIG}} ) for

D_{∅} := { u ∈ GT (sig) | ∃û ∈ GT (cons) : u⟷^{∗}_{R,∅} û } and

D′_{V′_{SIG}} := { u ∈ T (sig′, V′_{SIG}) | ∃û ∈ GT (cons′) : u⟷^{∗}_{R′,V′_{SIG}} û } .

87This means that each SUB(V, T (V_{SIG}))-instance of a term occurring in the antecedent Γ must be defined, i.e. have a congruent constructor ground term. This restriction is necessary because R′ may define some terms that were undefined in R: In the situation of Example 9 we can destroy the type-D-inductive validity of the two formulas there by adding the rule .

10 Conclusion

We have presented a novel constructor-based approach to positive/negative-conditional equational specifications, which was heavily inspired by previous work of Kapur&Musser[30, 31] (for the case of unconditional equations only) and Zhang[46]. Under some reasonable syntactical restrictions on the form of positive/negative-conditional rules it turns out that the combination of these ideas with the approach of Kaplan[28] becomes very fruitful and also relevant for practical purposes since many natural specifications involve both conditional equations with positive and negative conditions and partially specified functions. For such specifications we have been able to define semantics admitting a unique model, being initial in the class of constructor-minimal models, if [ground] confluence of our reduction relation is provided. The lack of an initial model was one of the main disadvantages of the approach of Kaplan[28]. The addition of constructor variables conceptually completes the constructor-based approach and shows up new possibilities for the practice of specification. Furthermore, a thorough and precise analysis of termination and decidability issues has led to some useful and slightly weakened “decreasingness”-notions for positive/negativeconditional rule systems. Moreover, we have also been able to provide some interesting confluence criteria. Finally, we have defined and disambiguated several notions of inductive validity in our constructor-based approach. Since (under reasonable assumptions) all these kinds of validity are monotonic w.r.t. consistent extension of the specification, the whole approach may be considered to be a firm theoretical basis for (first-order) inductive theorem proving in theories specified by positive/negative-conditional equations.

Dedication: To my father, Friedhelm Wirth, in gratefulness.

Acknowledgements: We would like to thank Jürgen enhaus and Klaus Becker for fruitful discussions, and Klaus Madlener and Rüdiger Lunde for useful hints.

Editorial Remark: This report is a thorough revision of Wirth&Gramlich[44]^{88} including lots of significant refinements and extensions^{89}.

88Cf. also the shortened version Wirth&Gramlich[45], which has been published in the proceedings of the Third International Workshop on Conditional Term Rewriting Systems in Pont-à-Mousson, July 1992.

89Besides lots of important details, Wirth&Gramlich[44] lacks the following: Constructor variables, embedding into the order-sorted framework, parameterization of ⟶_{R,X} in X, Theorem 6, Theorem 7, Lemma 8.1, Theorem 8.3 and the rest of Section 8.3, and (most important) the entire Section 9 about inductive validity.

A The Proofs

Proof of Lemma 5

1. Due to ker(A)=ker(B), A and B do not differ in their evaluation of two ground terms of the same sort regarding ‘=’ or ‘≠’. Furthermore, if A(t) ∈ A(CONS, s) for some t∈ GT_{SIG,s}, thenthereissomet′ ∈ GT_{CONS,s}with B(t′) = B(t) , bywhichweget B(t) ∈ B(CONS, s) .T hus‘Def t′istruew.r.t. A onlyifitistruew.r.t. B.Since‘Def′occursasapositiveliteralintheconditionsoftherulesonly, A isasig/cons− model ofeachgroundruleofwhichB isasig/cons − model. Now, ifB isasig/cons−model ofR, bytheSubstitution−Lemma(4.2), itisasig/cons− model ofallgroundinstancesoftherulesofR, whichimpliesthatA isasig/cons − model ofallgroundinstancesoftherulesofR, whichagainimpliesthatA isasig/cons − model ofallrulesofR.T hislaststepcanbeseenthefollowingway : Letκ be any Avaluation of V. Then by the Axiom of Choice there is a σ ∈ SUB(V, GT ) such that σ ∘ A = κ . Then by the Substitution-Lemma ∀t ∈ T : A_{κ}(t) = A(tσ) .

2. This is nothing but an application of the Homomorphism-Theorem(4.2).

3. By (2 ) and ≲_{H} ⊆ ≲_{CONS} .

Proof of Lemma 5

1. Trivial.

2. If B is minimal itself, we are finished. If not, by Lemma 5(2) we can w.l.o.g. assume B to be a factor algebra of GT and consider congruences on GT instead of sig/consalgebras. We only have to apply Zorn’s Lemma to get a minimal congruence whose factor algebra is a sig/cons-model of R, because this factor algebra will be a minimal sig/cons-model of R. Therefore, we are now going to show that the premise of Zorn’s Lemma is satisfied.

Let CHAIN = { ∼_{i} | i ∈ I } be a nonempty ⊆-chain of congruences on GT with ∀i ∈ I : (GT / ∼_{i} is a sig/cons-model of R) . Define ≈:= ⋂_{i∈I} ∼_{i} . Of course, ≈ is a congruence on GT that bounds CHAIN below. The only thing left to be shown is that GT /≈ is a sig/cons-model of R. Contrariwise there was^{90} a (l=r⟵C) ∈ R and a σ ∈ SUB(V, GT ) with ∀L in C : ∀u, v : (L = (u=v) ⇒ uσ ≈ vσ) ; ∀L in C : ∀u : (L = (Def u) ⇒ ∃û ∈ GT (cons) : uσ ≈ û) ; ∀L in C : ∀u, v : (L = (u≠v) ⇒ uσ ≉ vσ) ; lσ ≉ rσ . Now, by asking for the “reasons” of the ‘≉’, there is a J with J ⊆ I ; ∀L in C : ∀u, v : (L = (u≠v) ⇒ ∃j_{L} ∈ J : uσ ≁_{j_{L}} vσ) ; ∃j_{(l,r)} ∈ J : lσ ≁_{j_{(l,r)}} rσ ; and |J| ≤ |{ L in C | ∃u, v : L = (u≠v) }| + 1 . Define ≡ := ⋂_{j∈J} ∼_{j} . As ≈ ⊆ ≡ , ≡ yields no model of R for the same “reason” as ≈. But (as J finite) { ∼_{j} | j ∈ J } has a ⊆-minimal^{91} element ∼_{j_{0}} with j_{0} ∈ J . Now ≡ = ∼_{j_{0}}. Hence ∼_{j_{0}} yields no sig/cons-model of R, which is a contradiction.

3. By (1 ) and (2 ).

90We tacitly use the Substitution-Lemma(4.2) again, just the way we used it at the end of (1) in the proof of Lemma 5.

91and minimum

Proof of Correctness of Definition 6 Let ⟶ be the intersection of all relations satisfying the requirement of Definition 6. We claim the following:

1. ⟶_{R,X,ω} is the minimum of all relations satisfying the requirement of Definition 6 with the additional restriction of l ∈ T (cons, V_{SIG}⊎V_{CONS}) .

2. ∀s ∈ T (cons, V_{SIG}⊎V_{CONS}) : ∀t : (s⟶^{∗}_{R,X,ω}t ⇒ t ∈ T (cons, V_{SIG}⊎V_{CONS}))

3. ∀i ∈ N : ∀n ∈ N : (⟶^{n}_{R,X,ω+i} ∩ (T (cons, V_{SIG}⊎V_{CONS}) × T )) ⊆ ⟶^{n}_{R,X,ω}

4. ∀i ∈ N : ⟶_{R,X,ω+i} ⊆ ⟶_{R,X,ω+i+1}

5. ⟶_{R,X} satisfies the requirement of Definition 6; i.e. ⟶ ⊆ ⟶_{R,X}.

6. ⟶_{R,X,ω} ⊆ ⟶

7. (⟶∩(T (cons, V_{SIG}⊎V_{CONS}) × T )) ⊆ ⟶_{R,X,ω}

8. ∀i ∈ N : ⟶_{R,X,ω+i} ⊆ ⟶

9. ⟶_{R,X} is the minimum of all relations which satisfy the requirement of Definition 6. To the proofs of these claims:

1. By the restriction on the rules of Definition 6, ⟶_{R,X,ω} is just the standard closure over a finitary relation.

2. By the restriction on the rules of Definition 6.

3. By induction on i using (1), (2), and the restriction on the rules of Definition 6.

4. By induction on i using (3) and the restriction on the rules of Definition 6.

5. By (4), taking ⟶_{R,X,ω+i+1} on the left-hand side of the requirement for the maximum i of all ⟶_{R,X,ω+i} occurring positively (i.e. not in a ∤↓-statement) on the right-hand side of the requirement.

6. By (1), ⟶_{R,X,ω} is the intersection of a superset of the set whose intersection is ⟶.

7. By (3) and (5).

8. \underline{i = 0:} By (6). \underline{i ⇒ (i + 1):} By (6), (7), and (2).

9. By (5) and (8). Q.e.d. (Correctness Proof for Definition 6)

Proof of Lemma 6 By (9), (3), and (2) in the correctness proof for Definition 6 above. Q.e.d. (Lemma 6)

Proof of Lemma 6 By the restriction on the rules of Definition 6 and induction over i one gets ∀i ∈ N : ∀n ∈ N : ∀s ∈ T (cons, V_{CONS}) : ∀t : ( s⟶^{n}_{R,X,i}t ⇒ t ∈ T (cons, V_{CONS}) ) . By Lemma 6 this is sufficient. \underline{Q.e.d. (Lemma 6)}

Proof of Lemma 6 By the restriction on the rules of Definition 6 and induction over i one gets

∀i ∈ N : ∀n ∈ N : ∀s ∈ GT (cons) : ∀t : ( s⟶^{n}_{R,X,i}t ⇒ t ∈ GT (cons) ) .

By Lemma 6 this is sufficient. \underline{Q.e.d. (Lemma 6)}

Proof of Lemma 6 By Lemma 6. \underline{Q.e.d. (Lemma 6)}

Proof of Lemma 6 By (4), (9) in the correctness proof above we get ⟶_{R,X,β} ⊆ ⟶_{R,X,γ} ⊆ ⟶ . A literal L in C (being fulfilled w.r.t. ⟶_{R,X,β}) must have one of the following forms: If L = (u=v) , then by u↓_{R,X,β}v we get u↓_{R,X,γ}v . If L = (Def u) , then there is some û ∈ GT (cons) with u⟶^{∗}_{R,X,β} û and we get u⟶^{∗}_{R,X,γ} û . If L = (u≠v) , then there are û, v̂ ∈ GT (cons) with

u⟶^{∗}_{R,X,β} û∤↓_{R,X,β} v̂⟵^{∗}_{R,X,β}v and by ω ⪯ β we get u⟶^{∗}_{R,X,γ} û∤↓_{R,X,ω} v̂⟵^{∗}_{R,X,γ}v and finally by

Lemma 6 u⟶^{∗}_{R,X,γ} û∤↓_{R,X,γ} v̂⟵^{∗}_{R,X,γ}v . \underline{Q.e.d. (Lemma 6)}

Proof of Lemma 6 The ‘if’-part of the proof is trivial. The ‘only if’-part is straightforward as follows: If u ↓ v, then by confluence (below v) u⟶^{∗}NF(v) and then by confluence (below u) NF(u) = NF(v). If u⟶^{∗}û ∈ GT (cons) then by confluence û⟶^{∗}NF(u) and then by Lemma 6 NF(u) ∈ GT (cons). If û, v̂ ∈ GT (cons) and u⟶^{∗}û∤↓v̂⟵^{∗}v then by confluence NF(u)⟵^{∗}û∤↓v̂⟶^{∗}NF(v); hence NF(u) ≠ NF(v) and by Lemma 6 NF(u), NF(v) ∈ GT (cons). \underline{Q.e.d. (Lemma 6)}

Proof of Lemma 6 By the Axiom of Choice there is some τ ∈ SUB(Y, T (X))with τX ⊆ id .Usingthisτ in combination with Corollary 6 for getting rid of variables from Y\X (introduced by extravariables), the first sentence is trivial by induction on β. The rest then follows immediately from Corollary 6. \underline{Q.e.d. (Lemma 6)}

Proof of Theorem 6 Let A := T (X)/⟷^{∗}_{R,X} . Let I := GT /⟷^{∗}_{R,∅} . \underline{Claim 1}: If C is a sig/cons-model of R; μ ∈ SUB(X, C); then

∀β ⪯ ω : ∀s ∈ 𝕊 : ⟶_{R,X,β} ∩ (T_{SIG,s}×T_{SIG,s}) ⊆ ker(C_{μ})_{s} .

The proof of Claim 1 is omitted because it reads just like the proof of Claim 2 until it comes to β ≻ ω . \underline{Proof of (1.):} By the Axiom of Choice, each element of SUB(V, A) can be written σ ∘ A_{κ} for some σ ∈ SUB(V, T (X)).T hus(bytheSubstitution − Lemma(4.2)and X⊆V_{SIG} ), forA beingasig/cons−model ofR itissufficienttonotethat(byconfluenceof⟶_{R,X}[∩(D_{X}×D_{X})], the fact that R is a Def-MCRS, and Lemma 6) for ((l, r), C)∈ R; σ ∈ SUB(V, T (X)) :

Cσ is fulfilled w.r.t. ⟶_{R,X} iff

∀u, v ∈ T : ( \begin{matrix}( ( (u=v ) in Cσ) ⇒ & u⟷^{∗}_{R,X}v ) & ∧ \\ ( ( (Def u) in Cσ) ⇒ & ∃û ∈ GT (cons) : u⟷^{∗}_{R,X} û ) & ∧ \\ ( ( (u≠v ) in Cσ) ⇒ & u↚→^{∗}_{R,X}v ) \end{matrix} )

For the proof of A being a constructor-minimum model, suppose C to be a sig/cons-model of R. We have to find a cons-homomorphism from Aℂ ⊎ ({CONS}× 𝕊) to Cℂ ⊎ ({CONS}× 𝕊) . Let B be the ground term algebra over cons. There is a cons-homomorphism h::Aℂ ⊎ ({CONS}× 𝕊)→(B/(⟷^{∗}_{R,X} ∩ (T (cons, V_{CONS})×T (cons, V_{CONS})))) given by (s∈ 𝕊; A ∈ A(CONS, s)) : A ↦ T (cons, V_{CONS}) ∩ A .T husweonlyhavetofindacons −

homomorphismfrom B/(⟷^{∗}_{R,X} ∩ (T (cons, V_{CONS})×T (cons, V_{CONS}))) to Cℂ ⊎ ({CONS}× 𝕊) .Letμ

be a C-valuation of X (which always exists by the Axiom of Choice). Using the Homomorphism-Theorem (the usual one for cons-homomorphisms, not ours) all we have to show is ∀s ∈ 𝕊 : ⟷^{∗}_{R,X} ∩ (T_{CONS,s}×T_{CONS,s}) ⊆ ker(C_{μ})_{s} , which by confluence of ⟶_{R,X}[∩(D_{X}×D_{X})] is the same as ∀s ∈ 𝕊 : ↓_{R,X} ∩ (T_{CONS,s}×T_{CONS,s}) ⊆ ker(C_{μ})_{s} . Because of Lemma 6, ∀s ∈ 𝕊 : ⟶_{R,X,ω} ∩ (T_{CONS,s}×T_{CONS,s}) ⊆ ker(C_{μ})_{s} is sufficient for this. But this is implied by Claim 1. \underline{Q.e.d. (1.)} \underline{Claim 2:} If C∈ K; μ ∈ SUB(X, C);⟶_{R,∅}[∩(D_{∅}×D_{∅})] is confluent; then

∀β ⪯ ω+ω : ∀s ∈ 𝕊 : ⟶_{R,X,β} ∩ (T_{SIG,s}×T_{SIG,s}) ⊆ ker(C_{μ})_{s} .

\underline{Proof of Claim 2:} For the limit ordinals 0, ω, ω+ω the induction step is trivial. For a non-limit ordinal β+1 the induction step is as follows: Suppose s⟶_{R,X,β+1}t. If ω ⪯

βands⟶_{R,X,ω}t, thenwealreadyhave C_{μ}(s) = C_{μ}(t) .Otherwisethereare ((l, r), C) ∈ R ; σ ∈ SUB(V, T (X)) ; p ∈ s; with s/p = lσ ; t = s[ p ← rσ] ; and Cσ fulfilledw.r.t. ⟶_{R,X,β}.AsC isasig/cons−

model ofR, for C_{μ}(s) = C_{μ}(t) (bytheSubstitution−Lemma(4.2))weonlyhavetoshowthatthecondition Cσ istruew.r.t. C_{μ}.T hreecasesforLinCσ: If L = (u=v), by u ↓_{R,X,β} v the induction hypothesis implies C_{μ}(u) = C_{μ}(v) . If L = (Def u) with u ∈ T_{SIG,s′}, by the existence of some û ∈

GT_{CONS,s′}withu⟶^{∗}_{R,X,β} ûtheinductionhypothesisimpliesC_{μ}(u) = C_{μ}(û) ∈ C(CONS, s′).

If L = (u≠v), by the existence of some û, v̂ ∈ GT (cons) with u⟶^{∗}_{R,X,β} û∤↓_{R,X,β} v̂⟵^{∗}_{R,X,β}v the induction hypothesis implies C_{μ}(u) = C_{μ}(û) = C(û) and C(v̂) = C_{μ}(v̂) = C_{μ}(v) . Thus, for C_{μ}(u) ≠ C_{μ}(v) it is sufficient to show C(û) ≠ C(v̂) . By ω ⪯ βandLemma 6weknowthat û∤↓_{R,X} v̂; thenbyLemma 6 û∤↓_{R,∅} v̂; andtherefore(byconfluenceof⟶_{R,∅}[∩(D_{∅}×D_{∅})])

û↚→^{∗}_{R,∅} v̂ . Because of (1) (for X:=∅), C mustbenotonlyaconstructor −

minimalmodelbutalsoaconstructor−minimummodelofR.Hence C(û) ≠ C(v̂) simplybecause û, v̂ ∈ GT (cons) ; I(û) ≠ I(v̂) ; andI is(by(1))asig/cons− model ofR. \underline{Q.e.d. (Claim 2)} \underline{Claim 3 :}If⟶_{R,∅}[∩(D_{∅}×D_{∅})] is confluent, then A is free for K over X w.r.t. κ. \underline{Proof of Claim 3:} Suppose C∈ Kandμ to be a C-valuation of X. The uniqueness of the required sig/cons-homomorphism h::A→C with μ = κh is trivial. For its existence (by the Homomorphism-Theorem(4.2)) we only have to show

∀s ∈ 𝕊 : ⟷^{∗}_{R,X} ∩ (T_{SIG,s}×T_{SIG,s}) ⊆ ker(C_{μ})_{s} ,

which is implied by Claim 2. \underline{Q.e.d. (Claim 3)} \underline{Claim 4:} If ⟶_{R,X}[∩(D_{X}×D_{X})] is confluent, then ⟶_{R,∅}[∩(D_{∅}×D_{∅})] is confluent, too. \underline{Proof of Claim 4:} Trivial by Lemma 6. \underline{Q.e.d. (Claim 4)} \underline{Proof of (2.):} By (1) and the claims 4 and 3. \underline{Proof of (3.):} Suppose C to be a sig/cons-model of R with C ≲_{H}A . By (1) we get C ∈ K , and then by (2) A ≲_{H}C .

Proof of Theorem 6 First note that the remark of footnote 45 is respected during the whole proof. \underline{\underline{Claim 1:}} ∀i ∈ N: ∀n ∈ N: ∀s ∈ T (cons, X): ∀t:

(s⟶^{n}_{R′,X′,i}t ⇒ (s⟶^{n}_{R,X,i}t ∈ T (cons, X)))

\underline{\underline{Claim 2:}} ∀β ⪯ ω+ω : ⟶_{R,X,β} ⊆ ⟶_{R′,X′,β}

Claim 2 and Claim 1 (using Lemma 6 and T (cons, V_{SIG}⊎V_{CONS}) ⊆ T (cons′, V′_{SIG}⊎V′_{CONS})) imply (1 ); and Claim 2 implies (2 ) and (3 ).

\underline{\underline{Proof of Claim 1:}} \underline{i = 0:} ⟶_{R′,X′,0} = ∅ . \underline{i ⇒ (i + 1):} \underline{n = 0:} Trivial.

\underline{n ⇒ (n + 1):} Suppose s⟶^{n}_{R′,X′,i+1}s′⟶_{R′,X′,i+1}t . By induction hypothesis in n we know s⟶^{n}_{R,X,i+1}s′ ∈ T (cons, X) . By ($) there must be some l ∈ T (cons, V_{SIG}⊎V_{CONS}) ; ((l, r), C) ∈ R ; σ ∈ SUB(V(l), T ) ; p ∈ s′ with s′/p = lσ ; t = s′[ p ← rσ] ; Cσ fulfilled w.r.t. ⟶_{R′,X′,i}; ran(σ) ⊆ T (cons, X) . By the structure of constructor equations we have no inequality literal in Cσ. For (u=v) in Cσ we have u, v ∈ T (cons, X) and u↓_{R′,X′,i}v and therefore by induction hypothesis in i: u↓_{R,X,i}v . For (Def u) in Cσ we have u ∈ T (cons, X) and u⟶^{∗}_{R′,X′,i} û for some û ∈ GT (cons′) and hence by induction hypothesis in i: u⟶^{∗}_{R,X,i} û ∈ (T (cons, X) ∩ GT (cons′)) = GT (cons) . Thus, finally we conclude that Cσ is fulfilled w.r.t. ⟶_{R,X,i}, i.e. s′⟶_{R,X,i+1}t ∈ T (cons, X) . \underline{\underline{Q.e.d. (Claim 1)}} \underline{\underline{Proof of Claim 2:}} The induction step for the limit ordinals 0, ω, and ω + ω is trivial. For a non-limit ordinal β + 1 the induction step is as follows: Suppose s⟶_{R,X,β+1}t . In the case of ω ⪯ β this may be due to s⟶_{R,X,ω}t ; but then by induction hypothesis we succeed by ⟶_{R,X,ω} ⊆ ⟶_{R′,X′,ω} ⊆ ⟶_{R′,X′,β+1} . Otherwise there must be some ((l, r), C) ∈ R ; σ ∈ SUB(V, T ) ; p ∈ s with s/p = lσ ; t = s[ p ← rσ] ; Cσ fulfilled w.r.t. ⟶_{R,X,β} . The only thing to be shown is: Cσ fulfilled w.r.t. ⟶_{R′,X′,β} . For (u=v) in Cσ we have u↓_{R,X,β}v and therefore by induction hypothesis u↓_{R′,X′,β}v . For (Def u) in Cσ we have u⟶^{∗}_{R,X,β} û for some û ∈ GT (cons) and therefore by induction hypothesis u⟶^{∗}_{R′,X′,β} û . For (u≠v) in Cσ we have u⟶^{∗}_{R,X,β} û∤↓_{R,X,β} v̂⟵^{∗}_{R,X,β}v for some û, v̂ ∈ GT (\underline{\underline{cons}}) and ω ⪯ β . We get û∤↓_{R,X,ω} v̂ , and then (by Claim 1) û∤↓_{R′,X′,ω} v̂ and (by Lemma 6) û∤↓_{R′,X′} v̂ . Finally, by

induction hypothesis we get u⟶^{∗}_{R′,X′,β} û∤↓_{R′,X′,β} v̂⟵^{∗}_{R′,X′,β}v .

Proof of Lemma 7 For (((t_{0}, t_{1}), D), t̂, p) ∈ CP(R) there are ((l_{k}, r_{k}), C_{k}) ∈ R ; k < 2 ; ξ, σ ∈ SUB(V, T ) with l_{0}ξσ = l_{1}σ/p ; ((t_{0}, t_{1}), D) = ((l_{1}[ p ← r_{0}ξ], r_{1}), C_{0}ξ C_{1})σ. Let φ ∈ SUB(V, T (X)) and assume Dφ to be fulfilled. Then C_{0}ξσφ and C_{1}σφ are fulfilled, too. Therefore: t_{0}φ = l_{1}σφ[ p ← r_{0}ξσφ] ⟵ l_{1}σφ ⟶ r_{1}σφ = t_{1}φ and by confluence we have t_{0}φ ↓ t_{1}φ . Q.e.d. (Lemma 7)

Proof of Lemma 7 \underline{(1 ):} For p = ∅ the definition of “quasi overlay joinable” reads:

∀φ ∈ SUB(V, T (X)) : ( Dφ fulfilled ⇒ t_{0}φ ↓ t_{1}φ⟵^{+}t̂φ)

As we assume (((t_{0}, t_{1}), D), t̂, ∅) to be joinable, we now only have to show t_{1}φ⟵^{+}t̂φ under the assumption of Dφ being fulfilled. There are ((l_{k}, r_{k}), C_{k}) ∈ R ; k < 2 ; ξ, σ ∈ SUB(V, T ) with (((…, t_{1}), D), t̂) = (((…, r_{1}), C_{0}ξ C_{1}), l_{1})σ. Since C_{1}σφ is fulfilled, we have t_{1}φ = r_{1}σφ⟵l_{1}σφ = t̂φ. \underline{(2 ):} If Dφ is fulfilled, then we get by quasi overlay joinability and Corollary 6:

t_{0}φ = t_{0}φ[ p ← t_{0}φ/p] ↓ t_{0}φ[ p ← t_{1}φ/p] = t_{1}φ .

Proof of Theorem 7

For the proof of Sub-claim 3 below, we enrich the signatures by a new sort s_{new} and new constructor symbols eqs̄ for each old sort s̄ ∈ 𝕊 with arity s̄s̄ → s_{new} and ⊥ with arity s_{new}. We take (in addition to R) the following set of new rules (with xs̄ ∈ V_{SIG,s̄}fors̄ ∈ 𝕊) :

R’ := { eqs̄ xs̄ xs̄ = ⊥ | s̄ ∈ 𝕊 }

Sincethesortrestrictionsdonotallow⟶_{R∪R′,X,β}tomakeanyuseoftermsofthesorts_{new} when

rewriting terms of an “old” sort, we get

∀β ⪯ ω+ω : ⟶_{R∪R′,X,β} ∩ (T (sig, X)×T (sig, X)) = ⟶_{R,X,β/sig/cons}

(the latter being defined over the non-enriched signatures). Therefore (as no new critical peaks occur) the critical peaks keep being quasi overlay joinable. We are going to show confluence of ⟶_{R∪R′,X}, which implies confluence of ⟶_{R,X/sig/cons}. We know that ⟶_{R∪R′,X} is noetherian on each “old” sort; and by this we also know ⟶_{R∪R′,X} to be noetherian on s_{new} because ⊥ is irreducible and terms of the form ‘eqs̄ u v’ allow at most one reduction step via ⟶_{R∪R′,X} \ ⟶_{R,X/sig′/cons′} .

We define ⟶_{0} := ⟶_{R′,X} ; ⟶_{β} := ⟶_{R∪R′,X,β} for any ordinal β with 0 ≺ β ≺ ω + ω (where ≺ is the ordering of ordinal numbers); and ⟶ := ⟶_{ω+ω} := ⟶_{R∪R′,X} .

For v, u, s, t ∈ T with v⟵^{∗}u and s⟶^{∗}t ; Π ⊆ u with

∀p, q ∈ Π : (p ≠ q ⇒ p ∥ q) and ∀o ∈ Π : u/o = s ; we say that P (v, u, s, t, Π) holds if v ↓ u[ o ← t | o ∈ Π] . Now (by Π := {∅}) it suffices to show that P (v, u, s, t, Π) holds for all appropriate v, u, s, t, Π. We will show this by noetherian induction over the lexicographic combination of the following orderings:

1. (⟶ ∪ ▷_{ST})^{⊕}  (Cf. Lemma 8.1)
2. ≻
3. ≻

using the following measure on (v, u, s, t, Π):

1. s
2. the smallest ordinal β ⪯ ω+ω for which v⟵^{∗}_{β}u
3. the smallest n ∈ N for which v⟵^{n}_{β}u for the β of (2)

For the limit ordinals 0, ω, ω+ω in the second position of the measure, the induction step

is trivial (⟵^{∗}_{0} ⊆ ⟵_{0} ∪ id; ⟵^{∗}_{ω} ⊆ ⋃_{i∈N_{+}} ⟵^{∗}_{i}; ⟵^{∗}_{ω+ω} ⊆ ⋃_{i∈N} ⟵^{∗}_{ω+i}). Thus, as we now

suppose a smallest (v, u, s, t, Π) with P (v, u, s, t, Π) not holding for, the second position of the measure must be a non-limit ordinal β+1.

As P (v, u, s, t, Π) holds trivially for u = v or s = t we have some u′, s′ with

v⟵^{n}_{β+1}u′⟵_{β+1}u (n ∈ N) (with ∀m ∈ N : (v⟵^{m}_{β+1}u ⇒ m >

n))and s⟶s′⟶^{∗}t .Nowforacontradictionitissufficienttoshow

\underline{\underline{Claim:}} There is some z with v⟶^{∗}z⟵^{∗}u[ o ← s′ | o ∈ Π].

because then we have z ↓ u[ o ← t | o ∈ Π] by P (z, u[ o ← s′ | o ∈ Π], s′, t, Π), which is smaller than (v, u, s, t, Π) in the first position of the measure by s⟶s′.

If we had s⟶s′ by some redex below the top of s, then Claim would hold by induction hypothesis with P (…) being smaller in the first position using ▷_{ST}. Thus, there are some ((l_{0}, r_{0}), C_{0}) ∈ R ∪ R′; μ_{0} ∈ SUB(V, T (X)); with s = l_{0}μ_{0}; s′ = r_{0}μ_{0}; C_{0}μ_{0} fulfilled w.r.t. ⟶. Furthermore, we have some q ∈ u; ((l_{1}, r_{1}), C_{1}) ∈ R ∪ R′; μ_{1} ∈ SUB(V, T (X)); withu/q=l_{1}μ_{1}; u′ = u[ q ← r_{1}μ_{1} ]; C_{1}μ_{1} fulfilled w.r.t. ⟶_{β}.

We now distinguish two cases by the relative position of q and Π:

\underline{\underline{“q not strictly below any p ∈ Π”:}} There is no p′ with pp′ = q, p′ ≠ ∅, and p ∈ Π Define Π′ := { p | qp ∈ Π }. \underline{The critical peak case:} There is some p ∈ Π′ ∩ l_{1} with l_{1}/p ∉ V . Let ξ := min Sep(V(((l_{0}, r_{0}), C_{0})), V(((l_{1}, r_{1}), C_{1}))) . Let ϱ be given by (x∈ V) :xϱ :=

\begin{cases}xμ_{1} & if x ∈ V(((l_{1}, r_{1}), C_{1})) \\ xξ^{−1}μ_{0} & otherwise \end{cases}\}. By l_{0}ξϱ = l_{0}ξξ^{−1}μ_{0} = s = u/qp = l_{1}μ_{1}/p = (l_{1}/p)ϱ let

Y:=V(((l_{0}, r_{0}), C_{0})ξ, ((l_{1}, r_{1}), C_{1})), σ := min Mgu(⟨(l_{0}ξ, l_{1}/p)⟩, Y)andφ ∈ SUB(V, T (X)) with σφY = ϱY . Let (((t_{0}, t_{1}), D), t̂) := (((l_{1}[ p ← r_{0}ξ], r_{1}), C_{0}ξ C_{1}), l_{1})σ . Now we have (((t_{0}, t_{1}), D), t̂)φ = (((l_{1}μ_{1}[ p ← r_{0}μ_{0} ], r_{1}μ_{1}), C_{0}μ_{0} C_{1}μ_{1}), l_{1}μ_{1}). Therefore Dφ is fulfilled.

\underline{Sub-claim 1:} There is some w with s⟶^{+}r_{1}μ_{1}/p⟶^{∗}w⟵^{∗}s′ and r_{1}μ_{1} = l_{1}μ_{1}[ p ← r_{1}μ_{1}/p] .

\underline{Proof of Sub-claim 1}: If t_{0} = t_{1}, then s⟶s′ = r_{0}μ_{0} = t_{0}φ/p = t_{1}φ/p = r_{1}μ_{1}/p; and r_{1}μ_{1} = r_{1}μ_{1}[ p ← r_{1}μ_{1}/p] = t_{1}φ[ p ← r_{1}μ_{1}/p] = t_{0}φ[ p ← r_{1}μ_{1}/p] = l_{1}μ_{1}[ p ← r_{1}μ_{1}/p]. Otherwise, if t_{0} ≠ t_{1}, (((t_{0}, t_{1}), D), t̂, p) is a critical peak and we get s = u/qp = l_{1}μ_{1}/p =

t̂φ/p⟶^{+}t_{1}φ/p ↓ (t_{0}/p)φ = r_{0}μ_{0} = s′ where t_{1}φ/p = r_{1}μ_{1}/p; and

r_{1}μ_{1} = t_{1}φ = t_{0}φ[ p ← t_{1}φ/p] = l_{1}μ_{1}[ p ← r_{1}μ_{1}/p]. \underline{Q.e.d. (Sub-claim 1)} \underline{Sub-claim 2:} For o ∈ Π \ \{qp\} we have u′/o = s . \underline{Proof of Sub-claim 2:} If there is some p′ with o = qp′, then by Sub-claim 1: u′/o = u′/qp′ = r_{1}μ_{1}/p′ = l_{1}μ_{1}[ p ← …]/p′ = l_{1}μ_{1}/p′ = u/qp′ = u/o = s. Otherwise, by qp ∈ Π we know o ∥ q, and therefore u′/o = u/o = s. \underline{Q.e.d. (Sub-claim 2)} By Sub-claim 1 we get u′[ qp ← w] = u[ q ← r_{1}μ_{1}[ p ← w] ] = u[ q ← l_{1}μ_{1}[ p ← w] ] = u[ qp ← w]. Hence, for û := u′[ qp ← w][ o ← s′ | o ∈ Π \ {qp}] we get û =

u[ qp ← w][ o ← s′ | o ∈ Π \ {qp}]⟵^{∗}u[ o ← s′ | o ∈ Π] by w⟵^{∗}s′ (by Sub-claim 1).

Thus, for Claim we only have to show v ↓ û. For u′′ := u′[ o ← s′ | o ∈ Π \{qp}] (cf. Subclaim 2) there is some w′ with v⟶^{∗}w′⟵^{∗}u′′ by Sub-claim 2 and P (v, u′, s, s′, Π \ {qp}), which is smaller in the second or third position. Finally, we get w′ ↓ û by u′′/qp = u′/qp = r_{1}μ_{1}/p, Sub-claim 1, and P (w′, u′′, r_{1}μ_{1}/p, w, {qp}), which is smaller in the first position by Sub-claim 1. \underline{Q.e.d. (The critical peak case)} \underline{The variable overlap (if any) case:} ∀p ∈ Π′ ∩ l_{1} : l_{1}/p ∈ V Define Γ : V → 𝔓_{N}([T ]) by (x ∈ V): Γ (x) := { p′ | ∃p : (l_{1}/p = x ∧ pp′ ∈ Π′) } . Define μ′_{1} by (x ∈ V): xμ′_{1} := xμ_{1}[ p′ ← s′ | p′ ∈ Γ (x) ] . Define û := u[ q ← r_{1}μ′_{1} ][ o ← s′ | o ∈ Π \ (qΠ′) ] and ǔ := u[ q ← l_{1}μ′_{1} ][ o ← s′ | o ∈ Π \ (qΠ′) ] . We are going to show v ↓ û⟵ǔ⟵^{∗}u[ o ← s′ | o ∈ Π] for Claim. Since for p′ ∈ Γ (x) we always have some p with l_{1}/p = x; xμ_{1}/p′ = l_{1}μ_{1}/pp′ = u/qpp′ = s⟶s′; we get v ↓ û by P (v, u′, s, s′, (Π \ (qΠ′)) ∪ { qpp′ | ∃x : (r_{1}/p = x ∧ p′ ∈ Γ (x)) }), which is smaller in the second or third position. We get û⟵ǔ by \underline{Sub-claim 3:} C_{1}μ′_{1} is fulfilled.

Finally, ǔ⟵^{∗}u[ q ← l_{1}μ_{1}[ o ← s′ | o ∈ Π′] ][ o ← s′ | o ∈ Π \ (qΠ′) ] = u[ o ← s′ | o ∈ Π].

\underline{Proof of Sub-claim 3:} For (ū=v̄) in C_{1} we have ūμ_{1}↓_{β} v̄μ_{1} and hence for the sort s̄ of

ū: ⊥⟵^{+}_{β}(eqs̄ ū v̄)μ_{1}. We get ⊥ ↓ (eqs̄ ū v̄)μ′_{1} by P (⊥, (eqs̄ ū v̄)μ_{1}, s, s′ , { pp′ | ∃x :

((eqs̄ ū v̄)/p = x ∧ p′ ∈ Γ (x)) }), which is smaller in the second position. Since there are no rules for ⊥ and only one for eqs̄, this means ūμ′_{1} ↓ v̄μ′_{1}. For (Def ū) in C_{1} we know the existence of some ū ∈ GT (cons) with ū⟵^{∗}_{β} ūμ_{1}. We get some ˆ ū with ū⟶^{∗}ˆū⟵^{∗}ūμ′_{1} by P (ū, ūμ_{1}, s, s′, { pp′ | ∃x : (ū/p = x ∧ p′ ∈ Γ (x)) }), which is smaller in the second position. By Lemma 6 we get ˆ ū ∈ GT (cons). Finally, for (ū≠v̄) in C_{1} we have some ū, v̄ ∈ GT (cons) with ūμ_{1}⟶^{∗}_{β} ū∤↓v̄⟵^{∗}_{β} v̄μ_{1}. By applying the same procedure as before

twice we get ˆ ū, ˆ v̄ ∈ GT (cons) with ūμ′_{1}⟶^{∗}ˆū⟵^{∗}ū∤↓v̄⟶^{∗}ˆv̄⟵^{∗}v̄μ′_{1}, i.e. ūμ′_{1}⟶^{∗}ˆū∤↓ˆv̄⟵^{∗}v̄μ′_{1}.

Q.e.d. (Sub-claim 3; The variable overlap (if any) case; “q not strictly below any p ∈ Π”)

\underline{\underline{“q strictly below p ∈ Π”:}} There is some p′ with pp′ = q, p′ ≠ ∅, and p ∈ Π \underline{Sub-claim 4:} For o ∈ Π \ \{p\} we have u′/o = s = l_{0}μ_{0} . \underline{Proof of Sub-claim 4:} Since o ∥ p, we have u′/o = u[ pp′ ← …]/o = u/o = s = l_{0}μ_{0}. Q.e.d. (Sub-claim 4) \underline{The (second) critical peak case:} p′ ∈ l_{0} ∧ l_{0}/p′ ∉ V Let ξ := min Sep(V(((l_{1}, r_{1}), C_{1})), V(((l_{0}, r_{0}), C_{0}))) . Let ϱ be given by (x ∈ V): xϱ :=

\begin{cases}xμ_{0} & if x ∈ V(((l_{0}, r_{0}), C_{0})) \\ xξ^{−1}μ_{1} & otherwise \end{cases}\}. By l_{1}ξϱ = l_{1}ξξ^{−1}μ_{1} = u/q = u/pp′ = l_{0}μ_{0}/p′ =

(l_{0}/p′)ϱletY := V(((l_{1}, r_{1}), C_{1})ξ, ((l_{0}, r_{0}), C_{0})), σ := min Mgu(⟨(l_{1}ξ, l_{0}/p′)⟩, Y)andφ ∈ SUB(V, T (X)) with σφY = ϱY . Let (((t_{0}, t_{1}), D), t̂) := (((l_{0}[ p′ ← r_{1}ξ], r_{0}), C_{1}ξ C_{0}), l_{0})σ . Now we have (((t_{0}, t_{1}), D), t̂)φ = (((l_{0}μ_{0}[ p′ ← r_{1}μ_{1} ], r_{0}μ_{0}), C_{1}μ_{1} C_{0}μ_{0}), l_{0}μ_{0}). Therefore Dφ is fulfilled. \underline{Sub-claim 5:} There is some w with s⟶s[ p′ ← r_{1}μ_{1} ]⟶^{∗}w⟵^{∗}s′ . \underline{Proof of Sub-claim 5}: Since s/p′ = u/pp′ = u/q = l_{1}μ_{1} we have s⟶s[ p′ ← r_{1}μ_{1} ]. Because s[ p′ ← r_{1}μ_{1} ] = l_{0}μ_{0}[ p′ ← r_{1}μ_{1} ] = t_{0}φ and t_{1}φ = r_{0}μ_{0} = s′ we now only have to show t_{0}φ ↓ t_{1}φ. If t_{0} = t_{1}, this is trivial. Otherwise, if t_{0} ≠ t_{1}, (((t_{0}, t_{1}), D), t̂, p′) is a critical peak and we get t_{0}φ ↓ t_{1}φ by Lemma 7. \underline{Q.e.d. (Sub-claim 5)}

For û := u[ p ← w][ o ← s′ | o ∈ Π \ {p}] we get û⟵^{∗}u[ o ← s′ | o ∈ Π]

by w⟵^{∗}s′ (by Sub-claim 5). Thus, for Claim we only have to show v ↓ û. For u′′ := u′[ o ← s′ | o ∈ Π \{p}] (Cf. Sub-claim 4) there is some w′ with v⟶^{∗}w′⟵^{∗}u′′ by Sub-claim 4 and P (v, u′, s, s′, Π \ {p}), which is smaller in the second or third position. Finally, we get w′ ↓ û by u′′/p = u′/p = u[ pp′ ← r_{1}μ_{1} ]/p = u/p[ p′ ← r_{1}μ_{1} ] = s[ p′ ← r_{1}μ_{1} ], Sub-claim 5, and P (w′, u′′, s[ p′ ← r_{1}μ_{1} ], w, {p}), which is smaller in the first position by Sub-claim 5. Q.e.d. (The (second) critical peak case) \underline{The (second) variable overlap case:} There are p̌, p̂, x with p′ = p̌p̂ and l_{0}/p̌ = x ∈ V

Define μ′_{0} by (y ∈ V): yμ′_{0} := \{ \begin{matrix}xμ_{0}[ p̂ ← r_{1}μ_{1} ] & if y = x \\ yμ_{0} & otherwise \end{matrix} \} . Define û :=

u[ o ← r_{0}μ′_{0} | o ∈ Π] and ǔ := u[ o ← l_{0}μ′_{0} | o ∈ Π]. Since xμ_{0}/p̂= l_{0}μ_{0}/p̌p̂= s/p′= u/pp′= u/q =l_{1}μ_{1}⟶r_{1}μ_{1} and u′ =u[ pp̌p̂ ← r_{1}μ_{1} ]=u[ p ← l_{0}μ_{0}[ p̌ ← xμ′_{0} ] ][ o ← l_{0}μ_{0} | o ∈ Π \{p}] (by Sub-claim 4), we get some w with v⟶^{∗}w⟵^{∗}ǔ by P (v, u′, l_{1}μ_{1}, r_{1}μ_{1}, { oǒp̂ | o ∈ Π ∧ l_{0}/ǒ = x ∧ oǒ ≠ pp̌ }), which is smaller in the first position by

s▷_{ST}s/p′ = u/pp′ = u/q = l_{1}μ_{1}. Now by û ⟵^{∗} u[ o ← r_{0}μ_{0} | o ∈ Π] = u[ o ← s′ | o ∈ Π]

for Claim we only have to show w ↓ û. But this is given by Sub-claim 6 below and P (w, ǔ, l_{0}μ′_{0}, r_{0}μ′_{0}, Π), which is smaller in the first position of the measure by

s = l_{0}μ_{0} ⟶^{+} l_{0}μ′_{0}.

\underline{Sub-claim 6:} C_{0}μ′_{0} is fulfilled. \underline{Proof of Sub-claim 6:} For (ū=v̄) in C_{0} we have some w with ūμ_{0}⟶^{∗}w⟵^{∗}v̄μ_{0}. We get some

w′ with w⟶^{∗}w′⟵^{∗}ūμ′_{0} by P (w, ūμ_{0}, l_{1}μ_{1}, r_{1}μ_{1}, { op̂ | ū/o = x }), and then w′ ↓ v̄μ′_{0} by

P (w′, v̄μ_{0}, l_{1}μ_{1}, r_{1}μ_{1}, { op̂ | v̄/o = x }), which are smaller in the first position of the measure by s▷_{ST}l_{1}μ_{1} (shown above). For (Def ū) in C_{0} we know the existence of some ū ∈ GT (cons)

with ū⟵^{∗}ūμ_{0}. We get some ˆ ū with ū⟶^{∗}ˆū⟵^{∗}ūμ′_{0} by P (ū, ūμ_{0}, l_{1}μ_{1}, r_{1}μ_{1}, { op̂ | ū/o = x }),

which is smaller in the first position (as before). By Lemma 6 we get ˆ ū ∈ GT (cons). Finally, for (ū≠v̄) in C_{0} we have some ū, v̄ ∈ GT (cons) with ūμ_{0}⟶^{∗}ū∤↓v̄⟵^{∗}v̄μ_{0}. By applying the same procedure as before twice we get ˆ ū, ˆ v̄ ∈ GT (cons) with

ūμ′_{0}⟶^{∗}ˆū⟵^{∗}ū∤↓v̄⟶^{∗}ˆv̄⟵^{∗}v̄μ′_{0}, i.e. ūμ′_{0}⟶^{∗}ˆū∤↓ˆv̄⟵^{∗}v̄μ′_{0}.

Q.e.d. (Sub-claim 6) Q.e.d. (The (second) variable overlap case) Q.e.d. (“q strictly below p ∈ Π”) Q.e.d. (Proof of Theorem 7)

Proof of Theorem 7 \underline{Claim:} For β ⪯ ω+ω and s⟶^{∗}_{R,X,β}t we have A_{κ}(s) = A_{κ}(t). \underline{Proof of Claim:} By induction on β. By induction on the number of derivation steps, it suffices to do the proof for ⟶_{R,X,β} instead of ⟶^{∗}_{R,X,β}. If β is one of the limit ordinals 0, ω, ω+ω, the induction step is trivial. If β is a non-limit ordinal γ+1, the induction step is as follows: For s⟶_{R,X,γ+1}t, either s⟶_{R,X,ω}t and ω ⪯ γ, and then (by induction hypothesis) A_{κ}(s) = A_{κ}(t); or there is a substitution σ ∈ SUB(V, T (X)), a rule ((l, r), C) ∈ R, and a p ∈ t with s/p = lσ, t = s[ p ← rσ], and Cσ fulfilled w.r.t. ⟶_{R,X,γ}. Since A is a sig/consmodel of R, we only have to show that Cσ is true w.r.t. A_{κ}.F or(u=v)inCσ we have u↓_{R,X,γ}v and hence by induction hypothesis we have A_{κ}(u) = A_{κ}(v). For ū ∈ 𝕊, u ∈ T (sig, X)ū, (Def u) in Cσ there is some û ∈ GT_{CONS,ū} with u⟶^{∗}_{R,X,γ} û and hence by induction hypothesis we have A_{κ}(u) = A_{κ}(û) ∈ A(CONS, ū).F or(u≠v)inCσ we know ω ⪯ γ and there are û, v̂ ∈ GT (cons) with u⟶^{∗}_{R,X,γ} û∤↓_{R,X,γ} v̂⟵^{∗}_{R,X,γ}v and w.l.o.g. (since ⟶_{R,X}[∩(D_{X}×D_{X})] is noetherian and by Lemma 6) û, v̂ ∉ dom(⟶_{R,X}); thus, (since û and v̂ are of the same sort and unequal) we have by induction hypothesis: A_{κ}(u) = A_{κ}(û) ≠ A_{κ}(v̂) = A_{κ}(v).

Q.e.d. (Claim)

Now we show confluence for part (1) of the theorem. Suppose u⟵^{+}_{R,X}s⟶^{+}_{R,X}v. Since ⟶_{R,X} is noetherian, there are û, v̂ ∈ T (sig, X)\dom(⟶_{R,X}) with u⟶^{∗}_{R,X} û and v⟶^{∗}_{R,X} v̂. By Claim we have A_{κ}(û) = A_{κ}(u) = A_{κ}(s) = A_{κ}(v) = A_{κ}(v̂) and therefore û = v̂. Finally for the proof of part (2) of the theorem, in the above we can additionally assume s ∈ D_{X} and thus the existence of some t ∈ GT (cons)\dom(⟶_{R,X}) (since ⟶_{R,X}∩(D_{X}×D_{X}) is noetherian and by Lemma 6) with s⟷^{∗}_{R,X}t. Since ⟶_{R,X} ∩ (D_{X}×D_{X}) is noetherian we get û, v̂ like above. Then by Claim we have A_{κ}(û) = A_{κ}(u) = A_{κ}(s) = A_{κ}(t) and A_{κ}(v̂) = A_{κ}(v) = A_{κ}(s) = A_{κ}(t), i.e. û = t = v̂ .

Proof of Lemma 8 and Lemma 8 It is standard to encode a universal deterministic Turing machine with a finite set of leftlinear, non-overlapping rules. This can be done in the following way, where stop, left, right, nil, 0, ⊥ are constant symbols, s is a unary function symbol, cons and nth are binary, cmd, state are ternary, and T is sexary; and “ T l a r c s p ” encodes the Turing machine with

meaning  intended range
l being the tape to the left of the head  or cons s^{n} 0 list-of-integers
a being the symbol under the head  s^{n} 0
r being the tape to the right of the head  or cons s^{n} 0 list-of-integers
c being the next command to be executed stop or left or right or s^{n} 0
s being the next state to be in  s^{n} 0
p being the program  cons table-of-commands table-of-states

The rules are:

T l  a r  stop s p = ⊥
T nil  a r  left s p = T nil  0 cons a r cmd 0 s p state 0 s p p
T cons b l a r  left s p = T l  b cons a r cmd b s p state b s p p
T l  a nil  right s p = T cons a l 0 nil  cmd 0 s p state 0 s p p
T l  a cons b r right s p = T cons a l b r  cmd b s p state b s p p
T l  a r  0 s p = T l  0 r  cmd 0 s p state 0 s p p
T l  a r  s x s p = T l  s x r  cmd s x s p state s x s p p

with the following auxiliary functions:

nth 0 cons a l = a
nth s x cons a l = nth x l
cmd a s cons table-of-commands table-of-states = nth a nth s table-of-commands
state a s cons table-of-commands table-of-states = nth a nth s table-of-states

We use ⊥ instead of a reasonable output because we are interested in the halting problem only. We assume all function symbols so far to be constructor symbols.

From this system we are now going to construct our positive-conditional rule system by exchanging the recursive T-rules of the form “ T l a r c s p = T l′ a′ r′ c′ s′ p′ ” for rules of the form “ T l a r c s p = ⊥ ⟵ T l′ a′ r′ c′ s′ p′ = ⊥ ”.

Now the above Turing machine halts iff the ground term “ T l a r c s p ” is reducible. Therefore (the halting problem being not co-semi-decidable) the reducibility of ground terms cannot be co-semi-decidable.

For Lemma 8 we now add the following new rule:

foreverp l a r c s p = true ⟵ T l a r c s p ≠ ⊥, Def T l a r c s p, Def ⊥

Now “ foreverplarcsp ” is reducible iff the above Turing machine does not halt. Therefore the reducibility of ground terms cannot be semi-decidable.

Proof of Theorem 8 \underline{\underline{Proof of (1.):}} The function g that firstly tests whether its single argument s is in the enumerable set T (sig, X), secondly tries to compute f(s), and thirdly (if s ∈ T (sig, X) and f(s) is defined) is defined iff the test f(s) = s succeeds, is defined exactly on the irreducible terms from T (sig, X). \underline{\underline{Proof of (2.):}} \underline{Claim 1:} Let β ⪯ ω+ω. For all s ∈ T (sig, X) the fol. sets are enumerable:

\begin{matrix}Y_{β}(s) := \{ t | s⟶_{R,X,β}t \} \\ Z_{β}(s) := \{ t | s⟶^{∗}_{R,X,β}t \} \end{matrix}

If Claim 1 holds, we can enumerate Z_{ω+ω}(s) and simultaneously the irreducible terms from T (sig, X) until one term t occurs in both enumerations and we can return f(s) := t. \underline{Proof of Claim 1:} By induction on β. It suffices to show that Y_{β}(s) is enumerable for all s ∈ T (sig, X). The induction step for the limit ordinals 0, ω, ω+ω is trivial (Y_{0}(s) = ∅; Y_{ω}(s) = ⋃_{i≺ω} Y_{i}(s); Y_{ω+ω}(s) = ⋃_{i≺ω} Y_{ω+i}(s)). The induction step for the non-limit ordinals β+1 can be done the following way: For all rules ((l, r), C) ∈ R and all p ∈ s and all σ in the enumerable set SUB(V(((l, r), C)), T (X)) with s/p = lσ we test in an enumerative fashion whether Cσ is fulfilled w.r.t. ⟶_{R,X,β} and enumerate s[ p ← rσ] if the test succeeds. For ω ⪯ β we merge this enumeration with that of Y_{ω}(s). The test of “Cσ fulfilled w.r.t. ⟶_{R,X,β}” can be semi-decided the following way: For (u=v) in Cσ we test the enumerable set Z_{β}(u) ∩ Z_{β}(v) for non-emptiness. For (Def u) in Cσ we test the enumerable set Z_{β}(u) ∩ GT (cons) for non-emptiness. For (u≠v) in Cσ we test for the existence of û ∈ A(u) and v̂ ∈ A(v) with û ≠ v̂ (syntactically) for the enumerable sets A(w) := Z_{β}(w) ∩ (GT (cons) \ dom(⟶_{R,X})). This last test succeeds only if ∃û, v̂ ∈ GT (cons) : u⟶^{∗}_{R,X,β} û∤↓_{R,X,β} v̂⟵^{∗}_{R,X,β}v holds. It also succeeds if this property holds because of ∀s ∈ GT (cons) : ∃t : s⟶^{∗}_{R,X}t ∉ dom(⟶_{R,X}), Lemma 6, and ω ⪯ β.

Proof of Lemma 8.1 There exists some τ ∈ SUB(V, T (X)).Itsufficestoshowthefol. claimsforallt, t′ ∈ T :

\underline{Claim 1 :}F or t⟶_{R,V}t′ wehave tτ⟶_{R,X}t′τ .

\underline{Claim 2 :}F orq ∈ tand t/q↠_{R,V}t′ wehave tτ↠_{R,X}t′τ .

\underline{P roofofClaim 1 :}ByCorollary 6weget tτ⟶_{R,V}t′τ andthenbyLemma 6 tτ⟶_{R,X}t′τ .

\underline{P roofofClaim 2 :}T hereare((l, r), C) ∈ R; σ ∈ SUB(V, T ); p ∈ t/q; u ∈ TERMS(C)with t/qp = lσ ; t′ = uσ ; Cσfulfilledw.r.t. ⟶_{R,V}.ByCorollary 6, Cστisfulfilledw.r.t. ⟶_{R,V}.ByLemma 6, Cστisfulfilledw.r.t. ⟶_{R,X}.T hus; sincetτ ∈ T (sig, X); στ ∈ SUB(V, T (X)); qp ∈ tτ; tτ/qp = lστ ; t′τ = uστ ; weget tτ↠_{R,X}t′τ .

Proof of Lemma 8.1 \underline{8.1.:} Suppose that ≻ is not noetherian. As ▷_{ST} and ⇉ are noetherian, there must be r, s : N → T with ∀i ∈ N : r_{i}▷_{ST}s_{i} ⇉^{⊕} r_{i+1} . Then there is a p : N → N_{+}^{+} with ∀i ∈ N : r_{i}/p_{i} = s_{i} . Define t_{n} := r_{0} [ p_{0} ← r_{1} [ p_{1} ← r_{2} … [ p_{n−1} ← r_{n}] …]]. Because of r_{i}/p_{i} = s_{i} ⇉^{⊕} r_{i+1} we get t_{n} ∈ T (as ⇉^{⊕} sort-invariant) and t_{n} ⇉^{⊕} t_{n+1} (as ⇉^{⊕} T -monotonic). This contradicts ⇉ being noetherian. If ⇉ is V-stable, additionally, then ≻ is V-stable too, because ▷_{ST} is. Here is an example for ≻ not sort-invariant and not GT -monotonic: Let A, B be two different sorts. Let α(a) = A , α(f) = A → B , α(g) = A → A . Define ⇉:= ∅. Then we have ≻ = ▷_{ST} and therefrom: f a ≻ a (hence not sort-invariant); and g a ≻ a but f g a ⊁ f a (hence not GT -monotonic). \underline{8.1.:} Take the signature from the example in the proof of (8.1). ⇉:= \{(a, f a)\} is a T - monotonic (indeed!), well-founded ordering on T that is not sort-invariant. Now ≻ is not irreflexive: a ⇉ f a ▷_{ST} a . If one changes α(f) to be α(f) = A → A , then ⇉ is a sort-invariant, well-founded ordering on T that is not T -monotonic. \underline{8.1.:} For t▷_{ST}t′ ⇉ t′′ there is a p∈ t; p ≠ ∅with t′ = t/p .Bysort−invarianceandT −monotonicity of⇉ we get t = t[ p ← t′] ⇉ t[ p ← t′′]▷_{ST}t′′ . \underline{8.1.:} W.r.t. the noetherian word rewriting system \{(▷_{ST} ⇉, ⇉ ▷_{ST})\} , generated from (8.1), words from {⇉, ▷_{ST}}^{+} have normal forms only in {▷_{ST}}^{+} ∪ ({⇉}^{+} ∘ {▷_{ST}}^{∗}) .

Proof of Lemma 3 Suppose ▷ is not noetherian. Then there is a t : N → T with

∀i ∈ N : t_{i}(⇉ ∪ ↪ ∪▷_{ST}) t_{i+1} .

Define k : N → N by: \begin{matrix}k_{0} = & 0 \\ k_{i+1} = & 1 + min \{ j | j ≥ k_{i} ∧ t_{j} ↪ t_{j+1} \} \end{matrix}

The above minimum always exists because (⇉ ∪▷_{ST}) is noetherian. We have t_{k_{i}}((⇉ ∪▷_{ST}) ∘ ↪) t_{k_{i+1}} . By ▷_{ST}∘ ⇉ ⊆ ⇉ ∘▷_{ST} we get t_{k_{i}}(⇉ ∘▷_{ST} ∘ ↪) t_{k_{i+1}} , which means t_{k_{i}}(⇉ ∪ (⊵_{ST}∘ ↪))^{⊕}t_{k_{i+1}} , which contradicts the assertion that (⇉ ∪ (⊵_{ST}∘ ↪)) is noetherian. An alternative proof (using the Axiom of Choice) can be done the following way: (⇉ ∪ (⊵_{ST} ∘ ↪)) quasi-commutes over (⇉ ∪ ▷_{ST}) in the sense of Bachmair&Dershowitz[3]. Thus, (⇉ ∪ ↪ ∪▷_{ST}) must be noetherian by Theorem 1 of Bachmair&Dershowitz[3].

Proof of Lemma 8.3 ⟶_{R,Y} ⊆ > is trivial by induction on the construction of ⟶_{R,Y} using Lemma 6. ⟶_{R,Y} ∪ ↠_{R,Y} ∪ ▷_{ST} ⊆ ▷ is trivial. R is X-compatible with T by Lemma 6. By Lemma 8.1 we know that (⟶_{R,V} ∪ (⊵_{ST} ∘ ↠_{R,V})) is noetherian. By Lemma 8.1 and Lemma 3 we know that ( ⟶^{+}_{R,V}, (⟶_{R,V} ∪ ↠_{R,V} ∪ ▷_{ST})^{⊕} ) is a termination-pair over sig/V, with which R is trivially V-compatible.

Proof of Theorem 8.3 \underline{\underline{\underline{(1) ⇒ (2):}}} By Lemma 7. \underline{\underline{\underline{Q.e.d. ((1) ⇒ (2))}}}

\underline{\underline{\underline{(2) ⇒ (1):}}} First notice that the usual modularisation of the proof for the unconditional

analogue of the theorem (by showing first that local confluence is guaranteed except for the cases that are matched by critical peaks (the so-called “critical pair lemma”)) is not possible here because we need the confluence-property to hold for the condition terms even for the cases that are not matched by critical peaks. Now to the proof: Let s be minimal in ▷ such that ⟶ is not confluent below s. Because of ⟶ ⊆ ▷ (by Lemma 8.3), ⟶ is not even locally confluent below s. Let p, q ∈ s ; t_{0}⟵_{p}s⟶_{q}t_{1} ; t_{0} ∤↓t_{1} . Now as one of p, q must be a prefix of the other, w.l.o.g. say that q is a prefix of p. As s ⊵ s/q , by the minimality of s we have q = ∅. Now for k < 2 there must be ((l_{k}, r_{k}), C_{k}) ∈ R ; μ_{k} ∈ SUB(V, T (X)) ; with C_{k}μ_{k} fulfilled; s = l_{1}μ_{1} ; s/p = l_{0}μ_{0} ; t_{0} = l_{1}μ_{1}[ p ← r_{0}μ_{0} ] ; t_{1} = r_{1}μ_{1} . \underline{\underline{The inductive case: p = q_{0}q_{1}; l_{1}/q_{0} = x ∈ V :}} By xμ_{1}/q_{1} = l_{1}μ_{1}/q_{0}q_{1} = s/p = l_{0}μ_{0} and Lemma 6 (in case of x ∈ V_{CONS}), we can define ν ∈ SUB(V, T (X)) by (y ∈ V): yν :=

\{ \begin{matrix}xμ_{1}[ q_{1} ← r_{0}μ_{0} ] & if y = x \\ yμ_{1} & otherwise \end{matrix} \} andget yμ_{1}⟶^{=}yν for y ∈ V .ByCorollary 6 :

t_{0} = l_{1}μ_{1}[ q_{0}q_{1} ← r_{0}μ_{0} ] = l_{1}[ q_{0} ← xν][ q′ ← yμ_{1} | l_{1}/q′ = y ∈ V ∧ q′ ≠ q_{0} ]

⟶^{∗}l_{1}[ q′ ← yν | l_{1}/q′ = y ∈ V ] = l_{1}ν ;

t_{1} = r_{1}μ_{1}⟶^{∗}r_{1}ν .Itsufficestoshow l_{1}ν⟶r_{1}ν , whichfollowsfrom :

\underline{Claim :}C_{1}ν is fulfilled. \underline{Proof of Claim:} For each L in C_{1} we have to show that Lν is fulfilled. By our compatibilityproperty we get ∀u ∈ TERMS(L) : l_{1}μ_{1} ▷ uμ_{1} .

\underline{L = (u=v):} We know uν⟵^{∗}uμ_{1} ↓ vμ_{1}⟶^{∗}vν . As s = l_{1}μ_{1} ▷ uμ_{1} we have uν ↓ vμ_{1}⟶^{∗}vν

. As s = l_{1}μ_{1} ▷ vμ_{1} we have uν ↓ vν . \underline{L = (Def u):} We know the existence of û ∈ GT (cons) with uν⟵^{∗}uμ_{1}⟶^{∗}û. By Lemma 6 and Lemma 8.3 we can additionally assume û to be irreducible. By s = l_{1}μ_{1} ▷ uμ_{1} we get

uν⟶^{∗}û .

\underline{L = (u≠v) :} We know the existence of û, v̂ ∈ GT (cons) with uν⟵^{∗}uμ_{1}⟶^{∗}û∤↓v̂⟵^{∗}vμ_{1}⟶^{∗}vν . Just like above we can additionally assume û, v̂ to be

irreducible. By s = l_{1}μ_{1} ▷ uμ_{1}, vμ_{1} we get uν ↓ û ; v̂ ↓ vν ; and hence uν⟶^{∗}û∤↓v̂⟵^{∗}vν .

Q.e.d. (Claim; The inductive case)

\underline{\underline{The critical peak case: p ∈ l_{1}; l_{1}/p ∉ V :}} Let ξ := min Sep(V(((l_{0}, r_{0}), C_{0})), V(((l_{1}, r_{1}), C_{1}))) and Y := V(((l_{0}, r_{0}), C_{0})ξ, ((l_{1}, r_{1}), C_{1})) .

Let ϱ be given by xϱ = \{ \begin{matrix}xμ_{1} & if x ∈ V(((l_{1}, r_{1}), C_{1})) \\ xξ^{−1}μ_{0} & otherwise \end{matrix} \} (x ∈ V).

By l_{0}ξϱ = l_{0}ξξ^{−1}μ_{0} = s/p = l_{1}μ_{1}/p = l_{1}ϱ/p = (l_{1}/p)ϱ let σ := min Mgu(⟨(l_{0}ξ, l_{1}/p)⟩, Y) and τ ∈ SUB(V, T (X)) with στY = ϱY . Let ((l′, r′), D) := ((l_{1}[ p ← r_{0}ξ], r_{1}), C_{0}ξ C_{1})σ and t̂:= l_{1}σ . Now we have: ((l′, r′), D)τ = ((l_{1}[ p ← r_{0}ξ], r_{1}), C_{0}ξ C_{1})ϱ = ((l_{1}μ_{1}[ p ← r_{0}μ_{0} ], r_{1}μ_{1}), C_{0}μ_{0} C_{1}μ_{1}) = ((t_{0}, t_{1}), C_{0}μ_{0} C_{1}μ_{1}) . Hence Dτ is fulfilled. Furthermore, by t̂τ = l_{1}ϱ = l_{1}μ_{1} = s and induction hypothesis we get ∀u ◁ t̂τ : ⟶ is confluent below u . If t_{0} = t_{1}, then t_{0} ↓ t_{1} trivially. Otherwise (((l′, r′), D), t̂, p) ∈ CP(R) and then by (2 ) we get t_{0} ↓ t_{1} , too. Q.e.d. (The critical peak case; (2) ⇒ (1))

Proof of Theorem 8.3 Since the analoguos conclusions of Lemma 8.3 still hold, the proof reads just like the proof of Theorem 8.3 with the exception of the “Proof of Claim” in “The inductive case” of “ (2) ⇒ (1) ”, where after the first sentence we have to add the fol.:

Since we have free constructors and xμ_{1}⟶xν , we know x ∈ V_{SIG} . Now, if V(L) ⊆ V_{CONS} , we get x ∉ V(L) , and thus Lν = Lμ_{1} is fulfilled. Therefore we can assume V(L) ⊈ V_{CONS} in the sequel.

Proof of Lemma 8.3 Item (1 ) follows from item (2 ). By Lemma 8.3 we can now show items (2 ) and (3 ) by noetherian induction on s w.r.t. ▷. \underline{Proof of (2 ):} There is only a finite number of of positions p ∈ s and of rules l=r⟵C of R matching s/p, and the set of matching substitutions σ ∈ SUB(V(l=r⟵C), T (X)) with s/p = lσ is enumerable. Since s ▷ s[ p ← rσ] for Cσ being fulfilled, by induction hypothesis we only have to be able to semi-decide whether Cσ is fulfilled. In case of left-right-compatibility we semi-decide the fulfilledness of the literals from left to right; in case of compatibility only, we wait with our parallel enumeration until we have been able to establish the condition terms to be ◁-smaller than lσ. Thus, for semi-deciding the fulfilledness of a literal L in Cσ we can assume its terms to be ◁-smaller than s. By induction hypothesis it is obvious now how to semi-decide fulfilledness of ‘=’- and ‘Def’- literals in Cσ, and how to semi-decide ‘≠’-literals using item (3 ). \underline{Proof of (3 ):} By Lemma 6, the constructor rules being extra-variables free, and R and s being finite, there can be only a finite number of t with s⟶t , and by the induction hypothesis this also holds for those t with s⟶^{+}t . In case of left-right-compatibility we decide the fulfilledness of the literals from left to right; in case of compatibility only, we know that Cσ cannot be fulfilled if the test fails whether all its terms are ◁-smaller than lσ. Thus, for deciding the fulfilledness of a literal L in Cσ we can assume its terms to be ◁-smaller than s. By induction hypothesis it is obvious now how to decide fulfilledness of ‘=’- and ‘Def’-literals in Cσ.

Proof of Lemma 8.3 Take the unconditional rule system of the proof of Lemma 8. From this system we are now going to construct our positive-conditional rule system by adding as new first argument a step-counter to our Turing machine by exchanging the recursive T-rules of the form “ T l a r c s p = T l′ a′ r′ c′ s′ p′ ” for rules of the form “ T s x l a r c s p = T x l′ a′ r′ c′ s′ p′ ” and the non-recursive T-rule by T x l a r stop s p = ⊥ . Finally we add the rule

terminatesp l a r c s p = true ⟵ T x l a r c s p = ⊥ ,

where ‘terminatesp’ and ‘true’ are of a new sort. For the decidable ordering ▷ of the termination-pair take the lexicographic path ordering where ‘terminatesp’ is bigger than all other function symbols and the variables of the old sorts; ‘T’ is bigger than all function symbols except ‘terminatesp’; and ‘cmd’ and ‘state’ are bigger than ‘nth’. Now, since “ terminatesp l a r c s p ” is reducible iff the Turing machine of the proof of Lemma 8 halts, reducibility of ground terms cannot be co-semi-decidable.

Proof of Lemma 8.3 The proof is very similar to that of Lemma 8.3. Finally, (3 ) follows from (2 ), Theorem 8.3, and T (sig, X) being enumerable.

Proof of Lemma 8.3 Take the unconditional part of the rule system of the proof of Lemma 8.3. For getting our positive conditional CRS R, add the rules

terminatesp x = false
terminatesp x = true ⟵ T x l a r c s p = ⊥ ,

where ‘terminatesp’, ‘false’, and ‘true’ are of a new sort; and l, a, r, c, s, p are ground terms. For the decidable ordering ▷ of the termination-pair take the lexicographic path ordering where ‘terminatesp’ is bigger than all other function symbols and the variables of the old sorts; ‘T’ is bigger than all function symbols except ‘terminatesp’; and ‘cmd’ and ‘state’ are bigger than ‘nth’. Now, the fol. statements are logically equivalent:

• ⟶_{R,V} is confluent.

• The critical peak (((true, false), T x l a r c s p = ⊥), terminatesp x, ∅) is joinable w.r.t. R, V.

• There is no term t ∈ T (sig, V_{SIG}⊎V_{CONS}) with T t l a r c s p ⟶^{∗}_{R,V} ⊥ .

• The Turing machine of the proof of Lemma 8 does not halt.

Proof of Lemma 9 \underline{Proof of (1):} Since K ⊆ M . \underline{Proof of (2):} If no rule in R has a negative condition, then there is some A being free in M over V w.r.t. some κ. Then A is in K. Let B∈ Mandμ ∈ SUB(V, B).Theremustbesomeh::A→Bwith μ = κh .Since“ ⟶ Δ ′′istype − B − inductivelyvalidbyassumption, theremustbesomeatom(u=v)orsomeatom(Def u)inΔwhichistruew.r.t. A_{κ}.Thenwehave A_{κ}(u) = A_{κ}(v) or A_{κ}(u) ∈ A(CONS, s) forsomes ∈ 𝕊.ThenwehaveB_{μ}(u)= B_{κh}(u)= h(A_{κ}(u)) andthenB_{μ}(u)= h(A_{κ}(v))= B_{μ}(v) or B_{μ}(u) ∈ B(CONS, s) .

Proof of Lemma 9 \underline{\underline{Proof of (1):}} Let A be a CONS:cons-term-generated constructor-minimal model of R. Let χ ∈ SUB(V, A).BytheAxiomofChoicethereissomeτ ∈ CGSUB(V, cons)withχ = τA_{χ}. \underline{Claim} : F orA ∈ AT (sig, V) : Aistruew.r.t. A_{χ} iff Aτ is true w.r.t. A_{χ} . \underline{Proof of Claim:} By the Substitution-Lemma(4.2) we get for u∈ T :

A_{χ}(u) = A_{τA_{χ}}(u) = A_{χ}(uτ) \underline{Q.e.d. (Claim)}

Now, if each atom A in Γ istruew.r.t. A_{χ} , then(byClaim)Aτistruew.r.t. A_{χ} , too.T hus(since(Γ, Δ) istype− B−inductivelyvalidbyassumption), theremustbesomeatomAinΔforwhichAτistruew.r.t. A_{χ} .T hen(byClaim)Aistruew.r.t. A_{χ} , too. \underline{\underline{P roofof(2) :}}LetA beaconstructor − minimalmodelofR.Definethesig/cons − algebra B by f^{B} := f^{A} (f ∈ 𝔽); B(SIG, s) := A(SIG, s) (s ∈ 𝕊); B(CONS, s) := A[GT_{CONS,s}] (s ∈ 𝕊). \underline{Claim 1 :}F orχ ∈ SUB(V, B); (u=v) ∈ AT (sig, V) :

(u=v)istruew.r.t. B_{χ} iff (u=v)istruew.r.t. A_{χ}

\underline{Claim 2 :}F orχ ∈ SUB(V, B); (Def u) ∈ AT (sig, V) :

If(Def u)istruew.r.t. B_{χ} , then(Def u)istruew.r.t. A_{χ} too.

Bythesetwotrivialclaimsand  B ≲_{H}A  ; B  isaconstructor  −
minimalmodelofR, which, ofcourse, isCONS:cons  −  term  −  gene-

rated.Letτ ∈ CGSUB(V, cons)and χ ∈ SUB(V_{SIG}, A) = SUB(V_{SIG}, B) .Now, supposethatforeachatomAinΓ : Aτistruew.r.t. A_{χ} .T wocases : F or A = (u=v) , byClaim 1weknowthatAτistruew.r.t. B_{χ} , andbytheSubstitution− Lemma(4.2)Aistruew.r.t. B_{τB_{χ}} .F or A = (Def u) , weknowthat“ ⟶ A ′′istype − C − inductivelyvalidbyassumption, i.e. Aistruew.r.t. B_{τB_{χ}} , too.T hus(since(Γ, Δ) istype−C − inductivelyvalidbyassumption), theremustbesomeatomAinΔwhichistruew.r.t. B_{τB_{χ}} .BytheSubstitution− Lemma(4.2)Aτistruew.r.t. B_{χ} .ByClaim 1orbyClaim 2weknowthatAτistruew.r.t. A_{χ} .

Proof of Lemma 9 Define A := T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} . Define I := GT /⟷^{∗}_{R,∅} . Let κ be given by (x∈V_{SIG}):

x ↦ ⟷^{∗}_{R,V_{SIG}}[{x}] .

\underline{Proof of (1):} By confluence of ⟶_{R,V_{SIG}}[∩(D_{V_{SIG}}×D_{V_{SIG}})] and Theorem 6(1), A is a constructor-minimum model of R. Furthermore, A is CONS:cons-term-generated. \underline{Proof of (2):} Let B be a CONS:cons-term-generated constructor-minimal model of R.

Let μ ∈ SUB(V, B).Byconfluenceof ⟶_{R,∅}[∩(D_{∅}×D_{∅})] andT heorem 6, thereisasig/cons−

homomorphism h::A→B with μV_{SIG} = κh .F urthermore, bytheAxiomofChoicethereissomeτ ∈ SUB(V_{CONS}, GT )with μV_{CONS} = τB = τA h .Defineχ ∈ SUB(V, A)by χ := κ ⊎ τA .W ehave μ = χh .NowassumeeachatomAinΓ to be true w.r.t. B_{μ}.T wocases : If A = (Def u) , then(since“ ⟶ A ′′istype − D − inductivelyvalidbyassumption)Aistruew.r.t. A_{χ} .If A = (u=v) , then(since“ ⟶ Def u′′and“ ⟶ Def v′′aretype−

D−inductivelyvalidbyassumption)therearesomes ∈ 𝕊; û, v̂ ∈ GT_{CONS,s}with A_{χ}(u) = A(û) and A_{χ}(v) = A(v̂) .T henweget B(û) = h_{s}(A(û)) = h_{s}(A_{χ}(u)) = B_{χh}(u) = B_{μ}(u) = B_{μ}(v) = B_{χh}(v) = h_{s}(A_{χ}(v)) = h_{s}(A(v̂)) = B(v̂) .Byconfluenceof ⟶_{R,∅}[∩(D_{∅}×D_{∅})] andT heorem 6(1), I andthereforealsoB isaconstructor−

minimummodel.Hence(sinceû, v̂ ∈ GT (cons)) I(û) = I(v̂) ; i.e. û⟷^{∗}_{R,∅} v̂ .ByLemma 6weget û⟷^{∗}_{R,V_{SIG}} v̂ , andthen A_{χ}(u) = A(û) = A(v̂) = A_{χ}(u) .T husAistruew.r.t. A_{χ} .Allinall, allatomsinΓ

are true w.r.t. to A_{χ} . By the assumed type-D-inductive validity of (Γ, Δ), there must be an atom A in Δ which is true w.r.t. A_{χ} . Two cases: If A = (Def u) with u ∈ T_{SIG,s} , then (since A_{χ}(u) ∈ A(CONS, s) ) B_{μ}(u) = B_{χh}(u) = h_{s}(A_{χ}(u)) ∈ B(CONS, s) . If A = (u=v) , then (since A_{χ}(u) = A_{χ}(v) ) B_{μ}(u) = h_{s}(A_{χ}(u)) = h_{s}(A_{χ}(v)) = B_{μ}(v) .

Proof of Lemma 9

Let A:=T (V_{SIG})/⟷^{∗}_{R,V_{SIG}}.Letκ∈SUB(V_{SIG}, A)begivenby(x∈V_{SIG}):x↦ ⟷^{∗}_{R,V_{SIG}}[{x}].

\underline{Claim :}F orτ ∈ SUB(V, T (V_{SIG})); A ∈ AT (sig, V) :

Aistruew.r.t. A_{τA_{κ}} iff Aτistruew.r.t. A_{κ} .

\underline{P roofofClaim :}BytheSubstitution − Lemma(4.2). \underline{Q.e.d. (Claim)}

\underline{(1) ⇒ (2) :}Letτ ∈ SUB(V, T (V_{SIG}))andsupposethatforeach(u=v)inΓ wehave uτ⟷^{∗}_{R,V_{SIG}}vτ andforeach(Def u)inΓ wehavesomeû ∈ GT (cons)with uτ⟷^{∗}_{R,V_{SIG}} û .T henforeachatomAinΓ weknowthatAτistruew.r.t. A_{κ} , andthen(byClaim)thatAistruew.r.t. A_{τA_{κ}} .T hus(since(Γ, Δ) istype−

D−inductivelyvalidbyassumption), thereissomeAinΔwhichistruew.r.t. A_{τA_{κ}} .ByClaimAτistruew.r.t. A_{κ} .T wocases :

F or A = (u=v) , weget uτ⟷^{∗}_{R,V_{SIG}}vτ .F or A = (Def u) , wegetsomes ∈ 𝕊andsomeû ∈ GT_{CONS,s} = T (V_{SIG})(CONS, s)with uτ⟷^{∗}_{R,V_{SIG}} û .

\underline{(2) ⇒ (1) :}Letχ ∈ SUB(V, A).NowsupposethateachatomAinΓ istruew.r.t. A_{χ} .BytheAxiomofChoicethereissomeτ ∈ SUB(V, T (V_{SIG}))with χ = τA_{κ} .ByClaimAτistruew.r.t. A_{κ} .T hus(since(2)holdsbyassumption), thereissomeAinΔsuchthatAτistruew.r.t. A_{κ} .ByClaim, Aistruew.r.t. A_{χ} .

Proof of Theorem 9 Let A′ be a sig′/cons′-algebra. Define the sig/cons-algebra A by: A := A′𝔽 ⊎ {SIG, CONS}×𝕊 . Now an “old” formula (Γ, Δ)∈ isvalidinA iff itisvalidinA′.F urthermore, itsinductiveinstances (Γ, Δ)τ donotdifferfor τ ∈ CGSUB(V, cons) and τ ∈ CGSUB(V′, cons′) since ∀s ∈ 𝕊 : GT (cons)_{s} = GT (cons′)_{s} .T husforproving(A)[and(B)], itsufficestoshowthefol. :

Claim :

If A′ is a [constructor-minimal] model of R′, then A is a [constructor-minimal] model of R.

T hisClaimisalsosufficientfor(C); becauseifA′ isCONS:cons′ − term − generated, thenA isCONS:cons − term − generated. \underline{P roofofClaim :}AseachrulefromR canbetranslatedintoan“old′′formula(onwhichA andA′ donotdiffer(cf. above)), A isasig/cons−

model ofR.LetGT ’denotethegroundtermalgebraoversig’/cons’andGT (cons) denotethegroundtermalgebraovercons.Byconfluenceof ⟶_{R′,∅}[∩D′_{∅}×D′_{∅}] andT heorem 6(1), GT′/⟷^{∗}_{R′,∅} isaconstructor−

minimummodelofR′ w.r.t. sig’/cons’.T hus, A′ mustbeaconstructor −

minimummodelofR′ w.r.t. sig’/cons’, too.T hereforetheremustbesomecons’−homomorphism h′::A′ℂ′ ⊎ ({CONS}× 𝕊′)→(GT′/⟷^{∗}_{R′,∅})ℂ′ ⊎ ({CONS}× 𝕊′) .Bydefining h_{s}(a) := h′_{s}(a) ∩ GT (cons) ( a ∈ A(CONS, s) ; s ∈ 𝕊), wegetacons−

homomorphismh::Aℂ ⊎ ({CONS}× 𝕊)→GT (cons)/(⟷^{∗}_{R′,∅} ∩ (GT (cons)×GT (cons))).Byconfluenceof ⟶_{R′,∅}[∩D′_{∅}×D′_{∅}] andT heorem 6(1)andLemma 6weget (⟷^{∗}_{R′,∅} ∩ (GT (cons)×GT (cons))) ⊆ (↓_{R′,∅} ∩ (GT (cons)×GT (cons))) ⊆ (↓_{R,∅} ∩ (GT (cons)×GT (cons))) ⊆ ↓_{R,∅,ω} ⊆ ⟷^{∗}_{R,∅,ω} .F inally, foreachsig/cons−

model C ofR weget ∀β ⪯ ω : ∀s ∈ 𝕊 : ⟶_{R,∅,β} ∩ (GT_{SIG,s}×GT_{SIG,s}) ⊆ ker(C)_{s} byinductiononβ; thus ∀s ∈ 𝕊 : (⟷^{∗}_{R′,∅} ∩ (GT (cons)_{s}×GT (cons)_{s})) ⊆ ker(C)_{s} ; andthenbytheHomomorphism−

T heorem(4.2) A ≲_{CONS} C .T husA isnotonlyasig/cons − model ofR butalsoaconstructor − minimalone. \underline{Q.e.d. (Claim)} \underline{P roofof(D) :}W edotheprooffortheequivalentversionoftype − D −

inductivevaliditygivenbyLemma 9(2).Letτ′ ∈ SUB(V′, T′(V′_{SIG}))andsupposethepremiseofLemma 9(2)toholdforthisτ′.T hereisaτ ∈ CGSUB(V′, cons′)andaσ ∈ SUB(V′_{SIG}, T′(V′_{SIG}))suchthat τ′ = τσ .Notethat τV ∈ SUB(V, T (V_{SIG})) .F oreachatom(u=v)inΓ wehaveassumedthat“ ⟶ Def u′′and“ ⟶ Def v′′arevalidin T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} .T husthereareû, v̂ ∈ GT (cons)with uτ⟷^{∗}_{R,V_{SIG}} û and vτ⟷^{∗}_{R,V_{SIG}} v̂ .ByT heorem 6(2)weget uτ⟷^{∗}_{R′,V′_{SIG}} û and vτ⟷^{∗}_{R′,V′_{SIG}} v̂ , andthenbyCorollary 6andthesupposed uτ′⟷^{∗}_{R′,V′_{SIG}}vτ′ get û⟷^{∗}_{R′,V′_{SIG}} uτσ⟷^{∗}_{R′,V′_{SIG}} vτσ⟷^{∗}_{R′,V′_{SIG}} v̂ .ByLemma 6weget û⟷^{∗}_{R′,∅} v̂ andthen(byconfluenceof ⟶_{R′,∅}[∩(D_{∅}×D_{∅})] ) û↓_{R′,∅} v̂ , andthenbyT heorem 6(1)weget û↓_{R,∅} v̂ andthenbyLemma 6 uτ⟷^{∗}_{R,V_{SIG}} û⟷^{∗}_{R,V_{SIG}} v̂⟷^{∗}_{R,V_{SIG}}vτ .F urthermore, foreachatom(Def u)inΓ wehaveassumedthat“ ⟶ Def u′′isvalidin T (V_{SIG})/⟷^{∗}_{R,V_{SIG}} .T husthereisaû ∈ GT (cons)with uτ⟷^{∗}_{R,V_{SIG}} û .T hus(since(Γ, Δ) istype−

D−inductivelyvalidbyassumption), thereisaliteral(u=v)inΔwith uτ⟷^{∗}_{R,V_{SIG}}vτ oraliteral(Def u)inΔwith uτ⟷^{∗}_{R,V_{SIG}} û forsomeû ∈ GT (cons).ByT heorem 6(2)weget uτ⟷^{∗}_{R′,V′_{SIG}}vτ or uτ⟷^{∗}_{R′,V′_{SIG}} û , andthenbyCorollary 6 uτσ⟷^{∗}_{R′,V′_{SIG}}vτσ or uτσ⟷^{∗}_{R′,V′_{SIG}} û .

B Unification

An (inefficient) algorithm for computing a most general unifier for a finite multi-set E of sort-invariant pairs of terms is given by the fol. inference system, which must be started with (E, V_{CONS}(E, X), id) for computing an element of Mgu(E, X) in the last position of any triple to which no inference rule applies anymore:

Delete:  (E ⊔ ⟨(t, t)⟩  , X  , σ )
(E  , X  , σ )
Function Symbol Clash: (E ⊔ ⟨(fs_{0} … s_{m−1}, gt_{0} … t_{n−1})⟩ , X  , σ )

FAILURE

if f ≠ g.

Divide:  (E ⊔ ⟨(fs_{0} … s_{m}, ft_{0} … t_{m})⟩  , X  , σ )
(E ⊔ ⟨ (s_{i}, t_{i}) | i ≤ m ⟩  , X  , σ )
Align:  (E ⊔ ⟨(t, x)⟩  , X  , σ )
(E ⊔ ⟨(x, t)⟩  , X  , σ )
if (x ∈ V ∧ t ∉ V) or (x ∈ V_{SIG} ∧ t ∈ V_{CONS}) .
Occur-In Clash:  (E ⊔ ⟨(x, t)⟩  , X  , σ )

FAILURE

if x ∈ V(t) and x ≠ t.

Solve SIG-Variable:  (E ⊔ ⟨(x, t)⟩  , X  , σ )
(Eμ  , X  , σμ )

if x ∈ V_{SIG}\V(t) ; μ ∈ SUB(V, T ) given by xμ = t and μV \ {x} = idV \ {x} .

Solve CONS-Variable:  (E ⊔ ⟨(x, t)⟩  , X  , σ )
(Eμ  , X ∪ ran(ξ) , σμ )

if x ∈ V_{CONS}\V(t) ; t ∈ T (cons, V_{SIG}⊎V_{CONS}) ; μ ∈ SUB(V, T ) given by (y ∈ V)

yμ := \{ \begin{matrix}t(ξ ∪ idV_{CONS}) & if y = x \\ yξ & if y ∈ V_{SIG}(t) \\ y & otherwise \end{matrix} \}

such that ξ : V_{SIG}(t) → V_{CONS}\X is injective.

Variable Sort Clash:  (E ⊔ ⟨(x, t)⟩  , X  , σ )

FAILURE

if x ∈ V_{CONS} and t ∈ T \T (cons, V_{SIG}⊎V_{CONS}) .

The inference relation of the above inference system is noetherian on triples from

FMul(DEq(sig, V_{SIG}⊎V_{CONS})) × 𝔓_{N}(V_{CONS}) × SUB(V, T ) .

If it terminates on (E, V_{CONS}(E, X), σ) with FAILURE, then there is no μ ∈ SUB(V, T )withset[E]μ ⊆ id.Ifitterminateson(E, V_{CONS}(E, X), id) with (E′, X′, σ), then σ ∈ Mgu(E, X) , σσ = σ , and E′ = ∅ .

Proof of Lemma B

Let ‘⊢’ denote the inference relation. ⊢ is noetherian because it either yields FAILURE or decreases (w.r.t. the lexicographic combination of (1.) the usual ordering on N, (2.) the multi-set extension of the subterm ordering, (3.) the usual ordering on N)

(E, X, σ) measured by  1. |V(E)|, 2. ⟨ set(e)_{0}, set(e)_{1} | e ∈ E ⟩, 3. |{ e ∈ E | set(e) ∈ ((T \V) × V) ∪ (V_{CONS} × V_{SIG}) }|.

\underline{Claim 1:} Let n ∈ N ; ∀i < n : (E_{i}, X_{i}, σ_{i}) ⊢ (E_{i+1}, X_{i+1}, σ_{i+1}) ; and σ_{0} = id . Now: ∀τ ∈ SUB(V, T ) : ((set[E_{0}]σ_{n}τ ⊆ id) ⇔ (set[E_{n}]τ ⊆ id)) . \underline{Proof of Claim 1:} \underline{n = 0:} Trivial. \underline{n ⇒ (n + 1):} If (E_{n}, X_{n}, σ_{n}) ⊢ (E_{n+1}, X_{n+1}, σ_{n+1}) by a Delete, Divide, or Align, the proof succeeds due to σ_{n+1} = σ_{n} and set[E_{0}]σ_{n}τ ⊆ id iff set[E_{n}]τ ⊆ id iff set[E_{n+1}]τ ⊆ id . Thus, suppose this step to be a Solve. Then for some E′, using the denotation of the rules, we get σ_{n+1} = σ_{n}μ ; E_{n} = E′ ⊔ ⟨(x, t)⟩ ; and E_{n+1} = E′μ . \underline{Sub-claim:} xμ = tμ Now: set[E_{0}]σ_{n+1}τ ⊆ id iff set[E_{0}]σ_{n}μτ ⊆ id iff (by induction hypothesis) set[E_{n}]μτ ⊆ id iff (set[E′]μτ ⊆ id ∧ xμτ = tμτ) iff (by Sub-claim) set[E′]μτ ⊆ id iff set[E_{n+1}]τ ⊆ id . \underline{Proof of Sub-claim:} In case of a Solve SIG-Variable, we get xμ = t = tμ using x ∉ V(t) for the last step. In case of a Solve CONS-Variable, we get xμ = t(ξ ∪idV_{CONS}) = tμ using x ∉ V(t) for the last step. \underline{Q.e.d. (Claim 1)}

\underline{Claim 2:} Let n ∈ N ; ∀i < n : (E_{i}, X_{i}, σ_{i}) ⊢ (E_{i+1}, X_{i+1}, σ_{i+1}) ; σ_{0} = id ; and V_{CONS}(E_{0}) ⊆ X_{0} . Now:

1. V_{CONS}(E_{n} ∪ σ_{n}[X_{0} ∪ V_{SIG}]) ⊆ X_{n}

2. σ_{n}V(E_{n}) ∪ (V_{CONS} \ X_{n}) ⊆ id

3. σ_{n}σ_{n} = σ_{n}

4. If set[E_{0}]π_{0} ⊆ id for some π_{0} ∈ SUB(V, T ), thenthereissomeπ_{n} ∈ SUB(V, T )with π_{0}X_{0} ∪ V_{SIG} = σ_{n}X_{0} ∪ V_{SIG}π_{n} .

\underline{Proof of Claim 2(1):} \underline{n = 0:} Trivial. \underline{n ⇒ (n + 1):} If (E_{n}, X_{n}, σ_{n}) ⊢ (E_{n+1}, X_{n+1}, σ_{n+1}) by a Delete, Divide, or Align, the proof succeeds trivially. Now suppose this step to be a Solve CONS-Variable. Then V_{CONS}(E_{n+1} ∪ σ_{n+1}[X_{0} ∪ V_{SIG}]) ⊆ V_{CONS}(μ[V_{SIG} ∪ V_{CONS}(E_{n} ∪ σ_{n}[X_{0} ∪ V_{SIG}])]) ⊆ V_{CONS}(μ[V_{SIG} ∪ X_{n}]) ⊆ X_{n}∪V_{CONS}(t)∪ran(ξ) ⊆ X_{n} ∪ ran(ξ) = X_{n+1}. For a Solve SIG-Variable we only have to omit the “∪ ran(ξ)”. Q.e.d. (Claim 2(1))

\underline{Proof of Claim 2(2):} \underline{n = 0:} Trivial. \underline{n ⇒ (n + 1):} If (E_{n}, X_{n}, σ_{n}) ⊢ (E_{n+1}, X_{n+1}, σ_{n+1}) by a Delete, Divide, or Align, the proof succeeds due to σ_{n+1} = σ_{n} , V(E_{n+1}) ⊆ V(E_{n}) , and X_{n+1} = X_{n} . Now suppose this step to be a Solve CONS-Variable. Since V(E_{n+1}) ⊆ V(E_{n}μ) ⊆ (V(E_{n}) \ ({x} ∪ dom(ξ))) ∪ (ran(ξ) \ {x}) (using ran(ξ) ∩ X_{n} = ∅, x∈V_{CONS}(E_{n})⊆X_{n} (by Claim 2(1)), x ∉ V(t)), it suffices to show yσ_{n}μ = y for the following three cases: First, for y ∈ V(E_{n}) \ ({x} ∪ dom(ξ)) we get yσ_{n}μ = yμ = y . Second, for y ∈ ran(ξ) \ {x} by y ∈ V_{CONS}\X_{n} we get yσ_{n}μ = yμ = y . Third, for y ∈ V_{CONS}\X_{n+1} ⊆ V_{CONS}\X_{n} we have yσ_{n}μ = yμ = y because if we had yμ ≠ y then y ∈ V_{CONS}(E_{n}) ⊆ X_{n} (by Claim 2(1)). For a Solve SIG-Variable we only have to omit “dom(ξ)”, “ran(ξ)”, “x ∈ V_{CONS}(E_{n}) ⊆ X_{n}” and the second case. \underline{Q.e.d. (Claim 2(2))} \underline{Proof of Claim 2(3):} \underline{n = 0:} Trivial. \underline{n ⇒ (n + 1):} If (E_{n}, X_{n}, σ_{n}) ⊢ (E_{n+1}, X_{n+1}, σ_{n+1}) by a Delete, Divide, or Align, the proof succeeds due to σ_{n+1} = σ_{n} . Now suppose this step to be a Solve. \underline{Sub-claim:} μσ_{n}μ = σ_{n}μ Now we get σ_{n+1}σ_{n+1} = σ_{n}μσ_{n}μ = σ_{n}σ_{n}μ = σ_{n}μ = σ_{n+1} . Proof of Sub-claim: \underline{Solve CONS-Variable:} xμσ_{n}μ = t(ξ ∪ idV_{CONS}(t))σ_{n}μ = (using Claim 2(2)) t(ξ ∪ idV_{CONS}(t))μ = (using ran(ξ) ∩ X_{n} = ∅, x∈V_{CONS}(E_{n})⊆X_{n} (by Claim 2(1)), x∉V(t)) t(ξ ∪ idV_{CONS}(t)) = xμ = (using x ∈ V(E_{n}), Claim 2(2)) xσ_{n}μ . For y ≠ x ; y ∈ V_{SIG}(t) : yμσ_{n}μ = yξσ_{n}μ = (using Claim 2(2)) yξμ = (using Claim 2(1) just as last time) yξ = yμ = (using Claim 2(2)) yσ_{n}μ . For y ≠ x ; y ∈ V\V_{SIG}(t) : yμσ_{n}μ = yσ_{n}μ . \underline{Solve SIG-Variable:} Very similar. \underline{Q.e.d. (Claim 2(3))}

\underline{Proof of Claim 2(4):} \underline{n = 0:} Trivial. \underline{n ⇒ (n + 1):} If (E_{n}, X_{n}, σ_{n}) ⊢ (E_{n+1}, X_{n+1}, σ_{n+1}) by a Delete, Divide, or Align, the proof succeeds due to σ_{n+1} = σ_{n} by choosing π_{n+1} := π_{n} . Thus, suppose this step to be a Solve. Then for some E′, using the denotation of the rules, we get σ_{n+1} = σ_{n}μ ; E_{n} = E′ ⊔ ⟨(x, t)⟩ ; and E_{n+1} = E′μ . \underline{Sub-claim A:} tπ_{n} = xπ_{n} \underline{Sub-claim B:} ∃π_{n+1} ∈ SUB(V, T ) : μX_{n} ∪ V_{SIG}π_{n+1} = π_{n}X_{n} ∪ V_{SIG} By induction hypothesis and for the next step by Claim 2(1) and Sub-claim B we succeed with π_{0}X_{0} ∪ V_{SIG} = σ_{n}X_{0} ∪ V_{SIG}π_{n} = σ_{n}X_{0} ∪ V_{SIG}μπ_{n+1} = σ_{n+1}X_{0} ∪ V_{SIG}π_{n+1} . Proof of Sub-claim B: \underline{Solve CONS-variable:} Define π_{n+1} := (ξ^{−1} ∪ idV \ ran(ξ))π_{n} . Now π_{n+1} ∈ SUB(V, T ) because sort-invariance is obvious and for y ∈ V \ ran(ξ) we have yπ_{n+1} = yπ_{n} and for y ∈ ran(ξ) we have yξ^{−1} ∈ V(t) , yξ^{−1}π_{n}⊴_{ST}tπ_{n} = xπ_{n} ∈ T (cons, V_{CONS}) (using Subclaim A, x ∈ V_{CONS} and π_{n} ∈ SUB(V, T )), and then yπ_{n+1} = yξ^{−1}π_{n} ∈ T (cons, V_{CONS}) . Now: xμπ_{n+1} = t(ξ ∪ idV_{CONS}(t))(ξ^{−1} ∪ idV \ ran(ξ))π_{n} = (using ran(ξ) ∩ X_{n} = ∅, V_{CONS}(t)⊆V_{CONS}(E_{n})⊆X_{n} (by Claim 2(1))) t(ξξ^{−1} ∪ idV_{CONS}(t)idV \ ran(ξ))π_{n} = tπ_{n} = xπ_{n} (using Sub-claim A). For y ≠ x , y ∈ V_{SIG}(t) , we have yμπ_{n+1} = yξπ_{n+1} = yπ_{n} . For y ≠ x , y ∈ (X_{n}∪V_{SIG}) \ V_{SIG}(t) , we have yμπ_{n+1} = yπ_{n+1} = yπ_{n} (using ran(ξ) ∩ (X_{n}∪V_{SIG}) = ∅). \underline{Solve SIG-variable:} Define π_{n+1} := π_{n} . Now: xμπ_{n+1} = tπ_{n+1} = tπ_{n} = xπ_{n} (using Sub-claim A). For y ≠ x we have yμπ_{n+1} = yπ_{n+1} = yπ_{n} . \underline{Q.e.d. (Sub-claim B)} \underline{Proof of Sub-claim A:} By set[E_{0}]σ_{n}π_{n} = set[E_{0}]π_{0} ⊆ id and Claim 1 we get set[E_{n}]π_{n} ⊆ id , i.e. xπ_{n} = tπ_{n} . \underline{Q.e.d. (Claim 2(4))}

\underline{Claim 3:} If (E, V_{CONS}(E, X), σ) ⊢^{∗} FAILURE , then ¬∃μ ∈ SUB(V, T ) : set[E]μ ⊆ id . \underline{Proof of Claim 3:} W.l.o.g. suppose (E, V_{CONS}(E, X), σ) ⊢^{∗} (E′, X′, σ′′) ⊢ FAILURE . Since the last element of the triple has no influence on the inference steps, there is a σ′ with (E, V_{CONS}(E, X), id) ⊢^{∗} (E′, X′, σ′) ⊢ FAILURE . Now if we had set[E]μ ⊆ id , then by Claim 2(4) there is some π with set[E]σ′π ⊆ id , and then by Claim 1 set[E′]π ⊆ id , which contradicts (E′, X′, σ′) ⊢ FAILURE due to the form of each of the inference rules yielding FAILURE. \underline{Q.e.d. (Claim 3)}

\underline{Claim 4:} If (E, X, σ) ∉ dom(⊢) , then E = ∅ . (Trivial.) \underline{Claim 5:} If (E, V_{CONS}(E, X), id) ⊢^{∗} (∅, X′, σ) , then σ ∈ Mgu(E, X) and σσ = σ . \underline{Proof of Claim 5:} Since set[∅] id ⊆ id we get set[E]σ ⊆ id by Claim 1. For each μ ∈ SUB(V, T ) with set[E]μ ⊆ id there is a π ∈ SUB(V, T ) by Claim 2(4) with μX = σπX . Thus σ ∈ Mgu(E, X) . Finally, by Claim 2(3) we get σσ = σ. \underline{Q.e.d. (Claim 5)}

References

[1] Jürgen enhaus, Klaus Becker. Conditional Rewriting modulo a Built-in Algebra. SEKI-Report SR–92–11, 1992. .

[2] Leo Bachmair. Proof by Consistency in Equational Theories. 3^{rd} LICS 1988, pp. 228-233.

[3] Leo Bachmair, Nachum Dershowitz. Commutation, Transformation, and Termination. 8^{th} CADE 1986, LNCS 230. Springer-Verlag, Berlin 1986.

[4] Leo Bachmair, Harald Ganzinger. On Restrictions of Ordered Paramodulation with Simplification. 10^{th} CADE 1990, LNAI 449. Springer-Verlag, Berlin 1990.

[5] Leo Bachmair, Harald Ganzinger. Perfect Model Semantics for Logic Programs with Equality. Proc. of 8^{th} Int. Conf. on Logic Programming, pp. 645-659. MIT Press, 1991.

[6] Leo Bachmair, Harald Ganzinger. Rewrite-Based Equational Theorem Proving with Selection and Simplification. Technical Report MPI-I-91-208. Max-Planck-Institut für Informatik, Saarbrücken, August 1991.

[7] Klaus Becker. Inductive Proofs in Specifications Parameterized by a Built-In Theory. SEKI-Report SR–92–02, 1992. .

[8] Klaus Becker. Semantics for Positive/Negative Conditional Rewrite Systems. 3^{rd} CTRS 1992, LNCS 656. Springer Verlag, Berlin 1993.

[9] Eddy Bevers, Johan Lewi. Proof by Consistency in Conditional Equational Theories. Report CW 102, Revised July 1990. Department of Computer Science, K. U. Leuven.

[10] Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther. The Karlsruhe Induction Theorem Proving System. 8^{th} CADE 1986, LNCS 230. Springer-Verlag, Berlin 1986.

[11] Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch. Automated Mathematical Induction. Technical Report 1636, INRIA, 1992.

[12] Robert S. Boyer, J Strother Moore. A Computational Logic. Academic Press, 1979.

[13] Robert S. Boyer, J Strother Moore. A Computational Logic Handbook. Academic Press, 1988.

[14] François Bronsard, Uday S. Reddy. Conditional Rewriting in Focus. Department of Computer Science, The University of Illinois at Urbana-Champaign, Urbana, IL 61801.

[15] Nachum Dershowitz. Termination of Rewriting. J. Symbolic Computation (1987) 3, pp. 69-116.

[16] Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar. Confluence of Conditional Rewrite Systems. 1^{st} CTRS 1988, LNCS 308. Springer-Verlag, Berlin 1988.

[17] Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar. Canonical Conditional Rewrite Systems. 9^{th} CADE 1988, LNAI 310. Springer-Verlag, Berlin 1988.

[18] Herbert B. Enderton. A mathematical introduction to logic. Academic Press, 2^{nd} printing 1973.

[19] Harald Ganzinger. A Completion Procedure for Conditional Equations. First international workshop on Conditional Term Rewriting Systems. LNCS 308. Springer-Verlag, Berlin 1988.

[20] Harald Ganzinger, Jürgen Stuber. Inductive Theorem Proving by Consistency for First-Order Clauses. In: Informatik-Festschrift zum 60. Geburtstag von Günter Hotz. Teubner Verlag, Stuttgart 1992. Also in: 3^{rd} CTRS 1992, LNCS 656. Springer Verlag, Berlin 1993.

[21] Richard Göbel. A Completion Procedure for Generating Ground Confluent Term Rewriting Systems. Dissertation, 1988, .

[22] Martin Gogolla. Algebraic Specifications with Partially Ordered Sorts and Declarations. Forschungsbericht Nr. 169, 1983. Universität Dortmund, Postfach 500500, W-4600 Dortmund.

[23] Bernhard Gramlich. Inductive Theorem Proving Using Refined Unfailing Completion Techniques. SEKI-Report SR–89–14, 1989. .

[24] Gérard Huet, Jean-Marie Hullot. Proofs by Induction in Equational Theories with Constructors. 21^{th} FOCS 1980, pp. 96-107; also in: JCSS 25, 1982, pp. 293-266.

[25] Jean Pierre Jouannaud, Bernard Waldmann. Reductive Conditional Term Rewriting Systems. Conference on Formal Description of Programming Concepts III, 1986, pp. 223-244.

[26] Sam Kamin, Jean-Jacques Levy. Attempts for Generalizing the Recursive Path Ordering. Unpublished Manuscript, Department of Computer Science, University of Illinois, Urbana, Illinois, 1980.

[27] Stéphane Kaplan. Conditional Rewrite Rules. Theoretical Computer Science 33 (1984), pp. 175-193. North-Holland.

[28] Stéphane Kaplan. Positive/Negative Conditional Rewriting. 1^{st} CTRS 1988, LNCS 308. Springer-Verlag, Berlin 1988.

[29] Stéphane Kaplan, Marianne Choquer. On the Decidability of Quasi-Reducibility. EATCS Bulletin 28, 1986.

[30] Deepak Kapur, David R. Musser (1987). Proof by Consistency. Artificial Intelligence 31, pp. 125-157.

[31] Deepak Kapur, David R. Musser (1986). Inductive Reasoning with Incomplete Specifications. Preliminary Report. IEEE symposium on Logic In Computer Science.

[32] Deepak Kapur, Paliath Narendran, Friedrich Otto. On Ground-Confluence of Term Rewriting Systems. Technical Report TR 87-6, Dept. of Computer Science, State Univ. of New York, USA, 1987.

[33] Deepak Kapur, Paliath Narendran, Hantao Zhang. Automating Inductionless Induction. J. Symbolic Computation (1991) 11, pp. 83-111.

[34] Emmanuel Kounalis, Michaël Rusinowitch. On Word Problems in Horn Theories. 9^{th} CADE 1988, LNAI 310. Springer-Verlag, Berlin 1988.

[35] Emmanuel Kounalis, Michaël Rusinowitch. Mechanizing Inductive Reasoning. Proc. of 8^{th} AAAI 1990. AAAI Press/The MIT Press, Menlo Park, Cambridge, London, Vol. 1, pp. 240-245.

[36] Ulrich Kühler. Ein funktionaler und struktureller Vergleich verschiedener Induktionsbeweiser. Diplomarbeit, 1991, .

[37] Peter Padawitz. Horn Logic and Rewriting for Functional and Logic Program Design. MIP-9002, März 1990. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, W-8390 Passau.

[38] David A. Plaisted. Semantic Confluence Tests and Completion Methods. Information and Control 65, 1985, pp. 182-215.

[39] Uday S. Reddy. Term Rewriting Induction. 10^{th} CADE 1990, LNAI 449. Springer-Verlag, Berlin 1990.

[40] Gerd Smolka, Werner Nutt, Joseph A. Goguen, José Meseguer. Order-Sorted Equational Computation. In: H. Ait-Kaci, M. Nivat (eds.). Resolution of Equations in Algebraic Structures, Vol. 2. Academic Press, San Diego CA, 1989.

[41] Christoph Walther. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. 9^{th} CADE 1988, LNAI 310. Springer-Verlag, Berlin 1988.

[42] Christoph Walther. Computing Induction Axioms. LPAR 1992, LNAI 624. Springer-Verlag, Berlin 1992.

[43] Claus-Peter Wirth. Inductive Theorem Proving in Theories specified by Positive/Negative Conditional Equations. Diplomarbeit, 1991, .

[44] Claus-Peter Wirth, Bernhard Gramlich. A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. SEKI-Report SR–92–10 (SFB), May 4, 1992, .

[45] Claus-Peter Wirth, Bernhard Gramlich. A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. 3^{rd} CTRS 1992, LNCS 656. Springer Verlag, Berlin 1993.

[46] Hantao Zhang. Reduction, Superposition and Induction: Automated Reasoning in an Equational Logic. Rensselaer Polytech. Inst., Dept. of Comp. Sci., Troy, NY, PhD thesis, 1988.

[47] Hantao Zhang, Deepak Kapur. First-Order Theorem Proving using Conditional Rewrite Rules. 9^{th} CADE 1988, LNAI 310. Springer-Verlag, Berlin 1988.

[48] Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy. A Mechanizable Induction Principle for Equational Specifications. 9^{th} CADE 1988, LNAI 310. Springer-Verlag, Berlin 1988.