On the confluence of λ-calculus with conditional rewriting

Frédéric Blanqui^{1}, Claude Kirchner^{1}, and Colin Riba^{2}

1 INRIA & LORIA^{⋆} 2 INPL & LORIA

Abstract. The confluence of untyped λ-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of λ-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty’s result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.

1 Introduction

Rewriting [10] and λ-calculus [3] are two universal computation models which are both used, with their own advantages, in programming language design and implementation, as well as for the foundation of logical frameworks and proof assistants. Among other things, λ-calculus allows to manipulate abstractions and higher-order variables, while rewriting is traditionally well suited for defining functions over data-types and for dealing with equality.

Starting from Klop’s work on higher-order rewriting and because of their complementarity, many frameworks have been designed with a view to integrate these two formalisms. This integration has been handled either by enriching firstorder rewriting with higher-order capabilities, by adding to λ-calculus algebraic features or, more recently, by a uniform integration of both paradigms. In the first case, we find the works on combinatory reduction systems [17] and other higher-order rewriting systems [20] each of them subsumed by van Oostrom and van Raamsdonk’s axiomatization of HORS [23]. The second case concerns the more atomic combination of λ-calculus with term rewriting [15, 5] and the last category the rewriting calculus [9, 4].

⋆ UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP, Campus Scientifique, BP 239, 54506 Vandoeuvre-lès-Nancy Cedex, France

Despite this strong interest in the combination of both concepts, few works have considered conditional higher-order rewriting in λ-calculus. This is of particular interest for both computation and deduction. Indeed, conditional rewriting appears to be very convenient when programming with rewrite rules and its combination with higher-order features provides a quite agile background for the combination of algebraic and functional programming. This is also of main use in proof assistants based on the de Bruijn-Curry-Howard isomorphism where, as emphasized in deduction modulo [13, 5], rewriting capabilities for defining functions and proving equalities automatically is clearly of great interest when making large proof developments. Furthermore, while many confluence proofs often rely on termination and local confluence, in some cases, confluence may be necessary for proving termination (e.g. with type-level rewriting or strong elimination [5]). It is therefore of crucial interest to have also criteria for the preservation of confluence when combining conditional rewriting and β-reduction without assuming the termination of the combined relation. In particular, assuming the termination of just one of the two relations is already of interest.

The earliest work on preservation of confluence when combining typed λcalculus and first-order rewriting concerns the simple type discipline [7] and the result has been extended to polymorphic λ-calculus in [8]. Concerning untyped λ-calculus, the result was shown in [19] for left-linear rewriting. It is extended as a modularity result for higher order rewriting in [23]. In [12], it is shown that left-linearity is not necessary provided that terms considered are strongly βnormalizable and are well-formed with respect to the declared arity of symbols, a property that we call here arity-compliance. Higher-order conditional rewriting is studied in [1] and the confluence result relies on joinability of critical pairs, hence on termination of the combined rewrite relation. Another form of higherorder conditional rewriting is considered in [22]. It concerns confluence results for a very general form of orthogonal systems. These systems are related to those presented in Sect. 5. If modularity properties have been investigated in the pure first-order conditional case (e.g. [18, 14]), to the best of our knowledge, there was up to now no result on preservation of confluence when β-reduction is added to conditional rewriting.

In this paper, we study the confluence property of the combination of βreduction with a confluent conditional rewrite system. This of course should rely on a clear understanding of the conditional rewrite relation under use and, as usual, the ways the matching is performed and instantiated conditions are decided are crucial.

So, we start from λ-terms with curried constants and among them we distinguish applicative terms that contain no abstraction and algebraic terms that furthermore have no active variables, i.e. variables occurring in the left-hand side of an application. In this paper, we always consider algebraic left-hand sides. So, rewriting does not use higher-order pattern-matching but just syntactic matching. Furthermore, we consider two rewrite relations induced by a set of conditional rules. →_{A} is the conditional rewrite relation where the conditions are checked without considering β-reduction and →_{B} is the conditional rewrite relation where β-reduction is allowed when evaluating the conditions. Then, we study the confluence of the relations →_{β∪A} and →_{β∪B}, the respective combinations of →_{A} and →_{B} with β-reduction. This is made precise in Sect. 2 and accompanied of relevant examples.

We know that adding β-reduction to a confluent non left-linear algebraic rewriting system results in a non confluent relation. Of course, with conditional rewriting, non-linearity can be simulated by linear systems. Extending the result of Müller [19], we prove in Sect. 3 that confluence of →_{β∪A} follows from confluence of →_{A} when conditional rules are applicative, left-linear and do not allow their condition to test for equality of open terms. Such rules are called semi-closed. We also adapt to conditional rewriting the method of Dougherty [12] and extend it to show that for a large set of weakly β-normalizing terms, the left-linearity and semi-closed hypotheses can be dropped provided the rules are algebraic and terms are arity-compliant.

We then turn in Sect. 4 to the confluence modularity of →_{β∪B} for rules with algebraic right-hand side. In this case, we show that arity-compliance is a sufficient condition to deduce confluence of →_{β∪B} from confluence of →_{β∪A} (hence of →_{A}). This is done first for left-linear semi-closed systems, a restriction that we also show to be superfluous when considering only weakly β-normalizing terms.

The case of non-algebraic rules is handled in Sect. 5. Such rules can contain active variables and abstractions in right-hand sides or in conditions (but still not in left-hand sides). In this case, the confluence of →_{β∪B} no more follows from the confluence of →_{A} nor of →_{β∪A}. We show that the confluence of →_{β∪B} holds under a syntactic condition, called orthonormality ensuring that if two rules overlap at a non-variable position, then their conditions cannot be both satisfied. An orthonormal system is therefore orthogonal, and the confluence of →_{B∪β} follows using usual proof methods.

We assume some familiarity with λ-calculus [3] and conditional rewriting [11, 21] but we recall the main notations in the next section. By lack of place, the main proofs are only sketched here. They are detailed in [6].

2 General definitions

This section introduces the main notions of the paper. We use λ-terms with curried constants.

Definition 1 (Terms). We assume given a set F of function symbols and an infinite set X of variables. The set T of terms is inductively defined as follows:

t, u ∈ T ::= f ∈ F | x ∈ X | tu | λx.t

A term is applicative if it contains no abstraction and algebraic (“not variableapplying” in [19]) if it furthermore contains no subterm of the form xt with x ∈ X. We use t to denote a sequence of terms t_{1}, …, t_{n} of length |t| = n.

As usual, terms are considered modulo α-conversion. Let FV(t) be the set of variables free in t. We denote by tσ the capture-avoiding application of the substitution σ to the term t. By {x ↦ t}, we denote the substitution σ such that x_{i}σ = t_{i}. As usual, positions in a term are strings over {1, 2}. The subterm of t at position p is denoted by t|_{p}. If t is applicative, the replacement of t|_{p} by some term u is denoted by t[u]_{p}. A context is a term with exactly one free occurrence of a distinguished variable []. If C is an applicative context then C[t] stands for C[t]_{p}, where p is the position of [] in C.

A rewrite relation is a binary relation on terms → which is closed by term formation rules : if s → t then λx.s → λx.t, su → tu and us → ut ; and by substitution : s → t implies sσ → tσ. Its inverse is denoted by ←; its reflexive closure by →^{=}; its reflexive and transitive closure by →^{∗}; and its reflexive, symmetric and transitive closure by ↔^{∗}. The joinability relation is ↓ = →^{∗}←^{∗}. The β-reduction relation is the smallest rewrite relation →_{β} such that (λx.s)t →_{β} s{x ↦ t}. A term t →-rewrites (or →-reduces) to u if t →^{∗} u (we omit → when clear from the context). We write →_{R∪S} for the union of the relations →_{R} and →_{S}. We call parallel rewrite relation any reflexive rewrite relation ⊳ closed by parallel application : [s ⊳ s′ & t ⊳ t′] ⇒ st ⊳ s′t′.

We now introduce conditional rewriting. Let us emphasize that we consider first-order syntactical matching.

Definition 2 (Conditional rewriting). A conditional rewrite system R is a set of conditional rewrite rules^{3}:

d_{1} = c_{1} ∧ ⋯ ∧ d_{n} = c_{n} ⊃ l → r

where l is a non-variable algebraic term, d_{i}, c_{i} and r are arbitrary terms and FV(d_{i}, c_{i}, r) ⊆ FV(l). A system is right-applicative (resp. right-algebraic) if all its right-hand sides are applicative (resp. algebraic). A system is applicative (resp. algebraic) if all its rules are made of applicative (resp. algebraic) terms.

The join rewrite relation induced by R is usually defined as →_{A}= ⋃_{i≥0} →_{A_{i}} [21] where →_{A_{0}}= ∅ and for all i ≥ 0, →_{A_{i+1}} is the smallest rewrite relation such that for all rule d = c ⊃ l → r ∈ R, for all substitution σ, if dσ ↓_{A_{i}} cσ then lσ →_{A_{i+1}} rσ. This relation is sometimes called the standard conditional rewrite relation.

