On the confluence of lambda-calculus with conditional rewriting

Frédéric Blanqui (INRIA) ^{∗} Claude Kirchner (INRIA) ^{†}

Colin Riba (LIP - ENS Lyon) ^{‡}

February 20, 2009

The confluence of untyped λ-calculus with unconditional rewriting is now well understood. 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 betareduction 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.

∗FIT 3-604, Tsinghua University, Haidian District, Beijing 100084, China †INRIA Bordeaux - Sud-Ouest, Bât. A29, 351 cours de la Libération, 33405 Talence, France ‡UMR 5668 CNRS ENS-Lyon UCBL INRIA, 46 allée d’Italie, 69364 Lyon Cedex 7, France

Contents

1 Introduction  3
2 Lambda-calculus and conditional rewriting  5
2.1 Terms and rewrite relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Lambda-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.3 Conditional rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.4.1 Coherence of lambda-calculus with surjective pairing . . . . . . . . . . . . 12
2.4.2 A term manipulation system . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.5 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3 Confluence: from unconditional to conditional rewriting  14
3.1 Confluence of beta-reduction with unconditional rewriting . . . . . . . . . . . . . 15
3.1.1 Left-linear rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.1.2 Strongly beta-normalizing terms . . . . . . . . . . . . . . . . . . . . . . . 16
3.2 Orthogonal conditional rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.3 Overview of the results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4 Confluence of beta-reduction with conditional rewriting  18
4.1 Confluence for left-linear semi-closed systems . . . . . . . . . . . . . . . . . . . . 19
4.2 Confluence on weakly beta-normalizing terms . . . . . . . . . . . . . . . . . . . . 22
5 Using beta-reduction in the evaluation of conditions  26
5.1 Confluence for left-linear semi-closed systems . . . . . . . . . . . . . . . . . . . . 28
5.1.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5.1.2 Confluence of beta-reduction with beta-conditional rewriting . . . . . . . 34
5.2 Confluence on weakly beta-normalizing terms . . . . . . . . . . . . . . . . . . . . 35
6 Orthonormal systems  36
7 Conclusion  40

1 Introduction

Rewriting [DJ90] and λ-calculus [Bar84] 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 first-order 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 [KOR93] and other higher-order rewriting systems [Wol93, Nip91] each of them subsumed by van Oostrom and van Raamsdonk’s axiomatization of HORSs [OR94], and by the every expressive framework of CCERSs [GKK05]. The second case concerns the more atomic combination of λ-calculus with term rewriting [JO91, Bla05] and the last category the rewriting calculus [CK01, BCKL03].

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 Curry-Howard-de Bruijn isomorphism where, as emphasized in deduction modulo [DHK03, Bla05], 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 [Bla05]). 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 firstorder rewriting concerns the simple type discipline [BT88] and the result has been extended to polymorphic λ-calculus in [BTG94]. Concerning untyped λ-calculus, the result was shown in [Mül92] for left-linear rewriting. It is extended as a modularity result for higher-order rewriting in [OR94]. In [Dou92], 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 [ALS94] and the confluence result relies on joinability of critical pairs, hence on termination of the combined rewrite relation. An approach closer to ours is taken with a form of conditional λ-calculus in [Tak93], and with CCERSs in [GKK05]. In both cases, confluence relies on a form of conditional orthogonality. However, in these works, conditions are abstract predicates on terms, and confluence is achieved by assuming that the satisfaction of these predicates is preserved by reduction. These results do not directly apply in our case, since proving that the satisfaction of conditions is preserved by reduction is actually the most difficult task for confluence, and this requires a precise knowledge of the shape of the conditions. These systems are related to those presented in Section 6. Our results can rather be seen as a form of modularity properties. Concerning confluence of unconditional term rewriting, the early work of [Toy87] has been extended to the higher-order case in [OR94]. In the case of conditional rewriting, if modularity properties have been investigated in the pure first-order setting (e.g. [Mid91, Gra96]), to the best of our knowledge, there was up to now no result on the preservation of confluence for the combination with β-reduction.

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 way matching is performed and conditions are checked is crucial. We always consider left-hand sides without abstractions. So, rewriting is not in need of higher-order pattern-matching but just relies on syntactic matching.

We begin in Section 2 by presenting our notations and some basic facts on λ-calculus and conditional rewriting. We start from λ-calculus and discuss, via Böhm’s theorem, the need of enriching its syntax with symbols defined by rewrite rules. We then present the different kinds of conditional rewriting considered in this paper. We are interested in join conditional rewriting: the conditions of rewrite rules are evaluated by testing the joinability of terms. Given a conditional rewrite system, we consider two conditional rewrite relations, whether β-reduction is allowed or not in the evaluation of conditions. The case where β-reduction is allowed in the conditions is termed β-conditional rewriting. We also discuss the particular case of normal rewriting, i.e. when one side of the conditions is made of terms in normal form. We then give two examples of conditional rewrite system. The first one recalls the use of conditional rewriting in the study of λ-calculus with surjective pairing [Vri89]. The second one is a term manipulation system inspired from a program of [Hue86]. We conclude this section by some basic material on confluence.

In Section 3 we state precisely the known results from which this paper starts and give a short overview of our results. The general goal of this paper is to give sufficient conditions for the confluence of β-reduction with β-conditional rewriting (i.e. with β-steps allowed in the evaluation of conditions). Our main objective is the preservation of confluence, that is, given a conditional rewrite system, to get the confluence β-conditional rewriting combined with β-reduction assuming the confluence of conditional rewriting. Our approach is to generalize known results on the combination of β-reduction with unconditional rewriting. We present in Section 3.1 the two different cases we start with: Müller’s result [Mül92] for left-linear rewriting, and Dougherty’s result [Dou92] for algebraic rewriting on strongly β-normalizing terms respecting some arity conditions (called arity compliance). In each case, we will first consider the case of β-reduction with conditional rewriting (when β-reduction is not allowed in the evaluation of conditions) and then extend these results to β-conditional rewriting. However, Example 5.2 shows that for βconditional rewriting, we can not go beyond algebraic rewriting with arity conditions. In order to handle rewrite rules which can contain active variables and abstractions in right-hand sides or in conditions, we build on orthogonal conditional rewriting. Known results on the confluence of orthogonal for normal algebraic conditional rewriting are discussed in Section 3.2. We conclude this section by an informal overview of our results. They are summarized in Figure 1, page 6.

The last three sections contain the technical contributions of the paper. We begin in Section 4 by extending Müller’s and Dougherty’s result to conditional rewriting combined with β-reduction. Müller’s result [Mül92] assumes the left-linearity of rewrite rules. Of course, with conditional rewriting, non-linearity can be simulated by linear systems. Extending the result of Müller [Mül92], we prove in Section 4.1 that the confluence of conditional rewriting combined to β-reduction follows from the confluence of conditional rewriting when conditional rules are applicative, left-linear and semi-closed, which means that the conditions of rules cannot test for equality of open terms. In Section 4.2 we adapt Dougherty’s method [Dou92] to conditional rewriting and extend it to show that for a large set of weakly β-normalizing terms, the left-linearity and semi-closure hypotheses can be dropped provided that rules are algebraic and terms are arity compliant.

We then turn in Section 5 to the confluence of β-conditional rewriting combined with βreduction. We show in Example 5.2 that confluence is in general not preserved with non-algebraic rules. When rules are algebraic, we show that arity compliance is a sufficient condition to deduce the confluence of β-conditional rewriting combined with β-reduction from the confluence of conditional rewriting alone. This is done first for left-linear semi-closed systems in Section 5.1, a restriction that we also show to be superfluous when considering only weakly β-normalizing terms (Section 5.2).

The case of non-algebraic rules is handled in Section 6. 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 β-conditional rewriting combined with β-reduction does not follow anymore from the confluence of conditional rewriting. We show that confluence 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 an orthogonal system whose orthogonality follows from the confluence of the rewrite relation.

This paper is an extended version of [BKR06]. We assume familiarity with λ-calculus [Bar84] and conditional rewriting [DO90, Ohl02]. We recall the main notions in the next section.

2 Lambda-calculus and conditional rewriting

In this section we present the tools used in this paper and recall some well-known facts.

2.1 Terms and rewrite relations

We consider λ-terms with curried function symbols. Among them we distinguish applicative terms that do not contain abstractions, and algebraic terms that are applicative terms with no variable in active position.

Definition 2.1 (Terms) Let Σ be a set of function symbols and X be a set of variables.

(i) The set Λ(Σ) of λ-terms is defined by the grammar

t, u ∈ Λ(Σ) ::= x | λx.t | t u | f ,

where x ∈ X and f ∈ Σ. We denote by Λ the set Λ(∅) of pure λ-terms.

(ii) The set of applicative terms is defined by the grammar

t, u ::= x | t u | f .

(iii) The set of algebraic terms is defined by the grammar

t ::= x | f t_{1} …t_{n} .

As usual, λ-terms are considered equal modulo α-conversion. We denote by FV(t) the set of variables occurring free in the term t. A term is closed if it has no free variables and open otherwise, it is linear if each of its free variables occurs at most once. Given h ∈ X ∪ Σ, we write h t⃗ for h t_{1} …t_{n} and let |t⃗| =_{def} n. Similarly, we write λx⃗.t for λx_{1}….λx_{n}.t.

§ Left-Hand Sides Right-Hand Sides Conditions Terms

Result

4.1 Algebraic & Linear Applicative No equality tests between open terms (Semi-closed, Def. 4.2)

All (Λ(Σ))

)_{R} Confluent =} )_{β∪R} Confluent (Thm. 4.6)

4.2 Algebraic & Respect an arity a (Def. 4.8)

Algebraic & Respect the arity a Algebraic & Respect the arity a

Weakly β-normalizing & βnf respect the arity a (AN_{a}, Def. 4.9)

)_{R} Confluent =} )_{β∪R} Confluent (Thm. 4.15)

5.1 Algebraic & Linear & Respect an arity a (Def. 4.8)

Algebraic & Respect the arity a Algebraic & Respect the arity a & No equality tests between open terms (Semi-closed, Def. 4.2)

Respect the arity a (Conditionally (R, a)-stable, Def. 5.5)

)_{R} Confluent =} )_{β∪R(β)} Confluent (Thm. 5.10)

5.2 Algebraic & Respect an arity a (Def. 4.8)

Algebraic & Respect the arity a Algebraic & Respect the arity a

Weakly β-normalizing & βnf respect the arity a (AN_{a}, Def. 4.9)

)_{R} Confluent =} )_{β∪R(β)} Confluent (Thm. 5.12)

6 Algebraic & Linear Orthonormal (Def. 6.2)

All (Λ(Σ))

)_{β∪R(β)} Shallow Confluent (Thm. 6.7)

Figure 1: Overview of the results. Algebraic and applicative terms are defined in Def. 2.1 Example 2.2 Intuitively, an algebraic term is a curried first-order term with no arity constraint on symbols. For instance the terms filter and filterp x l are algebraic, as well as filterp x l y z. An applicative term is an algebraic term which may contain variables in head position, such as x filter. The λ-term λx.x is not applicative (and thus not algebraic).

A lot of proofs of this paper are made by induction on the structure of λ-terms. However, it is often not convenient to reason directly on their syntax as given by the productions of Λ(Σ). For instance, knowing that a term t is an application, say t = u v, gives little information on its behavior: we do not know whether u is an abstraction, in which case t is a β-redex, or whether it is an algebraic term, in which case t may be the instantiated left-hand side of a rewrite rule. It it is therefore useful to have an induction principle on λ-terms which makes apparent more informations on their structure. This is provided by the following well-known lemma, due to Wadsworth [Wad71].

Lemma 2.3 ([Wad71]) Any λ-term t ∈ Λ(Σ) can be uniquely written in one of the following forms:

λx_{1}….λx_{m}.v a_{1} …a_{n}  (a)
or λx_{1}….λx_{m}.(λy.b) a_{0} a_{1} …a_{n}  (b)

where n, m ≥ 0 and v ∈ X ∪ Σ.

A substitution is a map σ : X ) Λ(Σ) of finite domain. We denote by tσ the capture-avoiding application of the substitution σ to the term t. If σ is the substitution which maps x_{i} to u_{i} for all i ∈ {1, …, n}, then we may write t[u_{1}/x_{1}, …, u_{n}/x_{n}] instead of tσ.

Definition 2.4 (Rewrite Relations) A rewrite relation is a binary relation ) on Λ(Σ) closed under the following rules, where σ is a substitution:

(Abs) \frac{t ) u}{λx.t ) λx.u}  (App_{L}) \frac{t ) u}{t v ) u v}  (App_{R}) \frac{t ) u}{v t ) v u}  (Subst)\frac{t ) u}{tσ ) uσ}

We denote by )^{+} the transitive closure of ), by )^{=} its reflexive closure, by )^{∗} its reflexive and transitive closure, by ( its inverse and by ⌊ its reflexive symmetric and transitive closure. We write t ] u if there exists v such that t )^{∗} v (^{∗} u and t )^{k} u if t )^{∗} u in at most k steps.

Given two rewrite relations )_{A} and )_{B}, we let )_{A∪B} =_{def} )_{A} ∪ )_{B}. We say that a term t is an A-normal form if there is no u such that t )_{A} u. We let SN_{A}, the set of strongly A-normalizing terms, be the set of terms on which the relation )_{A} is well-founded and we let WN_{A}, the set of weakly A-normalizing terms, be the set of terms which rewrite to an A-normal form.

Rewrite relations ) satisfy the following property: for all t, u, v ∈ Λ(Σ),

if t ) u then v[t/x] )^{∗} v[u/x] .

In the following, we will often use a stronger property: for all t, u, v ∈ Λ(Σ),

if t ) u then v[t/x] ) v[u/x] .

This is in general false with rewrite relations, but this holds with parallel rewrite relations.

Definition 2.5 (Parallel Rewrite Relations) A parallel rewrite relation is a rewrite relation ⊳ closed under the rules

(⊳Var) \overline{x ⊳ x}  (⊳Symb) \overline{f ⊳ f}  (⊳App) \frac{t_{1} ⊳ u_{1}  t_{2} ⊳ u_{2}}{t_{1} t_{2} ⊳ u_{1} u_{2}}

Note that given a parallel rewrite relation ⊳, we have λx.t ⊳ λx.u if t ⊳ u, since by definition parallel rewrite relations are rewrite relations.

Given a rewrite relation ) and two substitutions σ and σ′, we write σ ) σ′ if σ and σ′ have the same domain and σ(x) ) σ′(x) for all x ∈ Dom(σ).

Proposition 2.6 If ⊳ is a parallel rewrite relation on Λ(Σ) then σ ⊳ σ′ implies vσ ⊳ vσ′.

Proof. By induction on v.

v ∈ X ∪ Σ. If v = x ∈ Dom(σ) then vσ = σ(x) ⊳ σ′(x) = vσ′. Otherwise, vσ = v ⊳ v = vσ′ thanks to the rules (⊳Var) and (⊳Symb).

v = v_{1} v_{2}. By induction hypothesis we have v_{i}σ ⊳ v_{i}σ′ for all i ∈ {1, 2}, and we conclude by the rule (⊳App).

v = λx.v_{1}. By induction hypothesis.

In particular, if Dom(σ) ∩ FV(v) = ∅ then v ⊳ v: parallel rewrite relations are reflexive.

2.2 Lambda-calculus

λ-calculus is characterized by β-reduction. This is the smallest rewrite relation )_{β} on Λ(Σ) such that

(λx.t)u )_{β} t[u/x] .

In order to understand our motivations for studying the combination of λ-calculus with (conditional) rewriting, let us recall some facts about pure λ-calculus. It is well-known that integers can be coded within pure λ-calculus. An example of such coding is that of Church’s numerals. The Zero and Succ functions are represented by the following terms:

Zero =_{def} λx.λf.x and Succ =_{def} λn.λx.λf.f (n x f) .

We can code iteration with the term Iter x y z =_{def} z x y, and for all n, u, v ∈ Λ we have