We define the β-standard rewrite relation induced by R as →_{B}= ⋃_{i≥0} →_{B_{i}} where →_{B_{0}}= ∅ and for all i ≥ 0, →_{B_{i+1}} is the smallest rewrite relation such that for all rule d = c ⊃ l → r ∈ R, for all σ, if dσ ↓_{B_{i}∪β} cσ then lσ →_{B_{i+1}} rσ.

If →_{A_{i}} is confluent for all i ≥ 0, we say that →_{A} is level confluent. It is shallow confluent when →_{A_{i}}^{∗} and →_{A_{j}}^{∗} commute for all i, j ≥ 0.

Other forms of conditional rewriting appear in the literature [11]. Natural rewriting is obtained by taking ↔_{A}^{∗} instead of ↓_{A} in the evaluation of conditions. Oriented rewriting is obtained by taking →_{A}^{∗}. A particular case of both standard and oriented rewriting is normal rewriting, in which the terms c are closed and in →_{A}-normal form.

3 The symbol = does not need to be interpreted by a symmetric relation.

Examples. We begin by some basic functions on lists.

car (x :: l) → x
car [ ]  → err

cdr (x :: l) → l
cdr [ ]  → err

get l 0 → car l
get l (s n) → get (cdr l) n
len [ ]  → 0
len (x :: l) → s (len l)

filter p [ ]  → [ ]
p x = tt ⊃ filter p (x :: l) → x :: (filter p l)
p x = ff ⊃ filter p (x :: l) → filter p l

Define > with > (s x) 0 → tt, > 0 y → ff and > (s x) (s y) → > x y. We can now define app such that app f n l applies f to the nth element of l. It uses ap as an auxiliary function:

> (len l) n = tt ⊃ app f n l → ap f n l
> (len l) n = ff ⊃ app f n l → err

ap f 0 l → f (car l) :: cdr l
ap f (s n) l → car l :: ap f n (cdr l)

We represent first-order terms as trees with nodes nd y l where y is intended to be a label and l the list of sons.

Positions are lists of integers and occ u t tests if u is an occurrence of t. We define it with occ [ ] t → tt and

> (len l) x = ff ⊃ occ (x :: o) (nd y l) → ff
> (len l) x = tt ⊃ occ (x :: o) (nd y l) → occ o (get l x)

To finish, rep t o s replaces by s the subterm of t at occurrence o. Its rules are occ u t = tt ⊃ rep t o s → re t o s and occ u t = ff ⊃ rep t o s → err. The rules re s [ ] t → s and re (nd y l) (x :: o) s → nd y (app (λz.re z o s) x l) define the function re.

The system Tree that consists of rules defining car cdr, get, len and occ is algebraic. Rules of app and ap are right-applicatives and those for filter contain in their conditions the variable p in active position. This definition of re involves a λ-abstraction in a right hand side. In Sect. 5, we prove confluence of the relation →_{β∪B} induced by the whole system.

3 Confluence of →_{β} with conditional rewriting

In this section, we study the confluence of →_{β∪A}. The simplest result is the preservation of confluence when R can not check arbitrary equalities (Sect. 3.1). In Sect. 3.2, we consider more general systems and prove that the confluence of →_{β∪A} follows from the confluence of →_{A} on terms having a β-normal form of a peculiar kind.

In [19], Müller shows that the union of β-reduction and the rewrite relation →_{A} induced by a left-linear non-conditional applicative system is confluent as soon as →_{A} is. This result is generalized as modularity result for higher-order rewriting in [23].

The importance of left-linearity is known since Klop [16]. We exemplify it with Breazu-Tannen’s counter-example [7]. The rules − x x → 0 and − (s x) x → s 0 are optimization rules for minus. Together with usual rules defining this function, they induce a confluent rewrite relation. With the fixpoint combinators of the λ-calculus, we can build a term Y →_{β}^{∗} s Y. This term makes the application of the two rules above possible on β-reducts of − Y Y, leading to an unjoinable peak : 0 ←_{A} − Y Y →_{β}^{∗} − (s Y) Y →_{A} s 0.

With conditional rewriting, we do not need non-linear matching to distinguish − (s x) x from − x x, since this can be done within the conditions. The previous system can be encoded into a left-linear conditional system with the rules x = y ⊃ − x y → 0 and s x = y ⊃ − x y → s 0. Of course, the relation →_{A} is still confluent. However, the same unjoinable peak starting from − Y Y makes fail the confluence of →_{β∪A}.

There are two ways to overcome the problem: limiting the power of rewriting or limiting the power of β-reduction. The first way is treated in Sect. 3.1, in which we limit the comparison power of conditional rewriting by restricting ourselves to left-linear and semi-closed systems. This can also be seen as a way, from the point of view of rewriting, to isolate the effect of fixpoints: since two distinct occurrences of Y can not be compared, they can be unfolded independently from each other.

Then, in Sect. 3.2, we limit the power of →_{β} by restricting ourselves to sets of terms having a special kind of β-normal-form. This amounts to only consider terms in which fixpoints do not have the ability to modify the result of →_{β∪A}. In fact, it is sufficient that they do not modify the result of →_{β} alone. More precisely, fixpoints are allowed when they are eliminated by head β-reductions.

3.1 Confluence of left-linear semi-closed systems

We now introduce semi-closed systems.

Definition 3 (Semi-closed systems). A system is semi-closed if in every rule d = c ⊃ l → r, each c_{i} is algebraic and closed.

The system Tree of Sect. 2 is left-linear and semi-closed. Given a semi-closed left-linear system, we show that confluence of →_{β∪A} follows from confluence of →_{A}. This follows from a weak commutation of →_{A} and Tait and Martin-Löf β-parallel reduction relation ⊳_{β}, defined as the smallest parallel rewrite relation (Sect. 2) closed by the rule (beta) [3]:

(beta) \frac{s ⊳_{β} s′ t ⊳_{β} t′}{(λx.s)t ⊳_{β} s′\{x ↦ t′\}}

We will use some well known properties of ⊳_{β}. If σ ⊳_{β} σ′ then sσ ⊳_{β} sσ′; this is the one-step reduction of parallel redexes. We can also simulate β-reduction: →_{β}⊆ ⊳_{β} ⊆→_{β}^{∗}. And third, ⊳_{β} has the diamond property: ⊲_{β}⊳_{β} ⊆ ⊳_{β}⊲_{β}. This corresponds to the fact that any complete development of →_{β} can be done in one ⊳_{β}-step.

Müller [19] uses a weaker parallelization of →_{β}: its relation is defined w.r.t. the applicative structure of terms only and does not reduces in one step nested β-redexes. Consequently, it does not enjoy the diamond property on which we rely in Sect. 4. Nested parallelizations (corresponding to complete developments) are already used in [23] for their confluence proof of HORS. However, our method inherits more from [19] than [23], as we use complete developments of →_{β} only, whereas complete developments of →_{β} and of →_{A} are used for the modularity result of [23].

Proposition 4. Let R be a semi-closed, left-linear and right-applicative system and assume that →_{A_{i−1}}^{∗} commutes with →_{β}^{∗}. For any rule d = c ⊃ l → r ∈ R and substitution σ, if u⊲_{β} lσ →_{A_{i}} rσ, then there exists σ′ such that u = lσ′ →_{A_{i}} rσ′ ⊲_{β} rσ.

Proof Sketch. Since l is algebraic and linear, there is a substitution σ′ such that σ ⊳_{β} σ′ and u = lσ′. It follows that rσ ⊳_{β} rσ′ and it remains to show that dσ′ ↓_{A_{i−1}} cσ′. Since lσ →_{A_{i}} rσ, there is v such that dσ →_{A_{i−1}}^{∗} v ←_{A_{i−1}}^{∗} cσ. Thus, dσ ⊳_{β}^{∗} dσ′ and, by assumption, there is v′ such that dσ′ →_{A_{i−1}}^{∗} v′ ⊲_{β}^{∗} v. Since c is algebraic and closed, we have cσ = c and v in β-normal form. Hence, v′ = v and dσ′ ↓_{A_{i−1}} c. □

Lemma 5 (Commutation of →_{A} and ⊳_{β}). If R is a semi-closed left-linear right-applicative system, then ⊲_{β}^{∗} →_{A}^{∗} ⊆ →_{A}^{∗} ⊲_{β}^{∗}.

Proof Sketch. The result follows from the commutation of →_{A_{i}}^{∗} and ⊳_{β}^{∗} for all i ≥ 0. The case i = 0 is trivial. For i > 0, there are three steps. First, we show by induction on the definition of the parallel rewrite relation ⊳_{β} that if u ⊲_{β} s →_{A_{i}} t then there exists v such that u →_{A_{i}}^{∗} v ⊲_{β} t. If u is s this is obvious. If s is an abstraction, the result follows from induction hypothesis (IH) and the context closure of →_{A_{i}} (CC). If s = s_{1}s_{2}, there are two cases: if t = t_{1}t_{2} with s_{k} →_{A_{i}}^{=} t_{k} then we conclude by (IH) and (CC). Otherwise, we use Prop. 4.

Second, use induction on the number of A_{i}-steps to show that ⊲_{β} →_{A_{i}}^{∗} ⊆ →_{A_{i}}^{∗} ⊳_{β}. Finally, to conclude that ⊲_{β}^{∗} →_{A_{i}}^{∗} ⊆ →_{A_{i}}^{∗} ⊲_{β}^{∗}, use an induction on the number of ⊳_{β}-steps. □

A direct application of Hindley-Rosen’s Lemma offers then the preservation of confluence.

Theorem 6 (Confluence of →_{β∪A}). Let R be a semi-closed left-linear rightapplicative system. If →_{A} is confluent then so is →_{β∪A}.

For the system Tree of Sect. 2, the relation →_{A} is confluent. As the rules are left-linear and semi-closed, Theorem 6 applies and →_{β∪A} is confluent.

3.2 Confluence on weakly β-normalizing terms

We now turn to the problem of dropping the left-linearity and semi-closure conditions.

As seen above, fixpoint combinators make the commutation of →_{β}^{∗} and →_{A}^{∗} fail when rewriting involves equality tests between open terms. When using weakly β-normalizing terms, we can project rewriting on β-normal forms (βnf), thus eliminating fixpoints as soon as they are not significant for the reduction.

Hence, we seek to obtain βnf(s) →_{A}^{∗} βnf(t) whenever s →_{β∪A}^{∗} t. This requires three important properties.

First, β-normal forms should be stable by rewriting. Hence, we assume that right-hand sides are algebraic. Moreover, we re-introduce some information from the algebraic framework, giving maximal arities to function symbols in F.

Second, we need normalizing β-derivations to commute with rewriting. This follows from using the leftmost-outermost strategy of λ-calculus [3].

Finally, we need rule conditions to be algebraic. Indeed, consider the rule x b = y ⊃ f x y → a that contains an non-algebraic condition. The relation →_{A} is confluent but a ←_{β∪A}^{∗} f (λx.x) ((λz.z)(λx.x) b) →_{β}^{∗} f (λx.x) b is an unjoinable critical peak.

Definition 7 (Arity-compliance). We assume that every symbol f ∈ F is equipped with an arity α_{f} ≥ 0. A term is arity-compliant if it contains no subterm of the form ft with f ∈ F and |t| > α_{f}. A rule d = c ⊃ l → r is almost arity-compliant if l and r are arity-compliant and l is of the form fl with |l| = α_{f}. A rule is arity-compliant if, furthermore, d and c are arity-compliant. Let U be the set of terms having an arity-compliant β-normal form.

Remark that a higher-order rule (with active variables and abstractions) can be arity-compliant.

Arity-compliance is useful because it prevents collapsing rules from creating β-redexes. For example, the rule id x → x forces the arity of id to be 1. Hence the term id (λx.x) y is not arity-compliant. Moreover it is a β-normal form that →_{A}-reduces to the β-redex (λx.x)y. It is then easy to build an arity-uncompliant term that makes the preservation of confluence to fail. Let Y = ω_{s}ω_{s} with ω_{s} = λx.s x x. The term − (id ω_{s}ω_{s}) (id ω_{s}ω_{s}) is an arity-uncompliant β-normal form. Reducing the id’s leads to − Y Y which is the head of an unjoinable critical peak.

However, we do not assume that every term at hand is arity-compliant. Indeed, a term that has an arity-compliant β-normal form does not need to be arity-compliant itself. More precisely, for a weakly β-normalizing term, the leftmost-outermost strategy (for →_{β}) never evaluates subterms that are not βnormalizing and it follows that such subterms may be arity-uncompliant without disturbing the projection on β-normal forms.

The point is the well-foundedness of the leftmost-outermost strategy for →_{β} on weakly β-normalizing terms [3]. This strategy can be described by means of head β-reductions, that are easily shown to commute with (parallel) conditional rewriting. Any λ-term can be written λx.v a_{0} a_{1} … a_{n} where either v ∈ X ∪F (a) or v is a λ-abstraction (b). We denote by →_{h} the head β-step λx.(λy.b)a_{0}a →_{h} λx.b{y ↦ a_{0}}a. Let s ≻ t iff either s is of the form (b) and s →_{h} t, or s is of the form (a) with n ≥ 1 and t = a_{i} for some i ≥ 0. In the latter case, the free variables of t can be bound in s. Hence, t can be a subterm of a term α-equivalent to s ; for instance λx.fx ≻ y for all y ∈ X.

Lemma 8. Let WN be the set of weakly β-normalizing terms ; (i) if s ∈ WN and s ≻ t then t ∈ WN, (ii) ≻ is well-founded on WN.

It follows that we can reason by well-founded induction on ≻. For all i ≥ 0, we use a nested parallelization of →_{A_{i}}. It corresponds to the one used in [23], that can be seen as a generalization of Tait and Martin-Löf parallel relation. As for ⊳_{β} and →_{β}, in the orthogonal case, a complete development of →_{A_{i}} can be simulated by one step ⊳_{A_{i}}-reduction. This relation is also an adaptation to conditional rewriting of the parallelization used in [12].

Definition 9 (Conditional nested parallel relations). For all i ≥ 0, let ⊳_{A_{i}} be the smallest parallel rewrite relation closed by:

(rule) \frac{d = c ⊃ l → r ∈ R lσ →_{A_{i}} rσ σ ⊳_{A_{i}} θ}{lσ ⊳_{A_{i}} rθ}

Recall that lσ →_{A_{i}} rσ is ensured by dσ ↓_{A_{i−1}} cσ. These relations enjoy some nice properties: (1) →_{A_{i}} ⊆ ⊳_{A_{i}} ⊆ →_{A_{i}}^{∗}, (2) s ⊳_{A_{i}} t ⇒ u{x ↦ s} ⊳_{A_{i}} u{x ↦ t} and (3) [s ⊳_{A_{i}} t & u ⊳_{A_{i}} v] ⇒ u{x ↦ s} ⊳_{A_{i}} v{x ↦ t}. The last one implies commutation of ⊳_{A_{i}} and →_{h}. Commutation of rewriting with head β-reduction has already been coined in [2]. We now turn to the main lemma.

Lemma 10. Let R be an arity-compliant algebraic system. If s ∈ U and s →_{β∪A}^{∗} t, then t ∈ U and βnf(s) →_{A}^{∗} βnf(t).

Proof Sketch. We show by induction on i the property for →_{β∪A_{i}}^{∗}. We denote by (I) the corresponding induction hypothesis. The case i = 0 is trivial. Assume that i > 0. An induction on the number of →_{β∪A_{i}}-steps leads us to prove that βnf(s)⊳_{A_{i}} βnf(t) whenever s⊳_{A_{i}} t and s has an arity-compliant β-normal form. We reason by induction on ≻.

First (1), assume that s is of the form (a). If no rule is reduced at its head, the result follows from induction hypothesis on ≻. Otherwise, there is a rule d = c ⊃ l → r such that s = λx.lσa and t = λx.rθb with lσ⊳_{A_{i}}rθ and dσ ↓_{A_{i−1}} cσ. Since l is algebraic, βnf(s) is of the form λx.lσ′a′ where σ′ = βnf(σ) and a′ = βnf(a). Since βnf(s) is arity-compliant, a′ = ∅, hence a = ∅ and s = λx.lσ. Therefore, because lσ ⊳_{A_{i}} rθ, we have b = ∅ and t = λx.rθ. It remains to show that t has an arity-compliant normal form and that βnf(s) = λx.lσ′ ⊳_{A_{i}} βnf(t). Because l is algebraic, its variables are ≺^{+} l. We can then apply induction hypothesis on σ ⊳_{A_{i}} θ. It follows that θ has an arity-compliant normal form θ′ with σ′ ⊳_{A_{i}} θ′. Since r is algebraic, λx.rθ′ is the (arity-compliant) β-normal form of t. Hence it remains to show that lσ′ ⊳_{A_{i}} rθ′. Because σ′ ⊳_{A_{i}} θ′, it suffices to prove that lσ′ →_{A_{i}} rσ′. Thus, we are done if we show that dσ′ ↓_{A_{i−1}} cσ′. Since d and c are algebraic, βnf(dσ) = dσ′ and βnf(cσ) = cσ′. Now, since d is algebraic and arity-compliant and σ′ is arity compliant, dσ′ is arity-compliant. The same holds for cσ′. Hence we conclude by applying induction hypothesis (I) on dσ ↓_{A_{i−1}} cσ.

Second (2), when s is of the form (b) we head β-normalize it and obtain a term s′ of the form (a) having an arity-compliant β-normal form. Using commutation of ⊳_{A_{i}} and →_{h}, we obtain a term t′ such that s′ ⊳_{A_{i}} t′. Since s ≻^{+} s′, we can reason as in case (1). □

The preservation of confluence is a direct consequence of the projection on β-normal forms.

Theorem 11. Let R be an arity-compliant algebraic system such that →_{A} is confluent. Then, →_{β∪A} is confluent on U.

Comparison with Dougherty’s work. This section is an extension of [12]. We give a further exploration of the idea that preservation of confluence, when using hypothesis on →_{β}, should be independent from any typing discipline for the λ-calculus.

Moreover, we extend its result in three ways. First, we adapt it to conditional rewriting. Second, we allow nested symbols in lhs to be applied to less arguments than their arity. And third, we use weakly β-normalizing terms whose normal forms are arity-compliant ; whereas Dougherty uses the set of strongly normalizing arity-compliant terms which is closed by reduction.