\begin{matrix}Iter u v Zero  = & (λxf.x) u v  )_{β}^{2} & u \\ Iter u v (Succ n) = & (λxf.f (n x f)) u v )_{β}^{2} & v (n u v) = v (Iter u v n) . \end{matrix}

However, recursion cannot be implemented in constant time (see for instance [Par89]): there is no term Rec x y z such that there is k ∈ ℕ such that for all u, v, n ∈ Λ,

Rec u v Zero )_{β}^{k} u and Rec u v (Succ n) )_{β}^{k} v (Rec u v n) n .

In particular, there is no coding of the predecessor function for Church’s numerals in constant time. This suggests that practical utilizations of the λ-calculus may require extensions of βreduction. At this point it is interesting to recall Böhm’s theorem. It states that any proper extension of βη-conversion on the set of weakly β-normalizing pure λ-terms is inconsistent.

Theorem 2.7 (Böhm [Böh68]) Let )_{η} be the smallest rewrite relation on Λ such that λx.t x )_{η} t if x ∉ FV(t). If ≃ is an equivalence relation on Λ which is stable by contexts, contains ⌊_{βη} and such that ≃ \ ⌊_{βη} contains a pair of weakly β-normalizing terms, then for all t, u ∈ Λ we have t ≃ u.

This theorem suggests to find extensions of β-reduction operating on extensions of the set of pure λ-terms Λ. A possibility, that we consider in this paper, is to work with function symbols f ∈ Σ defined by rewrite rules.

2.3 Conditional rewriting

In this paper, we are interested in conditional rewriting. The following example introduces the main ideas. Consider lists build from the empty list nil and the constructor cons. We use the symbols true and false to represent the boolean values "true" and "false". We would like to define, via rewriting, a function filter such that

— filterp nil rewrites to nil,

— filterp (const ts) rewrites to const (filterp ts) if p t rewrites to true, and

— filterp (const ts) rewrites to filterp ts if p t rewrites to false. This specification can be written using conditional rewrite rules (⊃ reads implies):

filter p nil  ) nil
p x = true ⊃ filter p (cons x xs) ) cons x (filter p xs)
p x = false ⊃ filter p (cons x xs) ) filter p xs

(1)

If we try to define a rewrite relation ) that corresponds to our specification, we get that

filter p (cons t ts) ) cons t (filter p ts) if p t )^{∗} true .  (2)

In other words, to define ) in the step

filter p (cons t ts) ) cons t (filter p ts) ,

we need to test if p t )^{∗} true, hence to use the relation ). This circularity can be broken off by using an inductive definition of conditional rewriting: the relation ) is stratified in relations ()_{i})_{i∈ℕ}. The correctness of the definition is ensured by Tarski’s fixpoint theorem, which can be applied because, when replacing the symbol = by )^{∗} in (1), the obtained formula is positive in ) (it is in fact a Horn clause).

We now turn to formal definitions. Definition 2.8 (Conditional Rewrite Rules) A conditional rewrite rule is an expression of the form

d_{1} = c_{1} ∧ … ∧ d_{n} = c_{n} ⊃ l ) r

where d_{1}, …, d_{n}, c_{1} …, c_{n}, l, r ∈ Λ(Σ) and (i) every variable of d⃗, c⃗, r occurs also in l, (ii) l is an algebraic term which is not a variable. In conditional rewrite rules, we distinguish

— the left-hand side l, the right-hand side r ;

— the conditions d_{1} = c_{1} ∧ ⋯ ∧ d_{n} = c_{n}. A rule d_{1} = c_{1} ∧ ⋯ ∧ d_{n} = c_{n} ⊃ l ) r is unconditional if n = 0. It is left-linear if l is linear.

Since left-hand sides are algebraic terms, rewriting is performed using syntactical first-order matching. Note that the conditions of rewrite rules are not symmetric: the condition d = c is not the same as c = d.

Given a set R of conditional rewrite rules, different conditional rewrite relations can be defined, depending on the evaluation of the conditions: by conversion, by joinability or by reduction. This leads respectively to semi-equational, join and oriented conditional rewriting. In this paper, we focus on join conditional rewriting. We consider two cases, whether β-reduction is allowed or not the evaluation of conditions.

Definition 2.9 (Conditional Rewriting) Let R be a set of conditional rewrite rules.

— The conditional rewrite relation )_{R} is defined as

)_{R} =_{def} ⋃_{i∈ℕ} )_{R_{i}} ,

where )_{R_{0}} =_{def} ∅ and for all i ∈ ℕ, )_{R_{i+1}} is the smallest rewrite relation such that for every rule d⃗ = c⃗ ⊃ l )_{R} r and every substitution σ,

if d⃗σ ]_{R_{i}}  c⃗σ  then  lσ )_{R_{i+1}} rσ .

— The β-conditional rewrite relation )_{R(β)} is defined as

)_{R(β)} =_{def} ⋃_{i∈ℕ} )_{R(β)_{i}} ,

where )_{R(β)_{0}} =_{def} ∅ and for all i ∈ ℕ, )_{R(β)_{i+1}} is the smallest rewrite relation such that for every rule d⃗ = c⃗ ⊃ l )_{R} r and every substitution σ,

if d⃗σ ]_{β∪R(β)_{i}}  c⃗σ  then  lσ )_{R(β)_{i+1}} rσ .

Hence, with conditional rewriting )_{R}, β-reduction is not allowed in the evaluation of conditions, while it is allowed with β-conditional rewriting )_{R(β)}. Note that )_{R}⊆)_{R(β)}. The converse is false, as shown by the following example.

Example 2.10 Consider the rule

p x = true ⊃ filter p (cons x l) ) cons x (filter p l)

issued from the conditional rewrite system (1) and assume that id x ) x. With conditional rewriting we have

filter id (cons true ts) )_{R} cons true (filter ts)  since  id true )_{R} true .

With β-conditional rewriting we also have

filter (λx.x) (cons true ts) )_{R(β)} cons true (filter ts)  since  (λx.x) true )_{β} true ,

but the term filter (λx.x) (cons true ts) is a )_{R}-normal form.

An interesting particular case of join conditional rewriting is normal rewriting.

Definition 2.11 (Normal Conditional Rewriting) Let R be a conditional rewrite system. If for every rule d⃗ = c⃗ ⊃ l )_{R} r, the conditions c⃗ are closed terms in )_{R}-normal form, then we say that )_{R} is a normal conditional rewrite relation.

In general, for a given conditional system the normal forms w.r.t. join and semi-equational rewriting are not the same (this is a by-product of the fact that semi-equational orthogonal rewriting is confluent, while join orthogonal rewriting is not [BK86, Ohl02], see also Theorem 3.12). The notion of normal conditional rewriting presented in Definition 2.11 is thus specific to join conditional rewriting (it is easy to see that it coincides with normality for oriented rewriting).

An important point with conditional rewriting is the possible undecidability of a rewriting step. This impacts of effectiveness of the notion of normal conditional rewriting.

Remark 2.12 (Decidability) One-step conditional rewrite relations are in general not decidable. Consider a rule d⃗ = c⃗ ⊃ l ) r. Because of the recursive definition of )_{R}, to know if lσ )_{R} rσ, we need to reduce the terms d⃗σ and c⃗σ. This is in general undecidable, even for terminating systems [Kap84] (see also [Ohl02]).

These facts have consequences on normal rewriting. Given a set of conditional rules, to determine whether it can generate a normal relation, we have to check that a part of the conditions is in normal form. This is in general undecidable, even when the rewrite relation terminates.

We therefore focus on join rewriting because it seems to be a more easily and generally applicable theory than normal rewriting, even if the implementation of conditional rewriting is easier when we already know that the conditional rewrite relation is normal.

Our results on the preservation of confluence impose restrictions on rewrite rules. Some of them concern the terms which can appear in different parts of the rules. This motivates the following definition. Recall from Definition 2.8 that left-hand sides are always assumed to be algebraic.

Definition 2.13 (Applicative and Algebraic Conditional Rewrite Rules) A conditional rewrite rule d⃗ = c⃗ ⊃ l ) r is

— right-applicative if r is an applicative term,

— applicative if it is right-applicative and if moreover the terms d⃗, c⃗ are applicative,

— right-algebraic if r is an algebraic term,

— algebraic if it is right-algebraic and if moreover the terms d⃗, c⃗ are algebraic.

A rewrite system R is right-applicative (resp. applicative, right-algebraic, algebraic) if all its rules are right-applicative (resp. applicative, right-algebraic, algebraic).

In the conditional rewrite system (1), the first rule filter p nil ) nil is algebraic. The two other rules are right-algebraic. They both use the term p x in their conditions, where p is a variable. This term is applicative but not algebraic.

2.4 Examples

We now give some examples of conditional rewrite systems.

2.4.1 Coherence of lambda-calculus with surjective pairing

We begin by recalling one use of conditional rewriting in the study of λ-calculus with surjective pairing. We use pair t_{1} t_{2} to denote the pairing of t_{1} and t_{2}. The rewrite rules for binary products are the following:

fst (pair x_{1} x_{2}) )_{π} x_{1} snd (pair x_{1} x_{2}) )_{π} x_{2} .

It is well-known that the combination of these rules with β-reduction is confluent (see Theorem 3.3, proved in [Mül92]). This follows from the left-linearity of the rewrite rules. However, when we add the rule for surjective pairing

pair (fst x) (snd x) )_{SP} x

then the combination of the resulting rewrite relation with β-reduction is not confluent [Klo80]. Note that the rule )_{SP} is not left-linear: the variable x appears twice in the left-hand side. However, the corresponding conversion is coherent: there are two terms that are not convertible. This has been first shown using semantic methods [Sco75].

In [Vri89], de Vrijer uses semi-equational β-conditional rewriting to give a syntactic proof of the coherence of β-reduction combined with surjective pairing. His rules are those of )_{π} plus

snd x = y ⊃ pair (fst x) y )_{lr} x fst x = y ⊃ pair y (snd x) )_{lr} x .

The resulting relation is confluent modulo an equivalence relation, and this allows de Vrijer to show that λ-calculus plus pairs and surjective pairing is a conservative extension of the pure λ-calculus: for any two pure λ-terms t, u ∈ Λ,

t ⌊_{β} u if and only if t ⌊_{β∪π∪SP} u .

2.4.2 A term manipulation system

Our main example is an adaptation of a CAML program of [Hue86]. It defines functions that perform in a term the replacement of the subterm at a given occurrence by another term. Terms are represented by trees whose nodes contain a label and the list of their successor nodes.

This system must be read having in mind the combination of λ-calculus with (join) βconditional rewriting.

We begin by some basic functions on lists.

car (cons x l) ) x
car nil  ) err

cdr (cons x l) ) l
cdr nil  ) err
get l zero  ) car l
get l (succ n) ) get (cdr l) n

length nil  ) zero
length (cons x l) ) succ (length l)
filter p nil  ) nil
p x = true ⊃ filter p (cons x l) ) cons x (filter p l)
p x = false ⊃ filter p (cons x l) ) filter p l

Let us define apply such that applyf n l applies f to the nth element of l. It uses app as an auxiliary function:

> (length l) n = true ⊃ apply f n l  ) app f n l
> (length l) n = false ⊃ apply f n l  ) err
app f zero l  ) cons (f (car l)) (cdr l)
app f (succ n) l ) cons (car l) (app f n (cdr l))

We represent first-order terms by trees with nodes nodey l where y is intended to be a label and l the list of sons. Positions are lists of integers and occu t tests if u is an occurrence of t. We define it as follows:

occ nil t  ) true
> (length l) x = false ⊃ occ (cons x o) (node y l) ) false
> (length l) x = true ⊃ occ (cons x o) (node y l) ) occ o (get l x)

To finish, replacet o s replaces by s the subterm of t at occurrence o.

occ u t = true ⊃ replace t o s ) rep t o s
occ u t = false ⊃ replace t o s ) err
rep t nil s  ) s
rep (node y l) (cons x o) s ) node y (apply (λz.rep z o s) x l)

The system Tree that consists of the rules defining car, cdr, get, length and occ is algebraic. The rules of apply and app are right-applicative and those for filter contain in their conditions the variable p in active position. This definition of rep involves a λ-abstraction in a right hand side. In Section 6, we prove confluence of the relation )_{β∪R(β)} induced by the whole system.

2.5 Confluence

The main property on rewrite relations studied in this paper is confluence. The confluence of a relation ) which has at least two distinct normal forms entails the coherence of the conversion ⌊. Moreover, it allows to evaluate terms in a modular way: the choice of the subterm to be evaluated first has no impact on the result of the evaluation.

In this section we recall some well-known facts about confluence which will be useful in the following.

A sufficient condition for confluence is the diamond property.

Definition 2.14 (Confluence) A rewrite relation ) is confluent if (^{∗})^{∗} ⊆ )^{∗}(^{∗} and has the diamond property if () ⊆ )( .

In diagrammatic form:

\xymatrix{ & · \ar[dr]_{∗} \ar[dl]^{∗} &  &  & · \ar[dr] \ar[dl] \\ · \ar@{.>}[dr]^{∗} &  & · \ar@{.>}[dl]_{∗} & · \ar@{.>}[dr] &  & · \ar@{.>}[dl] \\  & · &  &  & ·}

Confluence  Diamond property

The stratification of conditional rewrite relations leads to fine-grained notions of confluence.

Definition 2.15 (Stratified Confluences) Assume that ()_{i})_{i∈ℕ} are rewrite relations and let ) =_{def} ⋃_{i∈ℕ} )_{i} . We say that ) is level confluent if for all i ≥ 0 we have (_{i}^{∗})_{i}^{∗} ⊆ )_{i}^{∗}(_{i}^{∗} ; and shallow confluent if for all i, j ≥ 0 we have (_{i}^{∗})_{j}^{∗} ⊆ )_{j}^{∗}(_{i}^{∗} .

In diagrammatic form:

\xymatrix{ & · \ar[dr]^{i}_{∗} \ar[dl]_{i}^{∗} &  &  & · \ar[dr]^{i}_{∗} \ar[dl]_{j}^{∗} \\ · \ar@{.>}[dr]_{i}^{∗} &  & · \ar@{.>}[dl]^{i}_{∗} & · \ar@{.>}[dr]_{i}^{∗} &  & · \ar@{.>}[dl]^{j}_{∗} \\  & · &  &  & ·}

Level Confluence  Shallow Confluence

Note that shallow confluence implies level confluence which in turns implies confluence. For instance, in Section 6 we show that )_{β∪R(β)} is shallow confluent for some conditional rewrite systems R called orthonormal. This entails their confluence.

Combinations of rewrite relations. Since we are interested in the confluence of the combination of two rewrite relations (conditional rewriting and λ-calculus), we will use the following notions.

Definition 2.16 (Commutation) A rewrite relation )_{A} commutes with a rewrite relation )_{B} if (_{A}^{∗})_{B}^{∗} ⊆ )_{B}^{∗}(_{A}^{∗} .

The Hindley-Rosen Lemma is a simple but important tool to prove the confluence of the combination of two rewrite relations.

Lemma 2.17 (Hindley-Rosen) If )_{A} and )_{B} are two confluent rewrite relations that commute then )_{A∪B} is confluent.

The next simple lemma is useful to prove the commutation of two relations.

Lemma 2.18 Let )_{A} and )_{B} be two rewrite relations such that for all t, u, v ∈ Λ(Σ), if u (_{A} t )_{B} v then there is a term w such that u )_{B}^{∗} w (_{A} v. Then )_{A} commutes with )_{B}.

Proof. We show (i) by induction on )_{B}^{∗} and deduce (ii) by induction on )_{A}^{∗}.

\begin{matrix}\xymatrix{· \ar[r]^{B}_{∗} \ar[d]_{A} & · \ar@{.>}[d]^{A} \\ · \ar@{.>}[r]_{B}^{∗} & ·} & \xymatrix{· \ar[r]^{B}_{∗} \ar[d]_{A}^{∗} & · \ar@{.>}[d]^{A}_{∗} \\ · \ar@{.>}[r]_{B}^{∗} & ·} \\ (i) & (ii) \end{matrix}