4 Using →_{β} in the evaluation of conditions

The goal of this section is to give conditions on R to deduce confluence of →_{β∪B} from confluence of →_{A}. We achieve this by exhibiting two different criteria ensuring that

→_{β∪B}^{∗} ⊆ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} .  (⋆)

The first case concerns left-linear and semi-closed systems. This holds only on some sets of terms that, after Dougherty [12], we call R-stable, although our definition of stability does not require strong β-normalization (see Sect. 3.2 and Def. 12). This is an extra hypothesis compared to the result of Sect. 3.1. The second case is a direct extension of Lemma 10 to →_{β∪B}. In both cases, we assume the rules to be algebraic and arity-compliant. We are then able to obtain confluence of →_{β∪B} since, in each case, our assumptions ensure that the results of Sect. 3 applies, hence that →_{β∪A} is confluent whenever →_{A} is.

It is important to underline the meaning of (⋆). Given an arity-compliant algebraic rule d = c ⊃ l → r, every β-redex occurring in dσ or cσ also occurs in lσ. Then, (⋆) means that there is a β-reduction starting from lσ that reduces these redexes and produce a substitution σ′ such that lσ →_{β}^{∗} lσ′ →_{A} rσ′ ←_{β}^{∗} rσ. In other words, if the conditions are satisfied with σ and →_{β∪B} (i.e. dσ ↓_{β∪B} cσ), then they are satisfied with σ′ and →_{A} (i.e. dσ′ ↓_{A} cσ′).

We now give some examples of non arity-compliant or non algebraic rules in which, at the same time, (⋆) fails and →_{β∪B} is not confluent whereas →_{β∪A} for (1), (3), (4) and at least →_{A} for (2) is.

(1)  gx → xc  gx = d ⊃ fx → a  fx → b
(2)  xc = d ⊃ fx → a  fx → b
(3)  hx → x  hxc = d ⊃ fx → a  fx → b
(4)  hxy → gxy  gx → x  hxc = d ⊃ fx → a  fx → b

The first and second examples respectively contain a rule with a non algebraic right-hand side and a rule with a non algebraic condition. Examples (3) and (4) use non arity-compliant terms, in the conditional part and in the right-hand side of a rule respectively. For these four examples, the step f(λx.d) →_{B} a is not in →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} and a ←_{B} f(λx.d) →_{B} b is an unjoinable peak.

However, (⋆) is by no means a necessary condition ensuring that →_{β∪B} is confluent when →_{β∪A} so is. In the above examples, confluence of →_{β∪B} can be recovered when adding appropriate rules, yet not restoring (⋆).

As we are interested in deducing the confluence of →_{β∪B} from the confluence of →_{A}, it is more convenient to take in Def. 2 →_{B}= ⋃_{i≥0} →_{B_{i}} with →_{B_{0}}=→_{A} instead of →_{B_{0}}= ∅ (this does not change →_{B} since →_{A}⊆→_{B}).

4.1 Confluence of left-linear systems

In this paragraph, we prove (⋆) provided that rules are arity-compliant, algebraic, left-linear and semi-closed. This inclusion is shown on R-stable sets of terms.

Definition 12 (R-stable sets). Let R be a set of rules. A set S is almost R-stable if it contains only arity-compliant terms, is stable by subterm and βreduction, and C[rσ] ∈ S whenever C[lσ] ∈ S and d = c ⊃ l → r ∈ R. An almost R-stable set S is R-stable if dσ, cσ ∈ S whenever C[lσ] ∈ S and d = c ⊃ l → r ∈ R.

This includes the set of strongly →_{β∪A}-normalizable arity-compliant terms and any of its subset closed by subterm and reduction, by using a simple type discipline for instance.

The inclusion (⋆) is proved by induction on the stratification of →_{B} with →_{B_{0}}=→_{A}. The base case corresponds to →_{β∪A}^{∗} ⊆ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗}, which does not require rule conditions to be algebraic nor arity-compliant.

The previous examples show however that this may fail in presence of arityuncompliant or non-algebraic right-hand sides. Note that the result is proved only on almost R-stable sets of terms. Note also that a set containing a term reducible by the first rule of example (4) above is obviously not stable. Finally, note that the β-expansion steps are needed because rules can be duplicating.

Lemma 13. Let R be a semi-closed left-linear right-algebraic system. On any almost R-stable set of terms, →_{β∪A}^{∗} ⊆ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗}.

Proof Sketch. The proof is in four steps. We begin (1) to show that →_{A} ⊳_{β} ⊆ ⊳_{β} →_{A}^{∗} ⊲_{β}, reasoning by cases on the step ⊳_{β}. This inclusion relies on an important fact of algebraic terms: if s is algebraic and sσ ⊳_{β} v then v ⊳_{β} sσ′ with σ ⊳_{β}^{∗} σ′. From (1), it follows that (2) →_{A}^{∗} ⊳_{β} ⊆ ⊳_{β} →_{A}^{∗} ⊲_{β}^{∗}, by induction on the number of →_{A}-steps. Then (3), we obtain →_{A}^{∗} ⊳_{β}^{∗} ⊆ ⊳_{β}^{∗} →_{A}^{∗} ⊲_{β}^{∗} using an induction on the number of ⊳_{β}-steps and the diamond property of ⊳_{β}. Finally (4), we deduce that (⊳_{β}∪ →_{A})^{∗} ⊆ ⊳_{β}^{∗} →_{A}^{∗} ⊲_{β}^{∗} by induction on the length of (⊳_{β}∪ →_{A})^{∗}. □

We now turn to the main result of this subsection. As seen in the previous examples, rules have to be algebraic and arity-compliant.

Lemma 14. Let R be a semi-closed left-linear algebraic system. On any Rstable set of terms, →_{β∪B}^{∗} ⊆ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗}.

Proof Sketch. The first point is to see that (1) →_{B_{1}}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}. This is done by induction on the number of B_{1}-steps, using Lemma 13. We then deduce (2) →_{β∪B_{1}}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}, by induction on the number of →_{β∪B_{1}}-steps. The result follows from an induction on i showing that →_{B_{i}}⊆→_{B_{1}}. □

Theorem 15. Assume that R is a semi-closed left-linear algebraic system. If →_{A} is confluent, then →_{β∪B} is confluent on any R-stable set of terms.

Recall that in this case →_{β∪A}-confluence follows from →_{A}-confluence by Thm. 6.

4.2 Confluence on weakly β-normalizing terms

This subsection concerns the straightforward extension to →_{B} of the results of Sect. 3.2. The definition of ⊳_{B_{i}} follows the same scheme as the one of ⊳_{A_{i}}; the only difference is that B_{i} is used everywhere in place of A_{i}. It follows that given a rule d = c ⊃ l → r, to have lσ⊳_{B_{i}} rθ, we must have σ⊳_{B_{i}} θ and dσ ↓_{β∪B_{i−1}} cσ. The relations ⊳_{B_{i}} enjoy the same nice properties as the ⊳_{A_{i}}’s.

Lemma 16. Let R be an arity-compliant algebraic system. If s ∈ U and s →_{β∪B}^{∗} t, then t ∈ U and βnf(s) →_{A}^{∗} βnf(t).

The only difference in the proof is that the case i = 0 is now ensured by Lemma 10 (since →_{B_{0}}=→_{A}). The theorem follows easily:

Theorem 17. Let R be an arity-compliant algebraic system such that →_{A} is confluent. Then, →_{β∪B} is confluent on U.

5 Orthonormal systems

In this section, we give a criterion ensuring confluence of →_{β∪B} when conditions and right-hand sides possibly contain abstractions and active variables.

This criterion comes from peculiarities of orthogonality with conditional rewriting. In non-conditional rewriting, a system is orthogonal when it is leftlinear and has no critical pair. A critical pair comes from the superposition of two different rule left-hand sides at non-variable positions. The general definition of orthogonal conditional systems is the same. But, in conditional rewriting, there can be superpositions of two different rules left-hand sides whose conditions cannot be satisfied with the same substitution. Such critical pairs are said infeasible and it could be profitable to consider systems whose critical pairs are all infeasible.

In [21], it is remarked that results on the confluence of natural and normal orthogonal conditional systems should be extended to systems that have no feasible critical pair. But the results obtained this way are not directly applicable since proving unfeasibility of critical pairs may require confluence. In Takahashi’s work [22], conditions can be any predicate P on terms. Confluence is proved with the assumption that they are stable by reduction: if P σ holds and σ → θ, then P θ holds. For the systems studied in this section, stability of conditions by reduction precisely follows from confluence. Hence the results of [22] do not directly apply.

The purpose of this section is to give a syntactic condition on rules that imply unfeasibility of critical pairs, hence confluence.

Definition 18 (Conditional critical pairs). Given two rules d = c ⊃ l → r and d′ = c′ ⊃ l′ → r′, if p is a non-variable position in l and σ is a most general unifier of l|_{p} and l′, then

dσ = cσ ∧ d′σ = c′σ ⊃ (l[r′]_{p}σ, rσ)