3 Confluence: from unconditional to conditional rewriting

In this section we state precisely the known results from which this paper starts and give a short overview of our results. In Section 3.1 we review the results on the combination of λcalculus with unconditional rewriting that we extend to conditional and β-conditional rewriting in Section 4 and Section 5 respectively. In Section 3.2 we recall a result on the confluence of orthogonal normal rewrite relations, that we generalize to orthonormal β-conditional rewriting in Section 6. We then give a short overview of our results in Section 3.3.

3.1 Confluence of beta-reduction with unconditional rewriting

Our results of Section 4 and 5 on the preservation of confluence for the combination of λ-calculus with conditional rewriting are extensions of similar results on the combination of λ-calculus with unconditional rewriting. We concentrate of two cases, both untyped, that we review in this section:

— In Section 3.1.1 we discuss Müller’s result [Mül92] (stated in Theorem 3.3) on left-linear rewriting.

— In Section 3.1.2 we discuss Dougherty’s result [Dou92] (stated in Theorem 3.7) on strongly β-normalizing terms with arity conditions.

3.1.1 Left-linear rewriting

Using the example of surjective pairing [Klo80], we have recalled in Section 2.4.1 that the combination of a confluent non left-linear rewrite system with β-reduction may not be confluent. An example has also been presented in [BTM87], which can be seen as an adaptation of an example due to Huet [Hue80] concerning first-order rewriting.

Example 3.1 ([BTM87]) Consider the confluent rewrite system

minus x x )_{minus} zero minus (succ x) x )_{minus} (succ zero) ,

and let

Y_{succ} =_{def} (λx.succ (x x)) (λx.succ (x x)) .

Since Y_{succ} )_{β} succY_{succ}, we have the following unjoinable peak:

\xymatrix{ & minus Y_{succ} Y_{succ} \ar@{-->}[dl] \ar[dr] \\ minus (succ Y_{succ}) Y_{succ} \ar[d] &  & zero \\ _{succ zero}}

Remark 3.2 (Interpretation with Böhm trees) A simple interpretation of this system is to see Y_{succ} as representing the "infinite integer" , the term minusY_{succ} Y_{succ} representing the undefined operation − . This interpretation can be made concrete by using Böhm trees [Bar84]. The Böhm tree of the term Y_{succ} is the infinite term

succ succ ⋮

Intuitively, Ex 3.1 can be seen as an instance of the fact that confluence of non left-linear systems is not preserved when we extend the term algebra (in this case by infinite terms).

As shown in [Mül92], confluence is preserved when rewriting is left-linear. The original result concerns only algebraic systems, but can easily be extended to unconditional rewrite systems with arbitrary right-hand sides.

Theorem 3.3 ([Mül92]) If R is a left-linear unconditional rewrite system such that )_{R} is confluent then )_{β∪R} is confluent.

This result has been generalized to the case of Higher-Order Rewrite Systems [OR94].

3.1.2 Strongly beta-normalizing terms

To handle non left-linear systems, as seen in Example 3.1 we have to forbid infinite terms. This is possible for example by focusing on algebraic rewriting on typed terms. Confluence is preserved for the combination of algebraic rewriting with simply typed λ-calculus [BT88]. This result has been then extended to the polymorphic λ-calculus [BTG89, BTG94, Oka89].

A question arises from these results: besides strong normalization of β-reduction, what is the role of typing in the preservation of confluence ? This is studied in [Dou92], which shows that for algebraic rewriting terms must satisfy some arity conditions.

Example 3.4 Consider the rewrite system

id x )_{id} x ,

and let Ω_{succ} =_{def} λx.succ (x x). The term

t =_{def} minus (id Ω_{succ} Ω_{succ}) (id Ω_{succ} Ω_{succ})

is in β-normal form, hence strongly β-normalizing. Moreover, we can check that the rewrite system )_{minus∪id} is confluent. However, )_{β∪minus∪id} is not confluent since t rewrites to the unjoinable peak of Example 3.1:

minus(id Ω_{succ} Ω_{succ}) (id Ω_{succ} Ω_{succ}) )_{id}^{2} minus Y_{succ} Y_{succ} .

The problem is that reducing id in the β-normal form idΩ_{succ} Ω_{succ} leads to a term which is no longer in β-normal form: rewriting does not preserve β-normal forms. The approach taken in [Dou92] is to find arity conditions on terms for rewriting to preserve β-normal forms. Consider a symbol f ∈ Σ such that for all fl⃗ )_{R} r, we have |l⃗| ≤ n. Then we discard terms of the form ft⃗ with |t⃗| > n. For example, the term id Ω_{succ} Ω_{succ} is not allowed since id takes two arguments whereas its rewrite rule takes only one.

Definition 3.5 (Applicative Arity) An arity is a function a : Σ ) ℕ.

(i) A term t respects a if it contains no subterm ft⃗ with |t⃗| > a(f).

(ii) A rewrite system R respects a if for all fl⃗ )_{R} r, fl⃗ and r respect a and moreover |l⃗| = a(f).

However, the respect of an arity is not stable by β-reduction. For instance, with a(id) = 1 the term (λx.x Ω_{succ} Ω_{succ}) id respects a but it β-reduces to idΩ_{succ} Ω_{succ} which does not respect a. In order to work with terms which respect an arity a and whose βR-reducts respect a too, it is convenient to consider sets of terms respecting a and which are stable by reduction. This motivates the following definition.

Definition 3.6 ((R, a)-Stable Terms) Given an arity a and a rewrite system R, a set of terms S is (R, a)-stable if

(i) for all t ∈ S, t respects a, (ii) for all t ∈ S, if t )_{β∪R} u then u ∈ S,

(iii) for all t ∈ S, if u is a subterm of t then u ∈ S.

Dougherty [Dou92] obtain the preservation of confluence on (R, a)-stable sets of strongly β-normalizing terms.

Theorem 3.7 ([Dou92]) If R is an algebraic confluent unconditional rewrite system that respects an arity a, then )_{β∪R} is confluent on every (R, a)-stable set S ⊆ SN_{β}.

Remark 3.8 To get the preservation β-normal forms by rewriting it is necessary to restrict to algebraic right-hand sides, since in contrast with algebraic terms, substituting a variable in an applicative term may produce a β-redex. For instance (x z)[λy.y/x] = (λy.y) z.

3.2 Orthogonal conditional rewriting

Orthogonality is a sufficient condition for the confluence of some kinds of conditional rewriting. In this section we recall some known results about the confluence of algebraic orthogonal conditional rewrite systems. They were initially formulated in the framework of first-order conditional rewriting, of which algebraic rewriting is an instance. The main result is the shallow confluence of orthogonal normal conditional rewriting. We generalize it in Section 6 to orthonormal β-conditional rewriting.

For unconditional rewriting, orthogonality is a simple syntactic criterion: it entails the confluence of left-linear systems with no critical pairs [Hue80]. With conditional rewriting, things get more complicated since the notion of critical pairs has to take into account the conditions of rewrite rules.

Definition 3.9 (Conditional Critical Pairs) Let R be a set of conditional rules and suppose that ρ_{1} : d⃗ = c⃗ ⊃ l ) r and ρ_{2} : d⃗′ = c⃗′ ⊃ l′ ) r′ are two renaming of rules in R such that they have no variable in common. If p is a non-variable occurrence of l and σ is a most general unifier of l|_{p} and l′, then

d⃗σ = c⃗σ ∧ d⃗′σ = c⃗′σ ⊃ (l[p ( r′]σ , rσ)

is a conditional critical pair of R. If ρ_{1} and ρ_{2} are renaming of the same rule, we assume that p is not the root position of l. A critical pair of the form d⃗ = c⃗ ⊃ (s, s) is called trivial.

The important point is that in a conditional critical pair d⃗ = c⃗ ⊃ (s, t), it is possible that there is no substitution σ such that d⃗σ = c⃗σ. Thus, critical pairs can be feasible or unfeasible. According to the kind of conditional rewriting considered (with and without β-reduction in the evaluation of conditions), the satisfaction of conditions is done differently. Therefore, we consider two notions of feasibility.

Definition 3.10 (Feasibility of Conditional Critical Pairs) A critical pair d⃗ = c⃗ ⊃ (s, t) of a conditional system R is

— feasible if there is a substitution σ such that d⃗σ ]_{R} c⃗σ;

— β-feasible if there is a substitution σ such that d⃗σ ]_{β∪R(β)} c⃗σ;

A critical pair which is not feasible (resp. β-feasible) is said unfeasible (resp. β-unfeasible).

The easiest way to prove unfeasibility of critical pairs is often to use confluence. We come back on this question in Section 6. Both notions of feasibility induce a notion of orthogonality.

Definition 3.11 (Orthogonality) A set R of left-linear conditional rewrite rules is

— orthogonal (resp. β-orthogonal) if all its critical pairs are unfeasible (resp. β-unfeasible);

— weakly orthogonal (resp. weakly β-orthogonal) if all its critical pairs are either trivial or unfeasible (resp. β-unfeasible).

Hence, to test the orthogonality of a conditional system, we have to evaluate the conditions of its critical pairs. According to Remark 2.12, this is in general undecidable.

It is well-known that for normal (and semi-equational) rewriting, weak orthogonality implies confluence. This in general not the case for join conditional rewriting, as shown in [BK86].

Theorem 3.12 ([BK86, Ohl02]) Let R be a conditional rewrite system. If R is weakly orthogonal, and moreover is a normal system, then )_{R} is shallow confluent.

3.3 Overview of the results

The goal of this paper is to give sufficient conditions for the confluence of β-reduction with β-conditional rewriting (i.e. with β-steps allowed in the evaluation of conditions).

More precisely, we seek to obtain results on the preservation of confluence, that is to get the confluence of )_{β∪R(β)} assuming the confluence of )_{R}. Our approach is to generalize the results summarized in Section 3.1 on the combination of β-reduction with unconditional rewriting. We thus consider two different cases:

— First, the extension of Müller’s result [Mül92], when β-reduction is not restricted (we thus need to assume left-linearity, and to extend this notion to conditional rewriting).

— Second, the extension of Dougherty’s result [Dou92], when we restrict to β-normalizing terms (we thus need some arity conditions on terms). In fact, we improve [Dou92] from strongly β-normalizing terms to weakly β-normalizing terms.

In each case, we proceed in two steps. We first consider in Section 4 the case of β-reduction with conditional rewriting )_{R} (when β-reduction is not allowed in the evaluation of conditions). We then extend these results to β-conditional rewriting )_{R(β)} in Section 5.

As discussed at the beginning of Section 5 (see Example 5.2), for the extension of both [Mül92] and [Dou92] to β-conditional rewriting, rewrite rules must be algebraic and respect arity conditions. In contrast, the extension of [Mül92] to the simpler case of conditional rewriting holds without these restrictions. This motivates the definition of criteria for the confluence of βreduction with β-conditional rewriting when rules need not be algebraic nor to respect an arity (recall from Definition 2.8 that left-hand sides are always algebraic in this paper). We propose such a criterion in Section 6, which defines orthonormal conditional rewriting, an extension of orthogonal rewriting. We show the shallow confluence of β-reduction with β-conditional rewriting for these systems, hence extending Theorem 3.12.

Our results are summarized in Figure 1 page 6.

4 Confluence of beta-reduction with conditional rewriting

We now turn to conditional rewriting. In this section we focus on the combination of join conditional rewriting )_{R} with β-reduction: we do not allow the use of β-reduction in the evaluation of conditions.

The important point of left-linearity is to prevent unconditional rewriting from comparing arbitrary terms. It forbids in particular comparisons of infinite terms such as Y_{succ}. But with conditional rewriting, rewrite rules can make this comparison in their conditions while being left-linear. Hence, starting from Example 3.1, we can define a left-linear conditional rewrite system which makes the commutation of rewriting with β-reduction fail.

Example 4.1 Consider the conditional system

x = y ⊃ minus x y ) zero x = (succ y) ⊃ minus x y ) (succ zero) .

This system is left-linear, but the conditions can test the equality of open terms. The join conditional rewrite relation issued from this system forms with )_{β} the following unjoinable peak:

\xymatrix{ &  & minus Y_{succ} Y_{succ} \ar@{-->}[dl] \ar[dr] & (Y_{succ} ] Y_{succ}) \\ ((succ Y_{succ}) ] (succ Y_{succ})) & minus (succ Y_{succ}) Y_{succ} \ar[d] &  & zero \\  & (succ zero)}

As for unconditional rewriting in Section 3.1, we consider two ways to overcome the problem: to restrict rewriting (Section 4.1) or to restrict β-reduction (Section 4.2).

4.1 Confluence for left-linear semi-closed systems

In this section we are interested in the extension of Theorem 3.3 ([Mül92]) to conditional rewriting: we want sufficient conditions on rewrite rules for the preservation of confluence on all untyped terms of Λ(Σ). As seen in Example 4.1, for conditional rewriting we have to extend the notion of left-linearity in order to forbid comparison of open terms in the conditions of rewrite rules. To this end we restrict to semi-closed conditional rewrite rules.

Definition 4.2 (Semi-Closed Conditional Rewrite Rules) A conditional rewrite system R is semi-closed if for all rules

d_{1} = c_{1} ∧ … ∧ d_{n} = c_{n} ⊃ l )_{R} r ,

the terms c_{1}, …, c_{n} are applicative and closed.

For example, the system Tree of Section 2.4 is left-linear and semi-closed. In a semi-closed rule d⃗ = c⃗ ⊃ l ) r, since c⃗ are closed terms, it is tempting to normalize them and obtain a normal rewrite relation, but as noted in Remark 2.12, results on join rewriting seem more easily applicable.

We show that the confluence of )_{R} implies the confluence of )_{β∪R} for semi-closed leftlinear right-applicative systems (Theorem 4.6). Using Hindley-Rosen lemma (Lemma 2.17), this follows from the commutation of conditional rewriting with β-reduction. As in [Mül92], we obtain this commutation as a consequence of the commutation of conditional rewriting with a relation ⊳_{β} of parallel β-reduction (see Definition 2.5). This is shown in Lemma 4.5, which relies on Property 2.6 (σ ⊳_{β} σ′ implies tσ ⊳_{β} tσ′). This property holds for parallel rewrite relations but fails with )_{β}.

The parallel β-reduction ⊳_{β} we use is Tait and Martin-Löf’s relation [Bar84, Tak95]. It is defined as follows.

Definition 4.3 (Parallel β-Reduction) We let ⊳_{β} be the smallest parallel rewrite relation closed under the rule

(⊳β) \frac{t_{1} ⊳_{β} u_{1} t_{2} ⊳_{β} u_{2}}{(λx.t_{1})t_{2} ⊳_{β} u_{1}[u_{2}/x]}

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, ⊳_{β} enjoys the diamond property: ⊲_{β} ⊳_{β} ⊆ ⊳_{β} ⊲_{β}.

The relation ⊳_{β} is stronger than the one used in [Mül92]: it can reduce in one step nested β-redexes, while the relation of [Mül92] is simply the smallest parallel rewrite relation containing β-reduction (i.e. the parallel closure of )_{β}). The diamond property (which holds for ⊳_{β}) fails for the parallel closure of β-reduction precisely because it cannot reduce nested β-redexes in one step. The parallel closure of )_{β} would have been sufficient to obtain Lemma 4.5, but we use the nested relation ⊳_{β} because we rely on the diamond property in Section 5.1.

Nested parallelizations (corresponding to complete developments) are already used in [OR94] for their confluence proof of HORSs. However, our method inherits more from [Mül92] than from [OR94], as we use complete developments of )_{β} only, whereas complete developments of )_{β} and of )_{R} are used for the modularity result of [OR94].

The left-linearity assumption is used in the proof of Lemma 4.5 via the following property of linear algebraic terms.