is a conditional critical pair. A critical pair d = c ⊃ (s, t) is feasible for →_{A} (resp. →_{B}) if there is a substitution σ such that dσ ↓_{A} cσ (resp. dσ ↓_{β∪B} cσ).

As an example, consider the rules used to define occ in Sect. 2. There is a superposition between the left-hand sides of the last two rules giving the critical peak ff ← occ (x :: o) (nd y l) → occ o (get l x). But a peak of this form can occur only if there are two terms s, t such that tt ←^{∗} ≥ (len s) t →^{∗} ff. Using the stratification of →_{A}, the confluence of →_{A_{i}} implies that this pair is not feasible. Hence the above peak cannot occur with →_{A_{i+1}} and this relation is confluent.

This method can be used on systems with higher-order terms in right-hand sides and conditions, as for example the rules defining app and filter. Hence, it is useful for proving the confluence of →_{β∪B} for systems where this relation does not need to be included in ↔_{β∪A}^{∗}. In this section, we generalize the method and apply it on a class of systems called orthonormal. As in the previous section, we use stratification of →_{B}, but now with →_{B_{0}}= ∅. A symbol f ∈ F is defined if it is the head of a rule left-hand side.

Definition 19 (Orthonormal systems). A system is orthonormal if (1) it is left-linear; (2) in every rule d = c ⊃ l → r, the terms in c are closed βnormal forms not containing defined symbols; and (3) for every critical pair d = c ⊃ (s, t), there exists i ≠ j such that d_{i} = d_{j} and c_{i} ≠ c_{j}.

Note that an orthonormal system is left-linear and semi-closed, but does not need to be arity-compliant or algebraic. Note also that the form of the conditions leads to a normal conditional rewrite relation. The reader can check that the whole system given in Sect. 2 is orthonormal.

We now prove that →_{β∪B} is shallow confluent (i.e. →_{β∪B_{i}}^{∗} and →_{β∪B_{j}}^{∗} commute for all i, j ≥ 0) when R is orthonormal. The first point is that confluence of →_{β∪B_{i}} implies commutation of →_{β}^{∗} and →_{B_{i+1}}^{∗}. The proof is as in Sect. 3.1, except that in a rule d = c ⊃ l → r, c are closed →_{β∪B}-normal forms. The main Lemma concerns commutation of parallel relations of ⊳_{B_{i}} and ⊳_{B_{j}} for all i, j ≥ 0. But here, we use a weak form of parallelization: ⊳_{B_{i}} is simply the parallel closure of →_{B_{i}}. The name of the Lemma is usual for this kind of result with rewriting (see [21]). Write <_{mul} for the multiset extension of the usual ordering on naturals numbers.

Lemma 20 (Parallel Moves). Let R be an orthonormal system. If {n, m} <_{mul} {i, j} implies commutation of →_{β∪B_{n}}^{∗} and →_{β∪B_{m}}^{∗}, then ⊳_{B_{i}} and ⊳_{B_{j}} commute.

Proof Sketch. The key point is the commutation of →_{β∪B_{n}}^{∗} and →_{β∪B_{m}}^{∗} for {n, m} <_{mul} {i, j}. It implies that two rules whose respectives conditions are satisfied with →_{β∪B_{i}}^{∗} and →_{β∪B_{j}}^{∗} are not superposable at non-variable positions. The rest of the proof follows usual schemes (see Sect. 7.4 in [21]). □

Now, an induction on <_{mul} provides the commutation of →_{β∪B_{i}} and →_{β∪B_{j}} for all i, j ≥ 0. Shallow confluence immediately follows.

Theorem 21. If R is an orthonormal system, then →_{β∪B} is shallow confluent.

Hence, the relation →_{β∪B} induced by the system of Sect. 2 is confluent.

6 Conclusion

Our results are summarized in the following table.

§ Terms Lhs  Rhs  Conditions  Result
3.1 T  Linear Applicative  Semi-Closed

→_{A} Confluent ⇒
→_{A∪β} Confluent

3.2 U Arity-Compliant & Algebraic Arity-Compliant & Algebraic

idem

4.1 R-stable Linear Algebraic Semi-Closed & Algebraic

→_{A} Confluent ⇒
→_{B∪β} Confluent

4.2 U Arity-Compliant & Algebraic Arity-Compliant & Algebraic

idem

5  T  Linear  Orthonormal

→_{B∪β} Shallow Confluent

We provide detailed conditions to ensure modularity of confluence when combining β-reduction and conditional rewriting, either when the evaluation of conditions uses β-reduction or when it does not. This has useful applications on the high-level specification side and for enriching the conversion used in logical frameworks or proof assistants, while still preserving the confluence property.

These results lead us to the following remarks and further research points. The results obtained in Sect. 3 and 4 for the standard conditional rewrite systems extend to the case of oriented systems (hence to normal systems) and to the case of level-confluent natural systems. For natural systems, the proofs follow the same scheme, provided that level-confluence of →_{A} is assumed. However, it would be interesting to know if this restriction can be dropped.

Problems arising from non left-linear rewriting are directly transposed to leftlinear conditional rewriting. The semi-closure condition is sufficient to avoid this, and it provides the counter part of left-linearity for unconditional rewriting. As a matter of a fact, it is well known that orthogonal standard conditional rewrite systems are not confluent, but confluence of orthogonal semi-closed standard systems holds. However, two remarks have to be made about this restriction. First, it would be interesting to know if it is a necessary condition and besides, to characterize a class of non semi-closed systems that can be translated into equivalent semi-closed ones. Second, semi-closed terminating standard systems behave like normal systems. But normal systems can be easily translated in equivalent non-conditional systems. Moreover such a translation preserves good properties such as left-linearity and non-ambiguity. As many of practical uses of rewriting rely on terminating systems, semi-closed standard systems may be in practice essentially an intuitive way to design rewrite systems that can be then efficiently implemented by non-conditional rewriting.

An interesting extension of this work consists in adapting to conditional rewriting the axiomatization and the results of [23]. This should leads to a generalization of the higher-order conditional systems of [1].

Acknowledgments. We are quite grateful to the anonymous referees for their constructive and accurate comments and suggestions.

References

[1] J. Avenhaus and C. Loría-Sáenz. Higher order conditional rewriting and narrowing. In Proceedings of the 1st International Conference on Constraints in Computational Logics, volume 845 of LNCS, pages 269–284. Springer Verlag, 1994.

[2] F. Barbanera, M. Fernández, and H. Geuvers. Modularity of Strong Normalisation and Confluence in the Algebraic λ-Cube. Journal of Functional Programming, 7(6):613–660, November 1997.

[3] H.P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. North Holland, 1984. Second edition.

[4] G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure Patterns Type Systems. In Principles of Programming Languages, New Orleans, USA. ACM, 2003.

[5] F. Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures In Computer Science, 15(1):37–92, 2005.

[6] F. Blanqui, C. Kirchner, and C. Riba. On the confluence of lambda-calculus with conditional rewriting. HAL technical report, Oct 2005.

[7] V. Breazu-Tannen. Combining algebra and higher-order types. In 3rd IEEE Symposium on Logic in Computer Science Edinburg (UK), july 1988.

[8] V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation, 114(1):1–29, October 1994.

[9] H. Cirstea and C. Kirchner. The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427–498, May 2001.

[10] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 243–320. North-Holland, 1990.

[11] N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

[12] D.J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251–267, December 1992.

[13] G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33–72, Nov 2003.

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

[15] J.-P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of LICS’91.

[16] J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Center Tracts. CWI, 1980. PhD Thesis.

[17] J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. TCS, 121:279–308, 1993.

[18] A. Middeldorp. Completeness of Combinations of Conditional Constructor Systems. Journal of Symbolic Computation, 17(1):3–21, January 1994.

[19] F. Müller. Confluence of the lambda calculus with left linear algebraic rewriting. Information Processing Letters, 41:293–299, 1992.

[20] T. Nipkow. Higher-order critical pairs. In Proceedings of LICS’91.

[21] E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, April 2002.

[22] M. Takahashi. Lambda-calculi with conditional rules. In TLCA’93, LNCS, pages 406–417. Springer-Verlag, 1993.

[23] V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In LFCS’94, volume 813 of LNCS, 1994.

A Proofs of Section 3.2

We begin by proving the well-foundedness of ≻.

Lemma 22. Let WN be the set of weakly β-normalizing terms. The set WN is stable by ≻ and ≻ is well-founded on WN.

Proof. For the first part, let be s ∈ WN and s ≻ t. If s is of the form (b), the first step of the leftmost-outermost derivation normalizing s is t. Hence t ∈ WN. Otherwise, if t has no β-normal form, then s has no β-normal form.

For the second part, we write #(s) for the number of →_{h}-steps in the leftmost-outermost derivation starting from s and |s| for the size of s. We show that if s ≻ t, then (#(s), |s|) >_{lex} (#(t), |t|). If s is of the form (b), by the first point t ∈ WN. Since s →_{h} t, we have #(s) > #(t). Otherwise, the leftmostoutermost strategy starting from s reduces by leftmost-outermost reductions each a_{i} (1 ≤ i ≤ n). Hence #(s) ≥ #(t). But in this case, t is a proper subterm of s, hence |s| > |t|.

Then, we consider the properties (1)-(3) of the walk relations ⊳_{A_{i}}.

Proposition 23. For all i ≥ 0,

1. →_{A_{i}} ⊂ ⊳_{A_{i}} ⊂ →_{A_{i}}^{∗}.

2. s ⊳_{A_{i}} t ⇒ u{x ↦ s} ⊳_{A_{i}} u{x ↦ t}.

3. [s ⊳_{A_{i}} t & u ⊳_{A_{i}} v] ⇒ u{x ↦ s} ⊳_{A_{i}} v{x ↦ t}.

Proof. The first point is shown by induction on the definition of ⊳_{A_{i}} ; the second by induction on u. For the last one, we also use an induction on ⊳_{A_{i}} in u ⊳_{A_{i}} v. If u is v, the result is trivial. If u ⊳_{A_{i}} v was obtained by parallel application or if u is an abstraction, the result follows from induction hypothesis. Otherwise, u ⊳_{A_{i}} v is obtained by (rule). That is, there is a rule d = c ⊃ l → r ∈ R such that u = lσ, v = rθ, σ ⊳_{A_{i}} θ and lσ →_{A_{i}} rσ. Since →_{A_{i}} is a rewrite relation, we have lσ{x ↦ s} ⊳_{A_{i}} rσ{x ↦ s}. By induction hypothesis, we have σ{x ↦ s} ⊳_{A_{i}} θ{x ↦ t}. Therefore lσ{x ↦ s} ⊳_{A_{i}} rθ{x ↦ t}.

We now turn to the commutation of ⊳_{A_{i}} and →_{h}. This is a direct consequence of the case (3) of the above Proposition.

Lemma 24. For all i ≥ 0, ⊳_{A_{i}} commutes with →_{h}.

Proof. Assume that s ←_{h} λx.(λy.a_{0})a_{1} … a_{p} ⊳_{A_{i}} t. Because rules have nonvariable algebraic left hand-sides, t = λx.(λy.b_{0})b_{1} … b_{p} with for all k ∈ {0, …, p}, a_{k} ⊳_{A_{i}} b_{k}. On the other hand, s = λx.a_{0}{y ↦ a_{1}}a_{2} … a_{p}. It follows from Prop. 23.3 that a_{0}{x ↦ a_{1}} ⊳_{A_{i}} b_{0}{x ↦ b_{1}} (in one step). Hence we have s ⊳_{A_{i}} λx.b_{0}{y ↦ b_{1}}b_{2} … b_{p} ←_{h} t.

u

B Proofs of Section 4.1

We begin by two technical properties. The first one is a generalization of the diamond property of ⊳_{β}.

Proposition 25. Let be n ≥ 0 and assume that s, s_{1}, …, s_{n} are terms such that for all 1 ≤ i ≤ n, s ⊳_{β} s_{i}. Then there is a term s′ such that for all 1 ≤ i ≤ n, s_{i} ⊳_{β} s′.

Proof. The proof is by induction on the structure of s. First, if s is a constant symbol or a variable, then it is a β-normal from and we are done. If s is an abstraction λx.t, then for all 1 ≤ i ≤ n, s_{i} is of the form λx.t_{i} and we conclude by induction hypothesis on t, t_{1}, …, t_{n}. Now assume that s is an application. There are two cases. First, s = tu where t is not an abstraction. Then, for all 1 ≤ i ≤ n, s_{i} is of the form t_{i}u_{i} with t ⊳_{β} t_{i} and u ⊳_{β} u_{i} and we conclude by induction hypothesis. Otherwise, s must be of the form (λx.t)u and for all 1 ≤ i ≤ n, s_{i} is either of the form (λx.t_{i})u_{i} (1) or of the form t_{i}{x ↦ u_{i}} (2). In both cases we have t ⊳_{β} t_{i} and u ⊳_{β} u_{i}. By induction hypothesis, there are two terms t′, u′ such that for all 1 ≤ i ≤ n, t_{i} ⊳_{β} t′ and u_{i} ⊳_{β} u′. Therefore, in case (1), we have (λx.t_{i})u_{i} ⊳_{β} t′{x ↦ u′} and in case (2) t_{i}{x ↦ u_{i}} ⊳_{β} t′{x ↦ u′}. Hence, for all 1 ≤ i ≤ n, s_{i} ⊳_{β} t′{x ↦ u′}.

For the following Proposition, we define O(t, u), the set of occurrences of t in u as : O(t, u) = ε if t = u ; otherwise O(t, u_{1}u_{2}) = 1.O(t, u_{1}) ∪ 2.O(t, u_{2}), O(t, λx.u) = 1.O(t, u) and O(t, x) = O(t, f) = ∅.

Proposition 26. Let s be an algebraic term.

1. If sσ ⊳_{β} v then there is σ′ such that σ ⊳_{β}^{∗} σ′ and v ⊳_{β} sσ′.

2. If sσ ⊳_{β}^{∗} v then there is σ′ such that σ ⊳_{β}^{∗} σ′ and v ⊳_{β}^{∗} sσ′.

Note that s does not needs to be linear.

Proof. 1. Since s is algebraic, every occurrence of β-redex of sσ is of the form p.d where p is the occurrence of a variable x in s and d is an occurrence in σ(x). Therefore, v is of the form

s[t(x, p)]_{{p ; p∈O(x,s) & x∈F V (s)}}

where, for all x ∈ F V (s), for all p ∈ O(x, s), σ(x) ⊳_{β} t(x, p). By Prop. 25, for all x ∈ F V (s), there exists t(x) such that for all p ∈ O(x, s), t(x, p) ⊳_{β} t(x). Hence

v ⊳_{β} s[t(x)]_{{p ; p∈O(x,s) & x∈F V (s)}} .

That is, v ⊳_{β} sσ′ with σ′(x) = t(x).

2. We reason by induction on the number of ⊳_{β}-steps. If sσ = v the result is trivial. Otherwise, sσ ⊳_{β}^{∗} v is sσ ⊳_{β} v′ ⊳_{β}^{∗} v. By (1), there is a substitution σ′ such that sσ ⊳_{β} v′ ⊳_{β} sσ′. By strong confluence of ⊳_{β}, there is a v′′ such that sσ′ ⊳_{β}^{∗} v′′ ⊲_{β}^{∗} v and the length of sσ′ ⊳_{β}^{∗} v′′ is no more than the length of v′ ⊳_{β}^{∗} v. Hence, we can apply induction hypothesis on sσ′ ⊳_{β}^{∗} v′′ and thus obtain σ′′ such that sσ ⊳_{β}^{∗} v ⊳_{β}^{∗} sσ′′.

We now turn to the inclusion →_{βA}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗} on almost R-stable terms. We begin by showing that →_{A} ⊳_{β} ⊆ ⊳_{β} →_{A}^{∗} ⊲_{β}.

Proposition 27. Let R be a semi-closed left-linear right-algebraic system. On any almost R-stable set of terms, →_{A} ⊳_{β} ⊆ ⊳_{β} →_{A}^{∗} ⊲_{β}.

Proof. Let R be the binary relation be such that, for all t, u,

R(t, u) ⇔ ∀s [ s →_{A} t ⊳_{β} u ⇒ ∃s′ t′(s ⊳_{β} s′ →_{A}^{∗} t′ ⊲_{β} t) ]

We have to show that R is reflexive and compatible with terms formations rules, parallel application and with the rule (beta).

Reflexivity of R is trivial. We now prove that R is compatible with termformation rules, parallel application and (beta).

Term-Formation Note that compatibility with parallel application contains compatibility with application. Hence compatibility with context is only compatibility with λ-abstraction. We have to show that if R(t_{1}, u_{1}) holds, then R(λx.t_{1}, λx.u_{1}) holds whenever t_{1} ⊳_{β} u_{1}. So assume R(t_{1}, u_{1}), t_{1} ⊳_{β} u_{1} and let s be such that s →_{A} λx.t_{1} ⊳_{β} λx.u_{1}. Write t for λx.t_{1} and u for λx.u_{1}. If the contractum of the step s →_{A} t is in a proper subterm of t, we have s = λx.s_{1} with s_{1} →_{A} t_{1} and we conclude by assumption and context compatibility of →_{A} and ⊳_{β}. Otherwise, there is a rule d = c ⊃ l → r such that s = lσ and t = rσ. As r is algebraic, by Prop. 26 there is a substitution σ′ such that σ ⊳_{β}^{∗} σ′ and u ⊳_{β} rσ′. By linearity of l, we have lσ ⊳_{β} lσ′. We now show that lσ′ →_{A} rσ′. To this end he have to show that dσ′ ↓_{A} c. But dσ ⊳_{β}^{∗} dσ′ and by Lem. 5 there are terms v such that dσ′ →_{A}^{∗} v ←_{β}^{∗}←_{A}^{∗} c. Because terms in c and right-hand sides of rules are build without abstraction symbols, there cannot be any β-step starting from an →_{A}-reduct of c. Hence dσ′ ↓_{A} c and we are done.

Parallel application We have to show that

[ R(t_{1}, u_{1}) & R(t_{2}, u_{2}) ] ⇒ R(t_{1} t_{2}, u_{1} u_{2})