Proposition 4.4 Let t be an algebraic linear term and σ be a substitution such that tσ ⊳_{β} u. There is a substitution σ′ such that u = tσ′ with σ ⊳_{β} σ′ and σ′(x) = σ(x) for all x ∉ FV(t).

Proof. By induction on t.

t = x ∈ X. In this case tσ = σ(x). Take σ′ such that σ′(x) = u and σ′(y) = σ(y) for all y ≠ x.

t = f ∈ Σ. In this case tσ = t = u, hence σ′ = σ fits (recall that ⊳_{β} is reflexive).

t = t_{1}t_{2}. Since t is algebraic, t_{1}σ t_{2}σ is not a β-redex. It follows that u is of the form u_{1} u_{2} with (t_{1}σ, t_{2}σ) ⊳_{β} (u_{1}, u_{2}). By induction hypothesis, there are two substitutions σ′_{1} and σ′_{2} such that for each i ∈ {1, 2} we have σ ⊳_{β} σ′_{i}, u_{i} = t_{i}σ′_{i}, and σ′_{i}(x) = σ(x) for all x ∉ FV(t_{i}). Since t is linear, FV(t_{1}) ∩ FV(t_{2}) = ∅, hence with σ′ =_{def} σ′_{1} ⊎ σ′_{2}, we have u = u_{1}u_{2} = t_{1}σ′ t_{2}σ′ = tσ′, σ ⊳_{β} σ′ and σ(y) = σ′(y) for all y ∉ FV(t).

We are now ready to prove the commutation of )_{R} and ⊳_{β}. In fact we prove a slightly stronger statement, which can be termed as the "level commutation" of )_{R} and ⊳_{β}.

Lemma 4.5 (Commutation of )_{R_{i}} with ⊳_{β}) If R is a conditional rewrite system which is semi-closed, left-linear and right-applicative, then ⊳_{β} commutes with )_{R_{i}} for all i ∈ ℕ:

\xymatrix{· \ar[r]^{R_{i}}_{∗} \ar[d]_{⊳_{β}}^{∗} & · \ar@{.>}[d]^{⊳_{β}}_{∗} \\ · \ar@{.>}[r]_{R_{i}}^{∗} & ·}

Proof. We reason by induction on i ∈ ℕ. The base case i = 0 is trivial. Let i ≥ 0 and assume that )_{R_{i}} commutes with ⊳_{β}. We show that )_{R_{i+1}} commutes with ⊳_{β}.

We begin by showing that for all t, u, v ∈ Λ(Σ), if u ⊲_{β} t )_{R_{i+1}} v then there is a term w such that u )_{R_{i+1}}^{∗} w ⊲_{β} v. In diagrammatic form:

\xymatrix{t \ar[r]^{R_{i+1}} \ar[d]_{⊳_{β}} & v \ar@{.>}[d]^{⊳_{β}} \\ u \ar@{.>}[r]_{R_{i+1}}^{∗} & w}  (3)

We deduce from (3) that )_{R_{i+1}} commutes with ⊳_{β} by applying Lemma 2.18.

We now show (3) by induction on t. If both reductions t ⊳_{β} u and t )_{R_{i+1}} v occur in a proper subterm of t then we conclude by induction hypothesis. Otherwise there are two cases.

(i) t = (λx.t_{1})t_{2} with u = u_{1}[u_{2}/x] and v = (λx.v_{1})v_{2} where (u_{1}, u_{2}) ⊲_{β} (t_{1}, t_{2}) )_{R_{i+1}} (v_{1}, v_{2}). By induction hypothesis, there are terms w_{1} and w_{2} such that u_{i} )_{R_{i+1}}^{∗} w_{i} ⊲_{β} v_{i}. We deduce that u_{1}[u_{2}/x] )_{R_{i+1}}^{∗} w_{1}[w_{2}/x] and that (λx.v_{1})v_{2} ⊳_{β} w_{1}[w_{2}/x].

(ii) t is the R-redex contracted in the step t )_{R_{i+1}} v. In this case, there is a conditional rule d⃗ = c⃗ ⊃ l )_{R} r and a substitution σ s.t. t = lσ and v = rσ. Moreover, there are terms v⃗ such that d⃗σ )_{R_{i}}^{∗} v⃗ (_{R_{i}}^{∗} c⃗σ. Since R is semi-closed, the terms c⃗ are closed and applicative, hence c⃗σ = c⃗ and the terms v⃗ are applicative since R is right-applicative. Since l is left-linear and algebraic, we deduce from Proposition 4.4 that there is a substitution σ′ such that σ⊳_{β} σ′ and u = lσ′. It follows Proposition 2.6 that rσ⊳_{β} rσ′ and d⃗σ⊳_{β} d⃗σ′.

To conclude that w =_{def} rσ′ fits, it remains to show that lσ′ )_{R_{i+1}} rσ′, that is d⃗σ′ ]_{R_{i}} c⃗. We have d⃗σ′⊲_{β} d⃗σ )_{R_{i}}^{∗} v⃗, hence by induction hypothesis there are w⃗ s.t. d⃗σ′ )_{R_{i}}^{∗} w⃗⊲_{β}^{∗} v⃗. It follows that d⃗σ′ )_{R_{i}}^{∗} v⃗, the terms v⃗ being applicative hence in β-normal form. We thus have d⃗σ′ ]_{R_{i}} c⃗, and conclude that lσ′ )_{R_{i+1}} rσ′.

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

Theorem 4.6 (Confluence of )_{β∪R}) Let R be a semi-closed left-linear right-applicative system. If )_{R} is confluent then so is )_{β∪R}.

Comparison with Müller’s work. Our main result on the confluence of β-reduction with conditional rewriting for left-linear semi-closed system (Theorem 4.6) is not a true extension of Theorem 3.3. Indeed, Theorem 3.3 apply to unconditional systems with arbitrary right-hand sides, while Theorem 4.6 requires right-hand sides to be applicative.

The problem is that Lemma 4.5 may fail with non-applicative right-hand sides. Consider the system:

h ) λx.x x = h a ⊃ g x ) a

We have g a (_{β} g ((λx.x)a) )_{R} a. But since the term (λx.x)a is a R-normal form, the condition x ]_{R} h a is not satisfied, and g a is a R-normal form.

We can extend Theorem 3.3 to normal conditional rewriting, i.e. to systems R such that in all rules d⃗ = c⃗ ⊃ l )_{R} r, the cosed algebraic terms c⃗ are required to be in normal form w.r.t. )_{R} (recall from Remark 2.12 that this is undecidable). The proof follows exactly the same scheme as for Theorem 4.6. The only difference lies in the commutation of )_{R_{i}} with )_{β}, for which Lemma 4.5 does not apply.

Theorem 4.7 (Extension of [Mül92]) Let R be a left-linear semi-closed system such that )_{R} is a normal conditional rewrite relation. If )_{R} is confluent then so is )_{β∪R}.

Proof. As in Theorem 4.6, the proof relies on the commutation of )_{R_{i}} with )_{β}. Since righthand sides are not applicative, we can not use Lemma 4.5. However, the commutation of )_{R_{i}} with ⊳_{β} is proved using the same general reasoning, excepted for the following point. Assume that )_{R_{i}} commutes with ⊳_{β} and that for a rule d⃗ = c⃗ ⊃ l )_{R} r and a substitution σ we have lσ′ ⊲_{β} lσ )_{R_{i+1}} rσ. As )_{R} is normal, we have d⃗σ )_{R_{i}}^{∗} c⃗, and by induction hypothesis there are c⃗′ such that d⃗σ′ )_{R_{i}}^{∗} c⃗′ (_{β}^{∗} c⃗. Since R is semi-closed, the terms c⃗ are algebraic hence β-normals. It follows that d⃗σ′ )_{R_{i}}^{∗} c⃗, hence lσ′ )_{R_{i+1}} rσ′.

4.2 Confluence on weakly beta-normalizing terms

We now turn to the problem of dropping the left-linearity and semi-closure conditions. We generalize Theorem 3.7 [Dou92] in two ways. First, we adapt it to conditional rewriting. Second, we use weakly β-normalizing terms whose β-normal forms respect an arity, whereas Dougherty uses sets of strongly normalizing arity compliant terms closed under reduction.

As seen in Example 4.1, fixpoint combinators make the commutation of )_{β}^{∗} and )_{R}^{∗} 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

\xymatrix{s \ar[r]^{β∪R}_{∗} \ar@{.>}[d]_{β}^{∗} & t \ar@{.>}[d]^{β}_{∗} \\ βnf(s) \ar@{.>}[r]_{R}^{∗} & βnf(t)}  (4)

We rely on the following:

(i) First, β-normal forms should be stable by rewriting. By Remark 3.8 we must assume that right-hand sides are algebraic, and as seen in Example 3.4, we must use the notion of applicative arity (Definition 3.5).

(ii) We need normalizing β-derivations to commute with rewriting. This follows from using the leftmost-outermost strategy of λ-calculus.

(iii) Finally, we assume that conditions are algebraic. Since left-hand sides and right-hand sides are algebraic (by Definition 2.8 and item (i) respectively), this entails that for all rules d⃗ = c⃗ ⊃ l )_{R} r and all substitutions σ, we have βnf(d⃗σ) = d⃗ βnf(σ), βnf(c⃗σ) = c⃗ βnf(σ), βnf(lσ) = l βnf(σ), βnf(rσ) = r βnf(σ).

We now have to extend to conditional rewriting the condition of arity on rewrite rules stated in Definition 3.5.(ii).

Definition 4.8 (Applicative Arity for Conditional Rules) A rule d⃗ = c⃗ ⊃ l )_{R} r respects an arity a : Σ ) ℕ if the terms d⃗, c⃗ respect a and the unconditional rule l ) r respects a.

As seen in Example 3.4, terms and rewrite systems respecting an arity prevent collapsing rules from creating β-redexes.

However, we do not assume that every term at hand respects an arity. If a term has a β-normal form, the leftmost-outermost strategy for β-reduction never evaluates non-normalizing subterms.

It follows that such subterms may not respect any arity without disturbing the projection on βnormal forms. Therefore it is sufficient to require that terms have a β-normal form that respects an arity.

Definition 4.9 Given an arity a : Σ ) ℕ, we let AN_{a} be the set of terms having a β-normal form, and whose β-normal form respects a.

The proof goes through essentially thanks to two points: the well-foundedness of the leftmostoutermost strategy for )_{β} on weakly β-normalizing terms [Bar84]; and the fact that this strategy can be described by means of head β-reductions, that are easily shown to commute with (parallel) conditional rewriting.

We use a well-founded relation containing head β-reductions. Recall that by Lemma 2.3, any λ-term can be written either

λx⃗.va_{0} a_{1} …a_{n}  (a)
or λx⃗.(λy.b)a_{0} a_{1} …a_{n}  (b)

where v ∈ X ∪ Σ. We denote head β-reductions by )_{h}. They consist of head β-steps:

λx⃗.(λy.b)a_{0} a_{1} …a_{n} )_{h} λx⃗.b[a_{0}/y]a_{1} …a_{n} .

We use the relation ≻ defined as:

λx⃗.v a_{0} a_{1} …a_{n} ≻ a_{i}  (a)
λx⃗.(λy.b)a_{0} a_{1} …a_{n} ≻ λx⃗.b[a_{0}/y] a_{1} …a_{n}  (b)

where v ∈ X ∪ Σ and 0 ≤ i ≤ n and n > 0. Note that in the case (a), a_{i} can have free variables among x⃗, hence it can also be a subterm of a term α-equivalent to λx⃗.va⃗; for instance λx.fx ≻ y for all y ∈ X. Recall that WN_{β} is the set of weakly β-normalizing terms.

Lemma 4.10 If s ∈ WN_{β} and s ≻ t then t ∈ WN_{β}. Moreover, ≻ is well-founded on WN_{β}.

Proof. For the first part, let 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 leftmost-outermost strategy starting from s reduces each a_{i} by leftmost-outermost reductions. Hence #(s) ≥ #(t). But in this case, t is a proper subterm of s, hence |s| > |t|.

It follows that we can reason by well-founded induction on ≻. For all i ≥ 0, we use a nested parallelization of )_{R_{i}}. It corresponds to the one used in [OR94], 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 )_{R_{i}} can be simulated by one step ⊳_{R_{i}} -reduction. This relation is also an adaptation to conditional rewriting of the parallelization used in [Dou92].

Definition 4.11 (Conditional Nested Parallel Relations) For all i ≥ 0, let ⊳_{R_{i}} be the smallest parallel rewrite relation closed under the rule

(⊳R) \frac{d⃗ = c⃗ ⊃ l )_{R} r  lσ )_{R_{i}} rσ  σ ⊳_{R_{i}} θ}{lσ ⊳_{R_{i}} rθ}

Recall that lσ )_{R_{i}} rσ is ensured by d⃗σ ]_{R_{i−1}} c⃗σ. These relations enjoy some nice properties:

Proposition 4.12 For all i ≥ 0,

(i) )_{R_{i}} ⊆ ⊳_{R_{i}} ⊆ )_{R_{i}}^{∗};

(ii) s ⊳_{R_{i}} t =} u[s/x] ⊳_{R_{i}} u[t/x] ;

(iii) [s ⊳_{R_{i}} t & u ⊳_{R_{i}} v] =} u[s/x] ⊳_{R_{i}} v[t/x].

Proof. The first point is shown by induction on the definition of ⊳_{R_{i}} ; the second follows from Proposition 2.6 and the fact that ⊳_{R_{i}} is a parallel rewrite relation. For the last one, we use an induction on ⊳_{R_{i}} in u ⊳_{R_{i}} v. If u is v, the result is trivial. If u ⊳_{R_{i}} v was obtained by (⊳App) or (Abs), the result follows from induction hypothesis. Otherwise, u ⊳_{R_{i}} v is obtained by ⊳R. That is, there is a rule d⃗ = c⃗ ⊃ l )_{R} r such that u = lσ, v = rθ, σ ⊳_{R_{i}} θ and lσ )_{R_{i}} rσ. Since )_{R_{i}} is a rewrite relation, we have lσ[s/x] ⊳_{R_{i}} rσ[s/x]. By induction hypothesis, we have σ[s/x] ⊳_{R_{i}} θ[t/x]. Therefore lσ[s/x] ⊳_{R_{i}} rθ[t/x].

We now turn to the one step commutation of ⊳_{R_{i}} and )_{h}. This is a direct consequence of the third point of Proposition 4.12. Commutation of )_{h} with (unconditional) rewriting has already be coined in [BFG97].

Lemma 4.13 Let i ≥ 0. If u (_{h} s ⊳_{R_{i}} t then there exists v such that u ⊳_{R_{i}} v (_{h} t :

\xymatrix{s \ar[r]^{⊳_{R_{i}}} \ar[d]_{h} & t \ar@{.>}[d]^{h} \\ u \ar@{.>}[r]_{⊳_{R_{i}}} & v}

Proof. Assume that s (_{h} λx⃗.(λy.a_{0})a_{1} …a_{p} ⊳_{R_{i}} t. Because rules have non-variable algebraic left-hand sides, t = λx⃗.(λy.b_{0})b_{1} …b_{p} with for all k ∈ {0, …, p}, a_{k} ⊳_{R_{i}} b_{k}. On the other hand, s = λx⃗.a_{0}[a_{1}/y]a_{2} …a_{p}. It follows from Proposition 4.12.(iii) that a_{0}[a_{1}/x] ⊳_{R_{i}} b_{0}[b_{1}/x] (in one step). Hence we have s ⊳_{R_{i}} λx⃗.b_{0}[b_{1}/y]b_{2} …b_{p} (_{h} t.

The main lemma is the projection of rewriting on β-normal forms, that is, the commutation of diagram (4).

Lemma 4.14 Let a : Σ ) ℕ be an arity and R be an algebraic conditional rewrite system which respects a. For all i ∈ ℕ, if t ∈ AN_{a} and t )_{β∪R_{i}}^{∗} u, then u ∈ AN_{a} and βnf(t) )_{R_{i}}^{∗} βnf(u).

Proof. We reason by induction on i ∈ ℕ. The base case i = 0 is trivial. We assume that the property holds for i ≥ 0 and show it for i + 1. The proof is in two steps.

(i) We begin by showing that for all t ∈ AN_{a} we have

\xymatrix{t \ar[r]^{⊳_{R_{i+1}}} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ βnf(t) \ar@{.>}[r]_{⊳_{R_{i+1}}} & βnf(u)}  (5)

We reason by induction on ≻ using Lemma 2.3. t = λx⃗.xt_{1} …t_{n}. In this case, βnf(t) = λx⃗.x βnf(t_{1}) …βnf(t_{n}) and u = λx⃗.xu_{1} …u_{n}

with t_{k} ⊳_{R_{i+1}} u_{k} for all k ∈ {1, …, n}. As t ≻ t_{k}, for all k ∈ {1, …, n}, by induction hypothesis on ≻ we have u_{k} ∈ AN_{a} and βnf(t_{k}) ⊳_{R_{i+1}} βnf(u_{k}). Since βnf(u) = λx⃗.x βnf(u_{1}) …βnf(u_{n}), we have βnf(u) ∈ AN_{a} and βnf(t) ⊳_{R_{i+1}} βnf(u).

t = λx⃗.ft_{1} …t_{n}. If no rule is reduced at the head of t, the result follows from induction hypothesis on ≻. Otherwise, there is a rule d⃗ = c⃗ ⊃ l ) r such that t = λx⃗.lσa⃗ and u = λx⃗.rθb⃗ with lσ⊳_{R_{i+1}} rθ and d⃗σ ]_{R_{i}} c⃗σ. Since l is algebraic, βnf(t) is of the form λx⃗.lσ′a⃗′ where σ′ = βnf(σ) and a⃗′ = βnf(a⃗). Since βnf(t) respects a, a⃗′ = ∅, hence a⃗ = ∅ and t = λx⃗.lσ. Therefore, because lσ ⊳_{R_{i+1}} rθ, we have b⃗ = ∅ and u = λx⃗.rθ. It remains to show that u ∈ AN_{a} and that βnf(t) = λx⃗.lσ′ ⊳_{R_{i+1}} βnf(u). Because l is algebraic, its variables are ≺^{+} l. We can then apply induction hypothesis on σ ⊳_{R_{i+1}} θ. It follows that θ has a β-normal form θ′, which respects a and moreover such that σ′ ⊳_{R_{i+1}} θ′. Since r is algebraic, λx⃗.rθ′ is the β-normal form of u (which respects a). Hence it remains to show that lσ′ ⊳_{R_{i+1}} rθ′. Because σ′ ⊳_{R_{i+1}} θ′, it suffices to prove that lσ′ )_{R_{i+1}} rσ′. Thus, we are done if we show that d⃗σ′ ]_{R_{i}} c⃗σ′. Since d⃗ and c⃗ are algebraic, βnf(d⃗σ) = d⃗σ′ and βnf(c⃗σ) = c⃗σ′. Now, since d⃗ is algebraic and respects a, and since σ′ respects a, it follows that d⃗σ′ respects a. The same holds for c⃗σ′. Hence we conclude by applying on d⃗σ ]_{R_{i}} c⃗σ the induction hypothesis on i.

t = λx⃗.(λx.v)wt_{1} …t_{n}. In this case, we head β-normalize t and obtain a term t′ ∈ AN_{a}. Using the commutation of ⊳_{R_{i+1}} and )_{h}, we obtain a term u′ such that t′ ⊳_{R_{i+1}} u′. Since t ≻^{+} t′, we can reason as in the preceding cases.

(ii) We now show that t )_{β∪R_{i}}^{∗} u implies βnf(t) )_{R_{i}}^{∗} βnf(u). We reason by induction on t )_{β∪R_{i}}^{∗} u, using Proposition 4.12.(i). The base case t = u is trivial. Assume that t )_{β∪R_{i}} v )_{β∪R_{i}}^{∗} u. By induction hypothesis we have βnf(v) )_{R_{i}}^{∗} βnf(u). There are two cases. If t )_{β} v, then βnf(t) = βnf(v) and we are done. Otherwise we have t )_{R_{i}} v, hence βnf(t) )_{R_{i}}^{∗} βnf(v) )_{R_{i}}^{∗} βnf(u) by (i).

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

Theorem 4.15 Let a : Σ ) ℕ be an arity and R be an algebraic conditional rewrite system which respects a. If )_{R} is confluent on AN_{a}, then )_{β∪R} is confluent on AN_{a}.

Proof. Let s, t, u such that s ∈ AN_{a} and u (_{β∪R}^{∗} s )_{β∪R}^{∗} t. By two applications of Lemma 4.14 we get that βnf(u) (_{R}^{∗} βnf(s) )_{R}^{∗} βnf(t), with moreover βnf(s), βnf(t) and βnf(u) ∈ AN_{a}. Hence we conclude by )_{R}-confluence on AN_{a}. In diagrammatic form,

\xymatrix{ & s \ar[dr]^{β∪R}_{∗} \ar[dl]_{β∪R}^{∗} \ar@{.>}[d]_{β}^{∗} \\ u \ar@{.>}[d]_{β}^{∗} & βnf(s) \ar@{.>}[dr]_{R}^{∗} \ar@{.>}[dl]^{R}_{∗} & t \ar@{.>}[d]^{β}_{∗} \\ βnf(u) \ar@{.>}[dr]^{R}_{∗} &  & βnf(t) \ar@{.>}[dl]_{R}^{∗} \\  & v}

5 Using beta-reduction in the evaluation of conditions

In this section we focus on the combination of β-reduction with the join β-conditional rewrite relation )_{R(β)} issued from a conditional rewrite system R (see Definition 2.9).

We give sufficient conditions on R to deduce the confluence of )_{β∪R(β)} from the confluence of )_{R}. We achieve this by exhibiting two different criteria ensuring that derivations combining β-reduction and β-conditional rewriting can be projected, via β-reductions, to derivations made of conditional rewriting only (hence without using β-reduction in the evaluation of conditions):

\xymatrix{s \ar[r]^{β∪R(β)}_{∗} \ar@{.>}[d]_{β}^{∗} & t \ar@{.>}[d]^{β}_{∗} \\ s′ \ar@{.>}[r]_{R}^{∗} & t′}  (6)

It is easy to see that property (6) combined to the confluence of )_{β∪R} entails the confluence of )_{R}. We can actually prove property (6) on some subsets of Λ(Σ) only. This motivates the assumptions on the following proposition.

Proposition 5.1 Let R be a conditional rewrite system and S ⊆ Λ(Σ) be a set of terms closed under )_{β∪R(β)} . Assume that )_{β∪R} is confluent on S. If property (6) is satisfied for all s, t ∈ S then )_{β∪R(β)} is confluent on S.

Proof. Let t ∈ S and u, v such that

u (_{β∪R(β)}^{∗} t )_{β∪R(β)}^{∗} v .

Note that u, v ∈ S since S is closed under )_{β∪R(β)} . By property (6) applied twice and by confluence of )_{β∪R} on S, there is w such that u )_{β∪R}^{∗} w (_{β∪R}^{∗} v. We conclude by the fact that )_{R}⊆)_{R(β)}. In diagrammatic form,

\xymatrix{ & u \ar@{.>}[dl]_{β}^{∗} &  & t \ar[ll]_{β∪R(β)}^{∗} \ar[rr]^{β∪R(β)}_{∗} \ar@{.>}[dr]_{β}^{∗} \ar@{.>}[dl]^{β}_{∗} &  & v \ar@{.>}[dr]^{β}_{∗} \\ · \ar@{.>}[drrr]_{β∪R}^{∗} &  & · \ar@{.>}[ll]_{R}^{∗} &  & · \ar@{.>}[rr]^{R}_{∗} &  & · \ar@{.>}[dlll]^{β∪R}_{∗} \\  &  &  & w}

Our two different criteria to obtain (6) are the extensions to β-conditional rewriting of the two criteria studied for conditional rewriting in Section 4.

— The first one concerns left-linear (and semi-closed) rewriting, with no termination assumption on β-reduction.

— The second one concerns arity-preserving algebraic rewriting, with a weak-normalization assumption on β-reduction.

In the left-linear and semi-closed case, allowing β-reduction in the evaluation of conditions imposes us to put stronger assumptions on R than for conditional rewriting in Section 4.1: rewrite rules need to be algebraic and to respect and arity. Recall that these assumptions were already made in Section 4.2 when considering possibly non left-linear rewriting on weakly β-normalizing terms.

The following example presents rules which either are not algebraic or do not respect the arity prescribed by left-hand sides. With these rules property (6) fails and )_{β∪R(β)} is not confluent whereas )_{R} and )_{β∪R} are confluent.

Example 5.2 With the conditional rewrite systems (7), (8), (9) and (10) below,

(i) the relations )_{R} and )_{β∪R} are confluent,

(ii) property (6) is not satisfied and the relation )_{β∪R(β)} is not confluent.

g x y ) x y  g x c = d ⊃ f x ) a x  f x ) b x  (7)
x c = d ⊃ f x ) a x  f x ) b x  (8)
id x c = d ⊃ f x ) a x  f x ) b x  (9)
h x y ) id x y  h x c = d ⊃ f x ) a x  f x ) b x  (10)

where id is defined by id x ) x.

Proof.

(i) Since the symbol d is not defined, these systems lead to normal conditional rewrite relations. Since they are left-linear and semi-closed, we can apply Theorem 4.7, and deduce the confluence of )_{β∪R} from the confluence of )_{R}. Since they are left-linear systems, if their critical pairs are unfeasible, we can obtain the confluence of )_{R} by Theorem 3.12. Each system has a unique conditional rule and a unique critical pair, issued from the root superposition of this rule with f x ) b x. In each case, the number of occurrences of the symbol c in a term is preserved by )_{R}. Moreover, for each instantiation of the conditional rule, the instantiated left-hand side of the condition contains at least one occurrence of c. It follows that it cannot reduce to d, and that the critical pair is unfeasible. Therefore, we obtain the confluence of )_{R} by Theorem 3.12. and we deduce the confluence of )_{β∪R} thanks to Theorem 4.7.

(ii) In each case, the step f λx.d )_{R(β)} a λx.d is not in )_{β}^{∗})_{R}^{∗}(_{β}^{∗} and the following peak is

unjoinable

a λx.d (_{R(β)} f λx.d )_{R(β)} b λx.d .

Note that systems (7) and (8) contain respectively a right-hand side and a condition which are not algebraic, and that systems (9) and (10) contain respectively a right-hand side and a condition that do not respect the arity of id imposed by the rewrite rule idx ) x.

Note also that (6) is reminiscent of a property required on the substitution calculus used in [OR94]. This would require to see )_{β} as the substitution calculus. But this does not fit in our framework, in particular because we consider )_{β} and rewriting at the same level. Moreover, the substitution calculus used in [OR94] is required to be complete (i.e. strongly normalizing and confluent), which is not the case here for )_{β}.

Outline. We begin in Section 5.1 by the extension of Theorem 4.6 to β-conditional rewriting for left-linear and semi-closed systems. In this case, preservation of confluence only holds on terms respecting an arity (namely conditionally (R, a)-stable terms, see Definition 5.5). This is an extra hypothesis compared to the results of Section 4.1. Then, in Section 5.2 we consider the case of Theorem 4.15. It directly extends to β-conditional rewriting. In both cases, we assume that rules are algebraic and respect an arity. In each case our assumptions ensure that the results of Section 4 apply, hence that )_{β∪R} is confluent whenever )_{R} is confluent. Hence, using Proposition 5.1 we deduce the confluence of )_{β∪R(β)} from the confluence of )_{R} and property (6).

Remarks. In [BKR06], we have shown (6) by using a stratification of )_{R(β)} in which, instead of having )_{R(β)_{0}} = ∅ as in Definition 2.9, we had )_{R(β)_{0}} =)_{β} (it is easy to show that these two base cases induce the same relation )_{R(β)}).

We proceed here in a slightly different and more general way. We show (6) with )_{R(β)_{0}} = ∅ and use the following intermediate property: for all i ∈ ℕ,

\xymatrix{t \ar[r]^{β∪R(β)_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ t′ \ar@{.>}[r]_{R_{i}}^{∗} & u′}  (11)

5.1 Confluence for left-linear semi-closed systems

This section is devoted to the proof of (11) for left-linear semi-closed systems. Using Proposition 5.1 and Theorem 4.6, we then easily deduce the confluence of )_{β∪R(β)} when )_{R} is confluent. We postpone the proof of (11) until Lemma 5.9, Section 5.1.2. The material used in the proof is presented and motivated in Section 5.1.1 below.

5.1.1 Preliminaries

The proof of (11) involves some intermediate lemmas and the extension of (R, a)-stable sets of terms to conditional rewriting. In order to motivate them, we sketch some steps of the proof. Property (11) is proved by induction on i ∈ ℕ. Assuming the property for i ∈ ℕ, we discuss it for i + 1. We reason by induction on the length of the derivation t )_{β∪R(β)_{i+1}}^{∗} u. We present the ingredients used in the different steps of this induction.

The base case. In the base case, we have t )_{β∪R(β)_{i+1}} u in one step. The case of t )_{β} u is trivial: take t′ =_{def} u′ =_{def} u. The case of t )_{R(β)_{i+1}} u is more involved. We show

\xymatrix{t \ar[r]^{R(β)_{i+1}} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ t′ \ar@{.>}[r]_{R_{i+1}} & u′}  (12)

Consider a rule d⃗ = c⃗ ⊃ l )_{R} r. Recall from Example 5.2 that it must be algebraic and respect an arity. Hence every β-redex occurring in d⃗σ or c⃗σ also occurs in lσ. Then, property (12) means that there is a β-reduction starting from lσ that reduces these redexes and produce a substitution σ′ such that

lσ )_{β}^{∗} lσ′ )_{R_{i+1}} rσ′ (_{β}^{∗} rσ .

In other words, if the conditions are satisfied with σ and )_{β∪R(β)_{i}} (i.e. d⃗σ ]_{β∪R(β)_{i}} c⃗, recall that c⃗ are closed terms since R is semi-closed), then they are satisfied with σ′ and )_{R_{i}} (i.e. d⃗σ′ ]_{R_{i}} c⃗). Let us look at this more precisely. Assume that d⃗σ ]_{β∪R(β)_{i}} c⃗. Hence there are terms v⃗ such that

d⃗σ )_{β∪R(β)_{i}}^{∗}  v⃗ (_{β∪R(β)_{i}}^{∗}  c⃗ .

By induction hypothesis on i, we get terms w⃗ and v⃗′ such that

\xymatrix{d⃗σ \ar[r]^{β∪R(β)_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & v⃗ \ar@{.>}[d]^{β}_{∗} & c⃗ \ar[l]_{β∪R(β)_{i}}^{∗} \\ w⃗ \ar@{.>}[r]_{R_{i}}^{∗} & v⃗′}

In order to conclude, we need a substitution σ′ such that σ )_{β}^{∗} σ′ and w⃗ )_{β}^{∗} d⃗σ′. Using the algebraicity of d⃗, this follows from Proposition 5.4, which is stated and proved below. The remaining of the proof uses the commutation of )_{β} and )_{R_{i}} (Lemma 4.5) and relies on the semi-closure and the right-applicativity of R (which follows from its algebraicity). See the proof of Lemma 5.9 in Section 5.1.2 for details.

We need to show that if t is an algebraic term such that tσ )_{β}^{∗} v, then there is a substitution σ′ such that σ )_{β}^{∗} σ′ and v )_{β}^{∗} tσ′. This is provided by the two following technical propositions. The first one is a generalization of the diamond property of ⊳_{β}. It is a direct consequence of Lemma 3.2 in [Tak95].

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

We deduce the following property. The proof of case (ii) uses the diamond property of ⊳_{β}.

Proposition 5.4 Let t_{1}, …, t_{n} be algebraic terms and let σ be a substitution.