whenever t_{1} ⊳_{β} u_{1} and t_{2} ⊳_{β} u_{2}. So, assume R(t_{1}, u_{1}), R(t_{2}, u_{2}), and let s be such that s →_{A} t_{1} t_{2} ⊳_{β} u_{1} u_{2} where t_{i} ⊳_{β} u_{i}. Write t for t_{1} t_{2} and u for u_{1} u_{2}. If the contractum of the step s →_{A} t is in a proper subterm of t we can conclude by assumption and context compatibility of →_{A} and ⊳_{β}. Otherwise s = lσ and t = rσ for a rule d = c ⊃ l → r and we conclude as in Case 1.

(beta) rule We have to show that

[ R(t_{1}, u_{1}) & R(t_{2}, u_{2}) ] ⇒ R((λx.t_{1})t_{2}, u_{1}{x ↦ u_{2}})

whenever t_{1} ⊳_{β} u_{1} and t_{2} ⊳_{β} u_{2}. So assume R(t_{1}, u_{1}), R(t_{2}, u_{2}), and let s be such that s →_{A} (λx.t_{1})t_{2} ⊳_{β} u_{1}{x ↦ u_{2}} where t_{i} ⊳_{β} u_{i}. Write t for (λx.t_{1})t_{2} and u for u_{1}{x ↦ u_{2}}. As above, if s →_{A} t, is a rooted rewrite step, we refer to the Case 1. Otherwise, as s is arity-compliant, λx.t_{1} is not the instantiated right hand side of a rule d = c ⊃ l → r. Indeed, if it where, we would have s = f ls_{2} with l = fl. But the term fls_{2} is not arity-compliant, contradicting the hypothesis of stability. So we are in cases where s = (λx.s_{1})t_{2} (resp. (λx.t_{1})s_{2}) with s_{1} →_{A} t_{1} (resp. s_{2} →_{A} t_{2}). In both cases, we conclude by assumption and context compatibility of →_{A} and ⊳_{β}.

Lemma 28. Let R be a semi-closed left-linear right-algebraic system. On any almost R-stable set of terms, →_{β∪A}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}.

Proof. The proof is in three steps.

We first show (1) →_{A}^{∗} ⊳_{β} ⊆ ⊳_{β} →_{A}^{∗} ⊲_{β}^{∗}, by induction on the number of A-steps. Assume that s →_{A}^{∗} t′ →_{A} t⊳_{β} u. By Lemma 27, there are v and v′ such that t′ ⊳_{β} v →_{A}^{∗} v′ ⊲_{β} u. By induction hypothesis, there are s′ and s′′ such that s ⊳_{β} s′ →_{A}^{∗} s′′ ⊲_{β}^{∗} v. Then, by Lemma 5, there is t′′ such that s′′ →_{A}^{∗} t′′ ⊲_{β}^{∗} v′. Thus, s ⊳_{β} s′ →_{A}^{∗} t′′ ⊲_{β}^{∗} u.

We now show (2) →_{A}^{∗} ⊳_{β}^{∗} ⊆ ⊳_{β}^{∗} →_{A}^{∗} ⊲_{β}^{∗}, by induction on the number of ⊳_{β}-steps. Assume that s →_{A}^{∗} t⊳_{β} u′ ⊳_{β}^{∗} u. After (1), there are s′ and t′ such that s⊳_{β} s′ →_{A}^{∗} t′ ⊲_{β}^{∗} u′. By strong confluence of ⊳_{β}, there is v such that t′ ⊳_{β}^{∗} v ⊲_{β}^{∗} u, where t′ ⊳_{β}^{∗} v is no longer than u′ ⊳_{β}^{∗} u. Hence, by induction hypothesis, there are s′′ and t′′ such that s′ ⊳_{β}^{∗} s′′ →_{A}^{∗} t′′ ⊲_{β}^{∗} v. Therefore, s ⊳_{β}^{∗} s′′ →_{A}^{∗} t′′ ⊲_{β}^{∗} u.

We now prove (3) (⊳_{β}∪ →_{A})^{∗} ⊆ ⊳_{β}^{∗} →_{A}^{∗} ⊲_{β}^{∗}, by induction on the length of (⊳_{β}∪ →_{A})^{∗}. Assume that s →_{⊳_{β}∪A} t →_{⊳_{β}∪A}^{∗} u. There are two cases. First, s ⊳_{β} t. This case follows directly from the induction hypothesis. Second, s →_{A} t. By induction hypothesis, there are t′ and u′ such that t ⊳_{β}^{∗} t′ →_{A}^{∗} u′ ⊲_{β}^{∗} u. After (2), there are s′′ and u′′ such that s ⊳_{β}^{∗} s′′ →_{A}^{∗} u′′ ⊲_{β}^{∗} u′. Finally, by Lemma 5, there is t′′ such that u′′ →_{A}^{∗} t′′ and t′⊲_{β}^{∗}. Hence, s ⊳_{β}^{∗} s′′ →_{A}^{∗} t′′ ⊲_{β}^{∗} t.

We conclude by the fact that ⊳_{β}^{∗} =→_{β}^{∗}.

We now turn to the proof of →_{β∪B}^{∗} ⊆ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} on R-stables sets.

Lemma 29. Let R be an arity-compliant semi-closed left-linear algebraic system. On any set of R-stable terms, →_{β∪B}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}.

Proof. We first prove (1) →_{B_{1}}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}. Let R be the binary relation such that for all s, t ∈ T ,

R(s, t) ⇔ [ s →_{B_{1}} t ⇒ s →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} t ] .

We have to show that R is compatible with term-formation rules and that for all d = c ⊃ l → r ∈ R, for all substitution σ, if dσ ↓_{A∪β} cσ then R(lσ, rσ) holds. We only show this latter property. Let d = c ⊃ l → r be a rule and assume that lσ →_{B_{1}} rσ. Then, dσ ↓_{β∪A} cσ. Since c is a closed algebraic term, we have dσ →_{β∪A}^{∗} u ←_{A}^{∗} c with both c and u in β-normal form. Because dσ is stable, we can apply Lemma 28 and obtain v such that dσ →_{β}^{∗} v →_{A}^{∗} u. By Prop. 26, there is σ′ such that v →_{β}^{∗} dσ′. Now, by Lemma 5, dσ′ →_{A}^{∗} u. Therefore, s →_{A} t.

We now prove (2) →_{β∪B_{1}}^{∗}⊆→_{β}^{∗}→_{A}^{∗}←_{β}^{∗}, by induction on the number of β ∪B_{1}- steps. Assume that s →_{β∪B_{1}}^{∗} t →_{β∪B_{1}} u. By induction hypothesis, s →_{β}^{∗} s′ →_{A}^{∗} t′ ←_{β}^{∗} t. There are two cases. First, t →_{β} u. By β-confluence, t′ →_{β}^{∗} u′ ←_{β}^{∗} u. Applying Lem. 28 leads to s′ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} u′ and we get s →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} u. Assume now that t →_{B_{1}} u. From (1) it follows that, t →_{β}^{∗} t′_{2} →_{A}^{∗} u′ ←_{β}^{∗} u. Then, by virtue of β-confluence, t′ →_{β}^{∗} t′′ ←_{β}^{∗} t′_{2}. Commutation of β and A (Lem. 5) gives u′′ such that t′′ →_{A}^{∗} u′′ ←_{β}^{∗} u′. Finally, by Lemma 28, s′ →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} u′′. Therefore, s →_{β}^{∗}→_{A}^{∗}←_{β}^{∗} u.

We then prove by induction on i ≥ 1 that →_{B_{i}}⊆→_{B_{1}}. Let i ≥ 1 and let P_{i} be the binary relation such that for all s, t ∈ T ,

P_{i}(s, t) ⇔ [ s →_{B_{i}} t ⇒ s →_{B_{1}} t ] .

We have to show that P_{i} is compatible with term-formation rules and that for all d = c ⊃ l → r ∈ R, for all substitution σ, if dσ ↓_{A∪β} cσ then P_{i}(lσ, rσ) holds. We only show this latter property. Let d = c ⊃ l → r be a rule and assume that lσ →_{B_{i}} rσ. Then, dσ ↓_{β∪B_{i−1}} cσ. By induction hypothesis and since c is a closed algebraic term, we have dσ →_{β∪B_{1}}^{∗} u ←_{A}^{∗} c with both c and u in β-normal form. By (2), dσ →_{β}^{∗}→_{A}^{∗} u ←_{A} c. Therefore, lσ →_{B_{1}} rσ.

Theorem 30. Assume that R is an arity-compliant semi-closed left-linear algebraic system. If →_{A} is confluent then →_{β∪B} is confluent on any set of R-stable terms.

Proof. Let S be a stable set of terms and let s ∈ S such that u ←_{β∪B}^{∗} s →_{β∪B}^{∗} t. By lemma 29, there are u′, s′_{1}, s′_{2} and t′ such that u →_{β}^{∗} u′ ←_{A}^{∗} s′_{1} ←_{β}^{∗} s and s →_{β}^{∗} s′_{2} →_{A}^{∗} t′ ←_{β}^{∗} t. In other words, u′ ↔_{β∪A}^{∗} t′. Since A is confluent, by Theorem 6, there is s′′ such that u →_{β}^{∗} u′ →_{β∪A}^{∗} s′′ ←_{β∪A}^{∗} t′ ←_{β}^{∗} t. We conclude by the fact that →_{A}⊆→_{B}.