(i) If t_{i}σ ⊳_{β} u_{i} for all i ∈ {1, …, n}, then there is a substitution σ′ such that σ ⊳_{β} σ′ and u_{i} ⊳_{β} t_{i}σ′ for all i ∈ {1, …, n}.

(ii) If t_{i}σ )_{β}^{∗} u_{i} for all i ∈ {1, …, n}, then there is a substitution σ′ such that σ )_{β}^{∗} σ′ and u_{i} )_{β}^{∗} t_{i}σ′ for all i ∈ {1, …, n}.

Note that the terms t_{1}, …, t_{n} need not be linear.

Proof.

(i) Since t_{i} is algebraic, every occurrence of a β-redex in t_{i} is of the form p.d where p is an occurrence of a variable x in t_{i}. Since ⊳_{β} is reflexive, for each i ∈ {1, …, n}, each x ∈ FV(t_{i}) and each p ∈ Occ(x, t_{i}), there is a term s_{(i,x,p)} such that

t_{i}σ|_{p} = σ(x) ⊳_{β} s_{(i,x,p)}

and for all i ∈ {1, …, n},

u_{i} = t_{i}[p ( s_{(i,x,p)} | x ∈ FV(t_{i}) ∧ p ∈ Occ(x, t_{i})] .

By Proposition 5.3, for all x ∈ FV(t_{1}, …, t_{n}), there is a term v_{x} such that σ(x) ⊳_{β} v_{x} and s_{(i,x,p)} ⊳_{β} v_{x} for all i ∈ {1, …, n} and all p ∈ Occ(x, t_{i}). Therefore, for all i ∈ {1, …, n} we have

u_{i} ⊳_{β} t_{i}[p ( v_{x} | x ∈ FV(t_{i}) ∧ p ∈ Occ(x, t_{i})] .

Let σ′ be the substitution of same domain as σ such that σ′(x) = v_{x} for all x ∈ FV(t_{1}, …, t_{n}) and σ′(x) = σ(x) for all x ∉ FV(t_{1}, …, t_{n}). Then we have σ ⊳_{β} σ′ and u_{i} ⊳_{β} t_{i}σ′ for all i ∈ {1, …, n}.

(ii) By induction on k ∈ ℕ, we show that if t_{i}σ ⊳_{β}^{k} u_{i} for all i ∈ {1, …, n}, then there is σ′ such that σ ⊳_{β}^{∗} σ′ and u_{i} ⊳_{β}^{∗} t_{i}σ′ for all i ∈ {1, …, n}.

The base case t_{i}σ ⊳_{β}^{0} u_{i} for all i ∈ {1, …, n} is trivial. For the induction case, there are u′_{1}, …, u′_{n} such that t_{i}σ ⊳_{β}^{k} u′_{i} ⊳_{β} u_{i} for all i ∈ {1, …, n}. Then, by (i), there is σ′ such that σ ⊳_{β} σ′ and u′_{i} ⊳_{β} t_{i}σ′ for all i ∈ {1, …, n}. Since ⊳_{β} satisfies the diamond property (Proposition 5.3), for all i ∈ {1, …, n} there is u′′_{i} such that t_{i}σ′ ⊳_{β}^{k} u′′_{i} ⊲_{β} u_{i}, and by induction hypothesis on k, there is σ′′ such that σ′ ⊳_{β}^{∗} σ′′ and u′′_{i} ⊳_{β}^{∗} t_{i}σ′′ for all i ∈ {1, …, n}. We deduce that u_{i} ⊳_{β}^{∗} t_{i}σ′′ for all i ∈ {1, …, n}.

In diagrammatic form:

\xymatrix{t⃗σ \ar[r]^{⊳_{β}} & u⃗′ \ar[r]^{⊳_{β}}_{k} \ar@{.>}[d]_{⊳_{β}} & u⃗ \ar@{.>}[d]^{⊳_{β}} \\  & t⃗σ′ \ar@{.>}[r]_{⊳_{β}}^{k} & u⃗′′ \ar@{.>}[d]^{⊳_{β}}_{∗} \\  &  & _{t⃗σ′′}}

The induction case. In the induction case, we have t )_{β∪R(β)_{i+1}}^{∗} u in more than one step. Hence, this derivation can be written as t )_{β∪R(β)_{i+1}} v )_{β∪R(β)_{i+1}}^{∗} u for some v. If t )_{β} v, then we easily conclude by induction hypothesis on v )_{β∪R(β)_{i+1}}^{∗} u. Otherwise, we have t )_{R(β)_{i+1}} v and things get more involved. Using the induction hypothesis on v )_{β∪R(β)_{i+1}}^{∗} u and the discussion of the above paragraph for t )_{R(β)_{i+1}} v, we arrive at the following situation:

\xymatrix{ & t \ar[rr]^{R(β)_{i+1}} \ar@{.>}[dl]_{β}^{∗} &  & v \ar[rr]^{β∪R(β)_{i+1}}_{∗} \ar@{.>}[dl]^{β}_{∗} \ar@{.>}[dr]_{β}^{∗} &  & u \ar@{.>}[dr]^{β}_{∗} \\ t′ \ar@{.>}[rr]_{R_{i+1}} &  & v′′ &  & v′ \ar@{.>}[rr]_{R_{i+1}}^{∗} &  & u′}

Using the confluence of )_{β} and the commutation of )_{β} with )_{R_{i}} (Lemma 4.5), we get

\xymatrix{ & t \ar[rr]^{R(β)_{i+1}} \ar@{.>}[dl]_{β}^{∗} &  & v \ar[rr]^{β∪R(β)_{i+1}}_{∗} \ar@{.>}[dl]^{β}_{∗} \ar@{.>}[dr]_{β}^{∗} &  & u \ar@{.>}[dr]^{β}_{∗} \\ t′ \ar@{.>}[rr]_{R_{i+1}} &  & v′′ \ar@{.>}[dr]^{β}_{∗} &  & v′ \ar@{.>}[rr]_{R_{i+1}}^{∗} \ar@{.>}[dl]_{β}^{∗} &  & u′ \ar@{.>}[dl]^{β}_{∗} \\  &  &  & v′′′ \ar@{.>}[rr]_{R_{i+1}}^{∗} &  & u′′}

In order to conclude we use the following property: for all i ∈ ℕ,

\xymatrix{t \ar[r]^{β∪R_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ t′ \ar@{.>}[r]_{R_{i}}^{∗} & u′}  (13)

The intricate case of property (13) is when there is an R_{i}-step followed by a β-step:

t )_{R_{i}} v )_{β} u .

In this case, we have to make sure that the step t )_{R_{i}} v did not create the β-redex contracted in v )_{β} u. As seen in Section 3.1, this follows from arity assumptions on terms.

We therefore use terms whose arity is compatible with that of the rewrite system. We need this property to be preserved by )_{β∪R(β)} , but also by the conditions of rewrite rules: given a semi-closed rule d⃗ = c⃗ ⊃ l )_{R} r and a substitution σ, if lσ respects a : Σ ) ℕ, then the terms rσ, d⃗σ should also respect a. This is the case when r, d⃗ are algebraic and respect a. Moreover, in the following we have to make sure that every term at hand satisfy these properties. In particular, if we have a rule d⃗ = c⃗ ⊃ l ) r such that lσ and all its reducts respect an arity a, this has to be the case of d⃗σ too (the case of c⃗ follows from semi-closure). Hence, we consider sets of terms which are stable under the rewrite relation )\overline{R} issued from the rewrite system

\begin{aligned})\overline{R} & =_{def} & \{(l, d_{i}) | & d_{1} = c_{1} ∧ … ∧ d_{n} = c_{n} ⊃ l )_{R} r ∧ i ∈ \{1, …, n\}\} \\ & ∪ & \{(l, r) | & d_{1} = c_{1} ∧ … ∧ d_{n} = c_{n} ⊃ l )_{R} r\} . \end{aligned}

This motivates the following definition, which extends (R, a)-stability (Definition 3.6) to conditional rewriting.

Definition 5.5 (Conditionally (R, a)-Stable Terms) Let a : Σ ) ℕ be an arity and R be a conditional rewrite system. A set of terms S is conditionally (R, a)-stable if it is (\overline{R}, a)-stable.

We now show (13). The proof of this property occupies Proposition 5.6 and Lemma 5.7. Note that we prove Proposition 5.6 for systems whose conditions need not be algebraic. However, this property may fail in presence of right-hand sides which either are not algebraic or do not respect the arity prescribed by the left-hand sides. Note also that we work on conditionally (R, a)-stable terms.

Proposition 5.6 Let R be a left-linear semi-closed system which is right-algebraic and respects a : Σ ) ℕ, and let S ⊆ Λ(Σ) be conditionally (R, a)-stable. For all i ∈ ℕ and all t, u, v ∈ S, if t )_{R_{i}} u ⊳_{β} v, then there are t′ and v′ such that t ⊳_{β} t′ )_{R_{i}}^{∗} v′ ⊲_{β} v :

\xymatrix{t \ar[r]^{R_{i}} \ar@{.>}[d]_{⊳_{β}} & u \ar[r]^{⊳_{β}} & v \ar@{.>}[d]^{⊳_{β}} \\ t′ \ar@{.>}[rr]_{R_{i}}^{∗} &  & v′}

Proof. The base case i = 0 is trivial, and we assume i > 0. We reason by induction on t using Lemma 2.3.

t = λx⃗.x t_{1} …t_{n}. In this case, u = λx⃗.xu_{1} …u_{n} with (t_{1}, …, t_{n}) )_{R_{i}} (u_{1}, …, u_{n}). Moreover, v = λx⃗.x v_{1} …v_{n} with (u_{1}, …, u_{n}) ⊳_{β} (v_{1}, …, v_{n}). By induction hypothesis, there are (t′_{1}, …, t′_{n}) and (v′_{1}, …, v′_{n}) such that

(t_{1}, …, t_{n}) ⊳_{β} (t′_{1}, …, t′_{n}) )_{R_{i}}^{∗} (v′_{1}, …, v′_{n}) ⊲_{β} (v_{1}, …, v_{n}) .

It follows that

λx⃗.x t_{1} …t_{n} ⊳_{β} λx⃗.x t′_{1} …t′_{n} )_{R_{i}}^{∗} λx⃗.x v′_{1} …v′_{n} ⊲_{β} λx⃗.x v_{1} …v_{n} .

t = λx⃗.ft_{1} …t_{n}. If u = λx⃗.fu_{1} …u_{n} with

(t_{1}, …, t_{n}) )_{R_{i}} (u_{1}, …, u_{n}) ,

then v = λx⃗.fv_{1} …v_{n} with (u_{1}, …, u_{n}) ⊳_{β} (v_{1}, …, v_{n}) and we reason as in the previous case.

Otherwise, there is a rule d⃗ = c⃗ ⊃ l )_{R} r, a substitution σ and k ∈ {1, …, n} such that t = λx⃗.lσt_{k+1} …t_{n} and u = λx⃗.rσt_{k+1} …t_{n}. As t and R respect a, we have n = k, hence t = λx⃗.lσ, u = λx⃗.rσ and v = λx⃗.w with rσ ⊳_{β} w.

Since r is algebraic, by Proposition 5.4.(i) there is σ′ such that σ ⊳_{β} σ′ and w ⊳_{β} rσ′. As l is linear, by Proposition 4.4 we have lσ ⊳_{β} lσ′. It remains to show that lσ′ )_{R_{i}} rσ′. Since lσ )_{R_{i}} rσ, there are terms v⃗ such that d⃗σ )_{R_{i−1}}^{∗} v⃗ (_{R_{i−1}}^{∗} c⃗. Since d⃗σ )_{β}^{∗} d⃗σ′, by Lemma 4.5, we obtain terms v⃗′ such that

d⃗σ )_{β}^{∗} d⃗σ′ )_{R_{i−1}}^{∗}  v⃗′ (_{β}^{∗} v⃗ (_{R_{i−1}}^{∗}  c⃗ .

Since terms c⃗ are applicative and closed, they are algebraic, and since R is right-algebraic, terms v⃗ are also algebraic, hence in β-normal form. It follows that v⃗ = v⃗′, hence that d⃗σ′ ]_{R_{i−1}} c⃗, and we deduce that lσ′ )_{R_{i}} rσ′.

t = λx⃗.(λx.t_{0})t_{1} …t_{n} (n ≥ 1). Then u is of the form u = λx⃗.(λx.u_{0})u_{1} …u_{n} and we have (t_{0}, …, t_{n}) )_{R_{i}} (u_{0}, …, u_{n}). If v = λx⃗.(λx.v_{0})v_{1} …v_{n} with

(u_{0}, …, u_{n}) ⊳_{β} (v_{0}, …, v_{n}) ,

then we conclude by induction hypothesis, as in the first case.

Otherwise, v = λx⃗.v_{0}[v_{1}/x]v_{2} …v_{n} with (u_{0}, …, u_{n}) ⊳_{β} (v_{0}, …, v_{n}). By induction hypothesis, we have

(t_{0}, …, t_{n}) ⊳_{β} (t′_{0}, …, t′_{n}) )_{R_{i}}^{∗} (v′_{0}, …, v′_{n}) ⊲_{β} (v_{0}, …, v_{n}) .

It follows that by using (⊳β), (⊳App) we have

λx⃗.(λx.t_{0})t_{1} …t_{n}  λx⃗.v_{0}[v_{1}/x]v_{2} …v_{n}
▽_{β}  ▽_{β}
λx⃗.t′_{0}[t′_{1}/x]t′_{2} …t′_{n}  )_{R_{i}}^{∗} λx⃗.v′_{0}[v′_{1}/x]v′_{2} …v′_{n} .

Lemma 5.7 Let R be a semi-closed left-linear right-algebraic system which respects a : Σ ) ℕ, and let S ⊆ Λ(Σ) be conditionally (R, a)-stable. For all s, t ∈ S, if s )_{β∪R_{i}}^{∗} t then there are s′, t′ such that s )_{β}^{∗} s′ )_{R_{i}}^{∗} t′ (_{β}^{∗} t :

\xymatrix{s \ar[r]^{β∪R_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & t \ar@{.>}[d]^{β}_{∗} \\ s′ \ar@{.>}[r]_{R_{i}}^{∗} & t′}

Proof. The proof is in three steps.

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

(ii) We show )_{R_{i}}^{∗} ⊳_{β}^{∗} ⊆ ⊳_{β}^{∗} )_{R_{i}}^{∗} ⊲_{β}^{∗} by induction on the number of ⊳_{β} -steps. Assume that s )_{R_{i}}^{∗} t ⊳_{β} u′ ⊳_{β}^{∗} u. After (i), there are s′ and t′ such that s ⊳_{β} s′ )_{R_{i}}^{∗} t′ ⊲_{β}^{∗} u′. By the diamond property 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′′ )_{R_{i}}^{∗} t′′ ⊲_{β}^{∗} v. Therefore, s ⊳_{β}^{∗} s′′ )_{R_{i}}^{∗} t′′ ⊲_{β}^{∗} u.

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

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

Remark. Note that β-reduction is the only way to obtain a term not respecting a from a term respecting it. For instance, with a(id) = 1 the term (λx.x y y)id respects a whereas id y y does not respect a.

Proposition 5.8 Let R be an algebraic conditional rewrite system and t ∈ Λ(Σ) that both respect a : Σ ) ℕ. If t )_{R(β)} u then u respects a.

Proof. We reason by induction on t, using Lemma 2.3. The only case which does not directly follow from the induction hypothesis is when t = λx⃗.ft_{1} …t_{n} and there is a rule d⃗ = c⃗ ⊃ l )_{R} r, a substitution σ and k ∈ {1, …, n} such that t = λx⃗.lσt_{k+1} …t_{n}. Since t and R respect a, we have k = n. Hence u = λx⃗.rσ and u respects a since r is an algebraic term that respects a.

5.1.2 Confluence of beta-reduction with beta-conditional rewriting

We now have all we need to show property (11). As seen in Example 5.2, rules have to be algebraic and arity compliant. We reason by induction on i ∈ ℕ.

Lemma 5.9 Let R be a semi-closed left-linear algebraic system which respects a : Σ ) ℕ, and let S ⊆ Λ(Σ) be conditionally (R, a)-stable. For all t, u ∈ S, if t )_{β∪R(β)_{i}}^{∗} u then there are t′, u′ such that t )_{β}^{∗} t′ )_{R_{i}}^{∗} u′ (_{β}^{∗} u :

\xymatrix{t \ar[r]^{β∪R(β)_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ t′ \ar@{.>}[r]_{R_{i}}^{∗} & u′}  (14)

Proof. We show (14) by induction on i ∈ ℕ. The base case i = 0 is trivial. We assume that the property holds for i ≥ 0 and show it for i + 1. The proof is in two steps.

(i) We begin by showing that diagram (15) commutes:

\xymatrix{t \ar[r]^{R(β)_{i+1}} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ t′ \ar@{.>}[r]_{R_{i+1}} & u′}  (15)

We reason by induction on t, using Lemma 2.3. The only case that does not directly follow from the induction hypothesis is when t = λx⃗.ft_{1} …t_{n} and there is a rule d⃗ = c⃗ ⊃ l )_{R} r, a substitution σ and k ∈ {1, …, n} such that t = λx⃗.lσt_{k+1} …t_{n} and u = λx⃗.rσt_{k+1} …t_{n} with lσ )_{R(β)_{i+1}} rσ. Since t and R respect a, we have k = n, hence u = λx⃗.rσ.

To deduce (15), it remains to show that there is a substitution σ′ such that

lσ )_{β}^{∗} lσ′ )_{R_{i+1}} rσ′ (_{β}^{∗} rσ .

Since lσ )_{R(β)_{i+1}} rσ, there are terms v⃗ such that d⃗σ )_{β∪R(β)_{i}}^{∗} v⃗ (_{β∪R(β)_{i}}^{∗} c⃗. By induction hypothesis on i, there are terms w⃗ and v⃗′ such that

d⃗σ )_{β}^{∗} w⃗ )_{R_{i}}^{∗} v⃗′ (_{β}^{∗} v⃗ .

By Proposition 5.4.(ii), as terms d⃗ are algebraic there is a substitution σ′ such that σ )_{β}^{∗} σ′ and w⃗ )_{β}^{∗} d⃗σ′. By Lemma 4.5 (commutation of )_{R_{i}} with )_{β}), we obtain terms v⃗′ such that d⃗σ′ )_{R_{i}}^{∗} v⃗′ (_{β}^{∗} v⃗. It follows that

d⃗σ )_{β}^{∗} d⃗σ′ )_{R_{i}}^{∗} v⃗′ (_{β}^{∗} v⃗ (_{β∪R(β)_{i}}^{∗} c⃗ .

Since terms c⃗ are algebraic and R is right-applicative, every reduct of c⃗ by )_{R(β)} is βnormal. We thus have v⃗′ = v⃗ and by induction hypothesis on i we deduce that c⃗ )_{R_{i}}^{∗} v⃗. It follows that d⃗σ′ ]_{R_{i}} c⃗, hence lσ′ )_{R_{i+1}} rσ′. We have lσ )_{β}^{∗} lσ′ and rσ )_{β}^{∗} rσ′ since σ )^{∗} σ′, hence

t )_{β}^{∗} λx⃗.lσ′ )_{R_{i+1}} λx⃗.rσ′ (_{β}^{∗} u .

(ii) We now show (14) by induction on the length of t )_{β∪R(β)_{i+1}}^{∗} u. Assume that

t )_{β∪R(β)_{i+1}} v )_{β∪R(β)_{i+1}}^{∗} u .

By induction hypothesis, there are v′ and u′ such that v )_{β}^{∗} v′ )_{R_{i+1}}^{∗} u′ (_{β}^{∗} u. and there are two cases. If t )_{β} v, then we are done since t )_{β}^{∗} v′.

Otherwise, we have t )_{R(β)_{i+1}} u. From (i), there are t′ and v′′ such that

t )_{β}^{∗} t′ )_{R_{i+1}}^{∗} v′′ (_{β}^{∗} v .

Now, by confluence of )_{β}, there is v′′′ such that v′′ )_{β}^{∗} v′′′ (_{β}^{∗} v′. Commutation of )_{β} and )_{R_{i+1}} (Lemma 4.5) applied to v′′′ (_{β}^{∗} v′ )_{R_{i+1}}^{∗} u′ gives us a term u′′ such that v′′′ )_{R_{i+1}}^{∗} u′′ (_{β}^{∗} u′. We thus have t′ )_{β∪R_{i+1}}^{∗} u′′ and by Lemma 5.7 there are t′′ and u′′′ such that t′′ )_{β}^{∗})_{R_{i+1}}^{∗} (_{β}^{∗} u′′′. Therefore, t )_{β}^{∗})_{R_{i+1}}^{∗} (_{β}^{∗} u.

In diagrammatic form,

\xymatrix{ &  & t \ar[rr]^{R(β)_{i+1}} \ar@{.>}[dl]_{β}^{∗} &  & v \ar[rr]^{β∪R(β)_{i+1}}_{∗} \ar@{.>}[dl]^{β}_{∗} \ar@{.>}[dr]_{β}^{∗} &  & u \ar@{.>}[dr]^{β}_{∗} \\  & t′ \ar@{.>}[rr]_{R_{i+1}} \ar@{.>}[dl]_{β}^{∗} &  & v′′ \ar@{.>}[dr]^{β}_{∗} &  & v′ \ar@{.>}[rr]_{R_{i+1}}^{∗} \ar@{.>}[dl]_{β}^{∗} &  & u′ \ar@{.>}[dl]^{β}_{∗} \\ t′′ \ar@{.>}[drrrrr]_{R_{i+1}}^{∗} &  &  &  & v′′′ \ar@{.>}[rr]^{R_{i+1}}_{∗} &  & u′′ \ar@{.>}[dl]^{β}_{∗} \\  &  &  &  &  & u′′′}

We easily deduce (6) from (14). We get the confluence of )_{β∪R} using Theorem 4.6. By Proposition 5.1, the confluence of )_{β∪R(β)} follows from the confluence of )_{R} on conditionally (R, a)-stable sets of terms.

Theorem 5.10 Let R be a semi-closed left-linear algebraic system which respects a : Σ ) ℕ. Then, on any conditionally (R, a)-stable set of terms, if )_{R} is confluent then so is )_{β∪R(β)} .

Proof. Since R is semi-closed, left-linear and right-applicative, confluence of )_{β∪R} follows from confluence of )_{R} by Theorem 4.6. We then conclude by Lemma 5.9 and Proposition 5.1, since conditionally (R, a)-stable sets of terms are closed under )_{β∪R(β)} .

5.2 Confluence on weakly beta-normalizing terms

In this section, we extend to )_{R(β)} the results of Section 4.2. The main point is to obtain the lemma corresponding to Lemma 4.14. Moreover, as in Section 5.1, for all i ∈ ℕ we project )_{R(β)_{i}} on )_{R_{i}}. We thus want to obtain the following property, which implies (6):

\xymatrix{t \ar[r]^{β∪R(β)_{i}}_{∗} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ βnf(t) \ar@{.>}[r]_{R_{i}}^{∗} & βnf(u)}  (16)

We use the same tools as in Section 4.2. We consider weakly β-normalizing terms whose βnormal form respects the arity specified by rewrite rules, and we reason by induction on ≻. We also assume that rewrite rules are algebraic.

We denote by ⊳_{R(β)} the nested parallelization of join β-conditional rewriting, defined similarly as in Definition 4.11. It satisfies Proposition 4.12 and Lemma 4.13.

We now show (16) using exactly the same method as for showing (4) in Lemma 4.14.

Lemma 5.11 Let a : Σ ) ℕ be an arity and R be an algebraic conditional rewrite system which respects a. For all i ∈ ℕ, if t ∈ AN_{a} and t )_{β∪R(β)_{i}}^{∗} u, then u ∈ AN_{a} and βnf(t) )_{R_{i}}^{∗} βnf(u).

Proof. We reason exactly as in the proof of Lemma 4.14. We prove the property by induction on i ∈ ℕ. In the induction case we show that for all t ∈ AN_{a},

\xymatrix{t \ar[r]^{⊳_{R(β)_{i+1}}} \ar@{.>}[d]_{β}^{∗} & u \ar@{.>}[d]^{β}_{∗} \\ βnf(t) \ar@{.>}[r]_{⊳_{R_{i+1}}} & βnf(u)}  (17)

We reason by induction on ≻ using Lemma 2.3. The only difference with the proof of Lemma 4.14 is the case where t = λx⃗.ft_{1} …t_{n} and there is a rule d⃗ = c⃗ ⊃ l ) r such that t = λx⃗.lσa⃗ and u = λx⃗.rθb⃗ with lσ ⊳_{R(β)_{i+1}} rθ and d⃗σ ]_{β∪R(β)_{i}} c⃗σ. Exactly for the same reasons as in Lemma 4.14, we have a⃗ = b⃗ = ∅, t = λx⃗.lσ and u = λx⃗.rσ. Moreover, βnf(t) = λx⃗.lσ′ and βnf(u) = λx⃗.rθ′ with σ′ =_{def} βnf(σ) and θ′ = βnf(θ), and by induction hypothesis on ≻ we have σ′ ⊳_{R_{i+1}} θ′. It remains to show that lσ′ ⊳_{R_{i+1}} rθ′. Because σ′ ⊳_{R_{i+1}} θ′, it suffices to prove that lσ′ )_{R_{i+1}} rσ′. Thus, we are done if we show that d⃗σ′ ]_{R_{i}} c⃗σ′. Since d⃗ and c⃗ are algebraic, βnf(d⃗σ) = d⃗σ′ and βnf(c⃗σ) = c⃗σ′. Now, since d⃗ is algebraic and respects a, and since σ′ respects a, it follows that d⃗σ′ respects a. The same holds for c⃗σ′. Hence we conclude by applying on d⃗σ ]_{β∪R(β)_{i}} c⃗σ the induction hypothesis on i.

We deduce the preservation of confluence.

Theorem 5.12 Let a : Σ ) ℕ be an arity and R be an algebraic conditional rewrite system which respects a. If )_{R} is confluent on AN_{a}, then )_{β∪R(β)} is confluent on AN_{a}.

Proof. We can reason as described at the beginning of this section, using Proposition 5.1, Theorem 4.15 and Lemma 5.11. A direct proof is also possible, reasoning as for Theorem 4.15.

6 Orthonormal systems

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

This criterion comes from peculiarities of orthogonality with conditional rewriting. As remarked in Section 3.2, a conditional critical pair can be feasible or not. In [Ohl02], it is remarked that results on the confluence of semi-equational and normal orthogonal conditional systems could 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. An example of such situation is the following rewrite system.

Example 6.1 Consider the following two rules, taken from the system presented in Section 2.4.2:

> (length l) x = false ⊃ occ (cons x o) (node y l) )  false
> (length l) x = true ⊃ occ (cons x o) (node y l) )  occ o (get l x)

The only conditional critical pair between them is

> (length l) x = true ∧ > (length l) x = false ⊃ (false , occ o (get l x))

The condition of this pair cannot be satisfied by a confluent relation. Hence, if )_{β∪R(β)_{i}} is confluent then we can reason as in Lemma 4.5 and obtain the confluence )_{β∪R(β)_{i+1}} .

In this section, we define a class of systems, called orthonormal, that allows to generalize this reasoning. As in Example 6.1, confluence can be shown stratified way: the confluence of )_{β∪R(β)_{i}} implies the unfeasibility of critical pairs w.r.t. )_{β∪R(β)_{i}} , which in turn entails the confluence of the next stratum )_{β∪R(β)_{i+1}} . We thus obtain the level confluence of )_{β∪R(β)} .

Rules of orthonormal systems can have λ-terms in their right-hand sides and conditions. Moreover, no arity assumption is made. Hence, orthonormality ensures the confluence of βconditional rewriting combined to β-reduction when we cannot deduce it from the confluence of conditional rewriting (see Section 5).

Systems similar to orthonormal systems have already been studied in the first-order case [GM88, KW97]. It is worth relating orthonormal systems with approaches to conditional rewriting in which conditions are arbitrary predicates on terms. For first-order conditional rewriting this approach has been taken in [BK86]. It has been applied to λ-calculus [Tak93], and this is the way conditional rewrite rules are handled in the very expressive framework of CCERSs [GKK05]. Neither of these approaches can directly handle Example 6.1. In each case, confluence is proved under the assumption that the predicates used in conditions are stable by reduction, while proving this property in the case of Example 6.1 requires confluence.

A symbol f ∈ Σ is defined if it is the head of the left-hand side of a rule.

Definition 6.2 (Orthonormal Systems) A conditional rewrite system R is orthonormal if

(i) it is left-linear;

(ii) in every rule d⃗ = c⃗ ⊃ l )_{R} r, the terms in c⃗ are closed β-normal forms not containing defined symbols;

(iii) for every critical pair

d_{1} = c_{1} ∧ … ∧ d_{n} = c_{n} ⊃ (s, t)

there exist distinct i, j ∈ {1, …, n} such that d_{i} = d_{j} and c_{i} ≠ c_{j}.

Condition (ii) is a simple syntactic and decidable way to ensure that orthonormal systems are normal (recall from Remark 2.12 that normality is in general undecidable). As explained in Example 6.1, assuming the confluence of )_{β∪R(β)_{i}} , condition (iii) implies the unfeasibility of critical pairs w.r.t. )_{β∪R(β)_{i}} , hence the confluence of the next stratum )_{β∪R(β)_{i+1}} . This entails the level confluence of )_{β∪R(β)} . We actually prove in Theorem 6.7 the shallow confluence of )_{β∪R(β)} , which is a stronger property (see Definition 2.15). Theorem 6.7 is thus an extension of the shallow confluence of orthogonal first-order normal conditional rewriting (Theorem 3.12) to orthonormal β-conditional rewriting.

The most important point w.r.t. the results of Section 5 is that orthonormal systems do not need to respect an arity nor to be algebraic.

Example 6.3 The system presented in Section 2.4.2 is orthonormal.

We now show that )_{β∪R(β)} is shallow confluent when R is orthonormal. This result is stated and proved in Theorem 6.7 below. We use some intermediate lemmas. The parallel moves property occupies Lemmas 6.5 and 6.6. We begin by showing that the confluence of )_{β∪R(β)_{i}} implies the commutation of )_{β}^{∗} and )_{R(β)_{i+1}}^{∗} .

Lemma 6.4 Let R be an orthonormal system. For all i ∈ ℕ, if )_{β∪R(β)_{i}} is confluent then )_{R(β)_{i+1}} commutes with )_{β} :

\xymatrix{· \ar[r]^{R(β)_{i+1}}_{∗} \ar[d]_{β}^{∗} & · \ar@{.>}[d]^{β}_{∗} \\ · \ar@{.>}[r]_{R(β)_{i+1}}^{∗} & ·}

Proof. We reason as in Lemma 4.5. We show property (18) below and then deduce the commutation of )_{R(β)_{i+1}} and )_{β} using Lemma 2.18 and the fact that )_{β}^{∗} = ⊳_{β}^{∗}.

\xymatrix{t \ar[r]^{R(β)_{i+1}} \ar[d]_{⊳_{β}} & v \ar@{.>}[d]^{⊳_{β}} \\ u \ar@{.>}[r]_{R(β)_{i+1}}^{∗} & w}  (18)