C Proofs of Section 5

We begin by the commutation of →_{β}^{∗} and →_{B_{i}}^{∗}.

Lemma 31. If R is an orthonormal system and →_{β∪B_{i}} is confluent then →_{B_{i+1}}^{∗} and →_{β}^{∗} commute.

Proof. The proof follows the lines of the proof of Lemma 5. It also uses the relation ⊳_{β} defined in Sect. 3. We just prove that if d = c ⊃ l → r is a rule such that u ⊲_{β} lσ →_{B_{i+1}} rσ then there is a v such that u →_{B_{i+1}}^{∗} v ⊲_{β} rσ. As l is a non variable linear algebraic term, there is a substitution σ′ such that σ ⊳_{β} σ′ and lσ ⊳_{β} lσ′ = u. Therefore, rσ ⊳_{β} rσ′. It remains to show that lσ′ →_{B_{i+1}} rσ′. Recall that dσ →_{β∪B_{i}}^{∗} c. As dσ →_{β}^{∗} dσ′, by hypothesis, there is v such that dσ′ →_{β∪B_{i}}^{∗} v ←_{β}^{∗} c. But c are β-normal forms, hence v = c. Therefore, lσ′ →_{B_{i+1}} rσ′ ⊲_{β} rσ.

We now turn to parallel moves. Lemma 20 is decomposed into Lemmas 32 and 33. We denote by →^{=} the reflexive closure of a rewrite relation →.

Lemma 32. Let R be an orthonormal system and i, j ≥ 0. Assume that, for all n, m such that {n, m} <_{mul} {i, j} diagram (i) commutes. Let d = c ⊃ l → r be a conditional rewrite rule in R. Then, diagram (ii) commutes.

\begin{matrix}\xymatrix{s \ar[r]^{β∪B_{n}}_{∗} \ar[d]_{β∪B_{m}}^{∗} & t \ar@{.>}[d]^{β∪B_{m}}_{∗} \\ u \ar@{.>}[r]_{β∪B_{n}}^{∗} & v} & \xymatrix{lσ \ar[r]^{B_{i}} \ar[d]_{⊳_{B_{j}}} & rσ \ar@{.>}[d]^{⊳_{B_{j}}} \\ u \ar@{.>}[r]_{B_{i}}^{=} & v} \\ (i) & (ii) \end{matrix}

Proof. The results holds if i = 0 since →_{B_{0}}= ∅. If j = 0, then u = lσ and take v = rσ.

Assume that i, j > 0 and write q_{1}, …, q_{n} for the (disjoint) occurrences in lσ of the redexes contracted in lσ ⊳_{B_{j}} u. Therefore, for all k, 1 ≤ k ≤ n, there exists a rule ρ_{k} : d_{k} = c_{k} ⊃ l_{k} → r_{k} and a substitution θ_{k} such that lσ|_{q_{k}} = l_{k}θ_{k}. Thus, u = lσ[r_{1}θ_{1}]_{q_{1}} … [r_{n}θ_{n}]_{q_{n}}. It is possible to rename variables and assume that ρ, ρ_{1}, … ρ_{n} have disjoint variables. Therefore, we can take σ ≡ θ_{1} ≡ ⋯ ≡ θ_{n}.

Assume that there is a non-variable superposition, i.e. that a q_{k} is a non variable occurrence in l. Hence rules ρ and ρ_{k} forms an instance of a critical pair d′μ = c′ ⊃ (l[r_{k}]_{q_{k}}μ, rμ) and there exists a substitution μ′ such that σ = μμ′. By definition of orthonormal systems, |d′μ| ≥ 2 and there is m ≠ p such that c′_{m} ≠ c′_{p} and d′_{m}μ = d′_{p}μ. Let us write h for max(i, j) − 1. As d′_{m}μ = d′_{p}μ we have d′_{m}σ = d′_{p}σ and it follows that c′_{m} ←_{β∪B_{h}}^{∗} d′_{m}σ = d′_{p}σ →_{β∪B_{h}}^{∗} c′_{p}. But {h, h} <_{mul} {i, j} and by assumption →_{β∪B_{h}} is confluent. Therefore we must have c′_{m} ↓_{β∪B_{h}} c′_{p}. But it is not possible since c′_{m} and c′_{p} are distinct normal forms. Hence, conditions of ρ and ρ_{k} can not be both satisfied by σ and →_{β∪B_{h}} and it follows that there is no non-variable superposition.

Therefore, each q_{k} is of the form u_{k}.v_{k} where l|_{u_{k}} is a variable x_{k}. Let σ′ be such that σ′(x_{k}) = σ(x_{k})[r_{k}σ]_{v_{k}} and σ′(y) = σ(y) if y ≢ x_{k} for all 1 ≤ k ≤ n. Then, lσ ⊳_{B_{j}} lσ′ and by linearity of l, u = lσ′. Furthermore, rσ ⊳_{B_{j}} rσ′. We now show that lσ′ →_{B_{i}} rσ′. We have dσ →_{β∪B_{i−1}}^{∗} c and dσ →_{B_{j}}^{∗} dσ′. As i, j > 0, we have {i − 1, j} <_{mul} {i, j}. Therefore, by assumption →_{β∪B_{i−1}}^{∗} and →_{β∪B_{j}}^{∗} commute and there exist terms c′ such that dσ′ →_{β∪B_{i−1}}^{∗} c′ ←_{β∪B_{j−1}}^{∗} c. But as terms in c are →_{β∪B}-normal forms, we have c′ = c and it follows that lσ′ →_{B_{i}} rσ′.

Lemma 33. Let R be an orthonormal system and i, j ≥ 0. Diagram (iii) commutes if and only if for all rule d = c ⊃ l → r, diagrams (iv) and (v) commute.

\begin{matrix}\xymatrix{s \ar[r]^{⊳_{B_{i}}} \ar[d]_{⊳_{B_{j}}} & t \ar@{.>}[d]^{⊳_{B_{j}}} \\ u \ar@{.>}[r]_{⊳_{B_{i}}} & v} & \xymatrix{lσ \ar[r]^{B_{i}} \ar[d]_{⊳_{B_{j}}} & rσ \ar@{.>}[d]^{⊳_{B_{j}}} \\ u \ar@{.>}[r]_{B_{i}}^{=} & v} & \xymatrix{lσ \ar[r]^{B_{j}} \ar[d]_{⊳_{B_{i}}} & rσ \ar@{.>}[d]^{⊳_{B_{i}}} \\ u \ar@{.>}[r]_{B_{j}}^{=} & v} \\ (iii) & (iv) & (v) \end{matrix}

Proof. The “only if” statement is trivial. For the “if” case, let s, t, u be three terms such that u ⊲_{B_{j}} s ⊳_{B_{i}} t. If s is t (resp. u), then take v = u (resp. v = t). Otherwise, we reason by induction on the structure of s. If there is a rooted reduction, we conclude by commutation of diagrams (iv) and (v). Now assume that both reductions are nested. If s is an abstraction, we conclude by induction hypothesis. Otherwise s is an application s_{1}s_{2}, and by assumption u = u_{1}u_{2} and t = t_{1}t_{2} with u_{k} ⊲_{B_{j}} s_{k} ⊳_{B_{i}} t_{k}. In this case also we conclude by induction hypothesis.

We now turn to the main result with orthonormal systems.

Theorem 34. If R is an orthonormal system then →_{β∪B} is shallow confluent.

Proof. By induction on <_{mul}, we show the commutation of →_{β∪B_{i}}^{∗} and →_{β∪B_{j}}^{∗} for all i, j ≥ 0. The least unordered pair {i, j} with respect to <_{mul} is {0, 0}. As →_{β∪B_{0}}=→_{β} by definition, this case holds by confluence of β.

Now, assume that i > 0 and that the commutation of →_{β∪B_{n}}^{∗} and →_{β∪B_{m}}^{∗} holds for all n, m with {n, m} <_{mul} {i, 0}. As {i − 1, i − 1} <_{mul} {i, 0}, →_{β∪B_{i−1}} is confluent and the commutation of →_{β∪B_{i}}^{∗} and →_{β∪B_{0}}^{∗} (=→_{β}^{∗}) follows from lemma 31.

The remaining case is when i, j > 0. Using the induction hypothesis, from Lemma 32 and 33, we obtain commutation of ⊳_{B_{i}} and ⊳_{B_{j}}, which in turn implies commutation of →_{B_{i}}^{∗} and →_{B_{j}}^{∗}. Now, as {i − 1, i − 1} <_{mul} {i, j}, by Lemma 31, →_{β}^{∗} and →_{B_{i}}^{∗} commute. This way, we also obtain the commutation of →_{β}^{∗} and →_{B_{j}}^{∗}. Then, the commutation of →_{β∪B_{i}}^{∗} and →_{β∪B_{j}}^{∗} easily follows.