The only difference with the proof of Lemma 4.5 is when t )_{R(β)_{i+1}} v by contracting a rooted redex. In this case, there is a rule d⃗ = c⃗ ⊃ l )_{R} r and a substitution σ such that t = lσ and v = rσ. We show that there is a term w such that u )_{R(β)_{i+1}}^{∗} w ⊲_{β} rσ. As l is a non-variable linear algebraic term, there is a substitution σ′ such that σ⊳_{β} σ′ and lσ⊳_{β} lσ′ = u. Therefore we have rσ⊳_{β} rσ′. It remains to show that lσ′ )_{R(β)_{i+1}} rσ′. Recall that d⃗σ )_{β∪R(β)_{i}}^{∗} c⃗. By assumption (confluence of )_{β∪R(β)_{i}} ), since d⃗σ )_{β}^{∗} d⃗σ′ there are v⃗ such that d⃗σ′ )_{β∪R(β)_{i}}^{∗} v⃗ (_{β∪R(β)_{i}}^{∗} c⃗. But c⃗ are β ∪ R(β)-normal forms, hence v⃗ = c⃗. We conclude that lσ′ )_{R(β)_{i+1}} rσ′ ⊲_{β} rσ.

We follow the usual scheme of proofs of confluence of orthogonal conditional rewrite systems [Ohl02]. For all i ∈ ℕ, we denote by )_{∥R(β)_{i}} the smallest parallel rewrite relation containing )_{R(β)_{i}} (see Definition 2.5). Hence, )_{∥R(β)_{i}} is strictly included in the nested parallel relation ⊳_{R(β)_{i}} used in Section 5.2 (Definition 4.11). The main property is the commutation of )_{∥R(β)_{i}} and )_{∥R(β)_{j}} for all i, j ∈ ℕ, which corresponds to the usual parallel moves property. Let <_{mul} be the multiset extension of the usual ordering on naturals numbers. In our case, the parallel moves property is:

Parallel Moves. Given i, j ∈ ℕ, if )_{β∪R(β)_{n}} commutes with )_{β∪R(β)_{m}} for all n, m such that {n, m} <_{mul} {i, j}, then )_{∥R(β)_{i}} commutes with )_{∥R(β)_{j}} .

The proof is decomposed into Lemma 6.5 and Lemma 6.6. In Lemma 6.5, assuming the commutation of )_{β∪R(β)_{n}} and )_{β∪R(β)_{m}} for all n, m such that {n, m} <_{mul} {i, j}, we consider, for the commutation of )_{∥R(β)_{i}} and )_{∥R(β)_{j}} , the particular case of a rooted R(β)_{i}-reduction.

Lemma 6.5 Let R be an orthonormal system and i, j ≥ 0. Assume that )_{β∪R(β)_{n}} commutes with )_{β∪R(β)_{m}} for all n, m such that {n, m} <_{mul} {i, j}. Then for all rules d⃗ = c⃗ ⊃ l )_{R} r, we have

\xymatrix{lσ \ar[r]^{R(β)_{i}} \ar[d]_{∥R(β)_{j}} & rσ \ar@{.>}[d]^{∥R(β)_{j}} \\ u \ar@{.>}[r]_{R(β)_{i}}^{=} & v}

Proof. The result holds if i = 0 since )_{R(β)_{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σ )_{∥R(β)_{j}} u. Therefore, for all k, 1 ≤ k ≤ n, there exists a rule ρ_{k} : d⃗_{k} = c⃗_{k} ⊃ l_{k} )_{R} 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} form 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} (_{β∪R(β)_{h}}^{∗} d′_{m}σ = d′_{p}σ )_{β∪R(β)_{h}}^{∗} c′_{p} .

But {h, h} <_{mul} {i, j} and by assumption )_{β∪R(β)_{h}} is confluent. Therefore we must have c′_{m} ]_{β∪R(β)_{h}} c′_{p}. But it is not possible since c′_{m} and c′_{p} are distinct normal forms. Hence, conditions of ρ and ρ_{k} cannot be both satisfied by σ and )_{β∪R(β)_{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σ )_{∥R(β)_{j}} lσ′ and by linearity of l, u = lσ′. Furthermore, rσ )_{∥R(β)_{j}} rσ′. We now show that lσ′ )_{R(β)_{i}} rσ′. We have d⃗σ )_{β∪R(β)_{i−1}}^{∗} c⃗ and d⃗σ )_{R(β)_{j}}^{∗} d⃗σ′. As i, j > 0, we have {i − 1, j} <_{mul} {i, j}. Therefore, by assumption )_{β∪R(β)_{i−1}} and )_{β∪R(β)_{j}} commute and there exist terms c⃗′ such that

d⃗σ′ )_{β∪R(β)_{i−1}}^{∗}  c⃗′ (_{β∪R(β)_{j−1}}^{∗}  c⃗ .

As terms c⃗ are )_{β∪R(β)} -normal forms, we have c⃗′ = c⃗ and it follows that lσ′ )_{R(β)_{i}} rσ′.

Now, in Lemma 6.6 we show that the commutation of )_{∥R(β)_{i}} and )_{∥R(β)_{j}} is ensured by the two particular cases of rooted R(β)_{i}-reduction and R(β)_{j}-reduction.

Lemma 6.6 Let R be an orthonormal system and i, j ≥ 0. Property (i) below holds if and only if for all rules d⃗ = c⃗ ⊃ l )_{R} r, properties (ii) and (iii) hold.

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

Proof. The “only if” statement is trivial. For the “if” case, let s, t, u be three terms such that u (_{∥R(β)_{j}} s )_{∥R(β)_{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 properties (ii) and (iii). Now assume that both reductions are nested. In this case s cannot be a symbol f ∈ Σ nor a variable. 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} (_{∥R(β)_{j}} s_{k} )_{∥R(β)_{i}} t_{k}. In this case also we conclude by induction hypothesis.

Now, an induction on <_{mul} provides the commutation of )_{β∪R(β)_{i}} and )_{β∪R(β)_{j}} for all i, j ≥ 0, i.e. the shallow confluence of )_{β∪R(β)} .

Theorem 6.7 If R is an orthonormal system, then )_{β∪R(β)} is shallow confluent.

Proof. We reason by induction on unordered pairs {i, j} seen as multisets and compared with the well-founded relation <_{mul}. We show the commutation of )_{β∪R(β)_{i}} and )_{β∪R(β)_{j}} for all i, j ≥ 0. The least unordered pair {i, j} (considered as a multiset) with respect to <_{mul} is {0, 0}. As )_{β∪R(β)_{0}} =)_{β} by definition, this case holds by confluence of β.

Now, assume that i > 0 and that the commutation of )_{β∪R(β)_{n}} and )_{β∪R(β)_{m}} holds for all n, m with {n, m} <_{mul} {i, 0}. As {i − 1, i − 1} <_{mul} {i, 0}, )_{β∪R(β)_{i−1}} is confluent and the commutation of )_{β∪R(β)_{i}} with )_{β∪R(β)_{0}} (=)_{β}) follows from Lemma 6.4.

The remaining case is when i, j > 0. Using the induction hypothesis, from Lemma 6.5 and Lemma 6.6, we obtain the commutation of )_{∥R(β)_{i}} and )_{∥R(β)_{j}} , which in turn implies the commutation of )_{R(β)_{i}}^{∗} and )_{R(β)_{j}}^{∗} . Now, as {i − 1, i − 1} <_{mul} {i, j}, by Lemma 6.4, )_{β} and )_{R(β)_{i}} commute. This way, we also obtain the commutation of )_{β} and )_{R(β)_{j}} . Then, the commutation of )_{β∪R(β)_{i}}^{∗} and )_{β∪R(β)_{j}}^{∗} easily follows.

Example 6.8 The relation )_{β∪R(β)} induced by the system presented in Section 2.4.2 is shallow confluent and thus confluent.

7 Conclusion

Our results are summarized in Figure 1 page 6.

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 Section 4 and 5 for the join conditional rewrite systems extend to the case of oriented systems (hence to normal systems) and to the case of level-confluent semi-equational systems. For semiequational systems, the proofs follow the same scheme, provided that level-confluence of )_{R} 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 left-linear conditional rewriting. The semi-closure condition is sufficient to avoid this, and it seems to provide the counterpart of left-linearity for unconditional rewriting. 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 join systems behave like normal systems. But normal systems can be easily translated into equivalent non-conditional systems. Moreover such a translation preserves good properties such as left-linearity and non ambiguity. As many practical uses of rewriting rely on terminating systems, semi-closed join systems may be in practice essentially an intuitive way to design rewrite systems that can be then efficiently implemented by non-conditional rewriting.

A wider interesting perspective would be to extend the results to CCERSs [GKK05].

References

[ALS94] J. Avenhaus et C. Loría-Sáenz – “Higher Order Conditional Rewriting and Narrowing”, Proceedings of the 1st International Conference on Constraints in Computational Logics, LNCS, vol. 845, Springer Verlag, 1994, p. 269–284. 3

[Bar84] H.P. Barendregt – The Lambda-Calculus, its Syntax and Semantics, Studies in Logic and the Foundation of Mathematics, North Holland, 1984, Second edition. 3, 5, 15, 19, 23

[BCKL03] G. Barthe, H. Cirstea, C. Kirchner et L. Liquori – “Pure Patterns Type Systems”, Principles of Programming Languages, New Orleans, USA, ACM, 2003. 3

[BFG97] F. Barbanera, M. Fernández et H. Geuvers – “Modularity of Strong Normalization and Confluence in the Algebraic-lambda-Cube”, Journal of Functional Programming 7 (1997), no. 6, p. 613–660. 24

[BK86] J.A. Bergstra et J.W. Klop – “Conditional rewrite rules: Confluence and termination”, Journal of Computer and System Sciences 32 (1986), no. 3, p. 323–362. 11, 18, 37

[BKR06] F. Blanqui, C. Kirchner et C. Riba – “On the Confluence of Lambda-Calculus with Conditional Rewriting”, Proceedings of FoSSaCS’06, LNCS, vol. 3921, 2006. 5, 28

[Bla05] F. Blanqui – “Definitions by Rewriting in the Calculus of Constructions”, Mathematical Structures in Computer Science 15 (2005), no. 1, p. 37–92. 3

[BT88] V. Breazu-Tannen – “Combining Algebra and Higher-Order Types”, Proceedings of LiCS’88, IEEE Computer Society, 1988. 3, 16

[BTG89] V. Breazu-Tannen et J. Gallier – “Polymorphic Rewriting Conserves Algebraic Strong-Normalization and Confluence”, Proceedings of ICALP’89, 1989. 16

[BTG94] — , “Polymorphic Rewriting Conserves Algebraic Confluence”, Information and Computation 114 (1994), no. 1, p. 1–29. 3, 16

[BTM87] V. Breazu-Tannen et A. Meyer – “Computable Values Can Be Classical”, Proceedings of POPL’87, ACM, 1987. 15

[Böh68] C. Böhm – “Alcune Proprietà delle Forme β-η-Normali nel λ-K-Calcolo”, Tech. Report 696, Pubblicazioni dell’ Istituto per le Applicazioni del Calcolo, ROMA, 1968. 8

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

[DHK03] G. Dowek, T. Hardin et C. Kirchner – “Theorem Proving Modulo”, Journal of Automated Reasoning 31 (2003), no. 1, p. 33–72. 3

[DJ90] N. Dershowitz et J.-P. Jouannaud – “Rewrite Systems”, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (J. van Leeuwen, éd.), North-Holland, 1990, p. 243–320. 3 [DO90] N. Dershowitz et M. Okada – “A rationale for conditional equational program-

ming”, Theoretical Computer Science 75 (1990), p. 111–138. 5

[Dou92] D.J. Dougherty – “Adding Algebraic Rewriting to the Untyped Lambda Calculus”, Information and Computation 101 (1992), no. 2, p. 251–267. 3, 4, 15, 16, 17, 18, 22, 23

[GKK05] J. Glauert, D. Kesner et Z. Khasidashvili – “Expression Reduction Systems and Extensions: An Overview”, Processes, Terms and Cycles: Steps to the Road of Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion os His 60th Birthday, LNCS, vol. 3838, Springer, 2005, p. 496–553. 3, 37, 40

[GM88] E. Giovannetti et C. Moiso – “Notes on the Elimination of Conditions”, Proceedings of CTRS’87, LNCS, vol. 308, Springer, 1988, p. 91–97. 37

[Gra96] B. Gramlich – “On Termination and Confluence Properties of Disjoint and Constructor-Sharing Conditional Rewrite Systems”, Theoretical Computer Science 165 (1996), no. 1, p. 97–131. 4

[Hue80] G. Huet – “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems”, Journal of the Association for Computing Machinery 27 (1980), no. 4, p. 797–821. 15, 17

[Hue86] — , “Formal Structures for Computation and Deduction”, Technical report, INRIA, Rocquencourt, 1986. 4, 12

[JO91] J.-P. Jouannaud et M. Okada – “Executable Higher-Order Algebraic Specification Languages”, Proceedings of LiCS’91, IEEE Computer Society, 1991. 3

[Kap84] S. Kaplan – “Conditional Rewrite Rules”, Theoretical Computer Science 33 (1984), p. 175–193. 11

[Klo80] J.W. Klop – Combinatory Reduction Systems, Mathematical Center Tracts, vol. 127, CWI, 1980, PhD Thesis. 12, 15

[KOR93] J.W. Klop, V. van Oostrom et F. van Raamsdonk – “Combinatory Reduction Systems: Introduction and Survey”, Theoretical Computer Science 121 (1993), p. 279–308. 3

[KW97] U. Kühler et C.-P. Wirth – “Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving”, Proceedings of RTA’97, LNCS, vol. 1232, Springer, 1997, p. 38–52. 37

[Mid91] A. Middeldorp – “Confluence of the Disjoint Union of Conditional Term Rewriting Systems”, Proceedings of CTRS’91, LNCS, vol. 516, 1991, p. 295–306. 4

[Mül92] F. Müller – “Confluence of the Lambda Calculus with Left Linear Algebraic Rewriting”, Information Processing Letters 41 (1992), p. 293–299. 3, 4, 12, 15, 16, 18, 19, 20, 22

[Nip91] T. Nipkow – “Higher-Order Critical Pairs”, Proceedings of LiCS’91, IEEE Computer Society, 1991. 3 [Ohl02] E. Ohlebusch – Advanced Topics in Term Rewriting, Springer, April 2002. 5, 11,

18, 36, 38

[Oka89] M. Okada – “Strong Normalizability for the Combined System of the Typed Lambda-Calculus and an Arbitrary Convergent Term Rewrite System”, Proceedings of ISSAC’89, ACM, 1989, p. 357–363. 16

[OR94] V. van Oostrom et F. van Raamsdonk – “Weak Orthogonality Implies Confluence: the Higher-Order Case”, Proceedings of LFCS’94, LNCS, vol. 813, 1994. 3, 16, 20, 23, 27

[Par89] M. Parigot – “On the Representation of Data in Lambda-Calculus”, Proceedings of CSL’89, LNCS, vol. 440, 1989, p. 309–321. 8

[Sco75] D. Scott – “Lambda Calculus and Recursion Theory”, Proc. of the third Scandinavian Logic Symposium (S. Kanger, éd.), North Holland, 1975, p. 154–193. 12

[Tak93] M. Takahashi – “Lambda-Calculi with Conditional Rules”, Proceedings of TLCA’93, LNCS, Springer-Verlag, 1993, p. 406–417. 3, 37

[Tak95] — , “Parallel Reductions in λ-Calculus”, Information and Computation 118 (1995), p. 120–127. 19, 29

[Toy87] Y. Toyama – “On the Church-Rosser Property for the Direct Sum of Term Rewriting Systems”, Journal of the Association for Computing Machinery 34 (1987), no. 1, p. 128–143. 3

[Vri89] R.C. de Vrijer – “Extending the Lambda Calculus with Surjective Pairing is Conservative”, Proceedings of LiCS’89, IEEE Computer Society, 1989, p. 204–215. 4, 12

[Wad71] C.P. Wadsworth – “Semantics and Pragmatics of the Lambda-Calculus”, Thèse, Oxford University, 1971. 7

[Wol93] D.A. Wolfram – The Clausal Theory of Types, Cambridge Tracts in Theoretical Computer Science, vol. 21, Cambridge University Press, 1993. 3