9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # On the confluence of λ-calculus with conditional rewriting

On the con?uence of λ-calculus with conditional rewriting

Fr?d?ric Blanqui1 , Claude Kirchner1, and Colin Riba2 e e

arXiv:cs/0609002v2 [cs.LO] 11 Sep 2006

1 2

INRIA & LORIA? INPL & LORIA

Abstract. The con?uence of untyped λ-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the con?uence 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 u rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty’s result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of con?uence is di?cult to achieve. Second, we go beyond the algebraic framework and get new con?uence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.

1

Introduction

Rewriting [10] and λ-calculus [3] are two universal computation models which are both used, with their own advantages, in programming language design and implementation, as well as for the foundation of logical frameworks and proof assistants. Among other things, λ-calculus allows to manipulate abstractions and higher-order variables, while rewriting is traditionally well suited for de?ning 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 ?rstorder rewriting with higher-order capabilities, by adding to λ-calculus algebraic features or, more recently, by a uniform integration of both paradigms. In the ?rst case, we ?nd the works on combinatory reduction systems [17] and other higher-order rewriting systems [20] each of them subsumed by van Oostrom and van Raamsdonk’s axiomatization of HORS [23]. The second case concerns the more atomic combination of λ-calculus with term rewriting [15, 5] and the last category the rewriting calculus [9, 4].

?

UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP, Campus Scienti?que, BP 239, 54506 Vandoeuvre-l`s-Nancy Cedex, France e

Despite this strong interest in the combination of both concepts, few works have considered conditional higher-order rewriting in λ-calculus. This is of particular interest for both computation and deduction. Indeed, conditional rewriting appears to be very convenient when programming with rewrite rules and its combination with higher-order features provides a quite agile background for the combination of algebraic and functional programming. This is also of main use in proof assistants based on the de Bruijn-Curry-Howard isomorphism where, as emphasized in deduction modulo [13, 5], rewriting capabilities for de?ning functions and proving equalities automatically is clearly of great interest when making large proof developments. Furthermore, while many con?uence proofs often rely on termination and local con?uence, in some cases, con?uence may be necessary for proving termination (e.g. with type-level rewriting or strong elimination [5]). It is therefore of crucial interest to have also criteria for the preservation of con?uence 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 con?uence when combining typed λcalculus and ?rst-order rewriting concerns the simple type discipline [7] and the result has been extended to polymorphic λ-calculus in [8]. Concerning untyped λ-calculus, the result was shown in [19] for left-linear rewriting. It is extended as a modularity result for higher order rewriting in [23]. In [12], it is shown that left-linearity is not necessary provided that terms considered are strongly βnormalizable and are well-formed with respect to the declared arity of symbols, a property that we call here arity-compliance. Higher-order conditional rewriting is studied in [1] and the con?uence result relies on joinability of critical pairs, hence on termination of the combined rewrite relation. Another form of higherorder conditional rewriting is considered in [22]. It concerns con?uence results for a very general form of orthogonal systems. These systems are related to those presented in Sect. 5. If modularity properties have been investigated in the pure ?rst-order conditional case (e.g. [18, 14]), to the best of our knowledge, there was up to now no result on preservation of con?uence when β-reduction is added to conditional rewriting. In this paper, we study the con?uence property of the combination of βreduction with a con?uent conditional rewrite system. This of course should rely on a clear understanding of the conditional rewrite relation under use and, as usual, the ways the matching is performed and instantiated conditions are decided are crucial. So, we start from λ-terms with curried constants and among them we distinguish applicative terms that contain no abstraction and algebraic terms that furthermore have no active variables, i.e. variables occurring in the left-hand side of an application. In this paper, we always consider algebraic left-hand sides. So, rewriting does not use higher-order pattern-matching but just syntactic matching. Furthermore, we consider two rewrite relations induced by a set of conditional rules. →A is the conditional rewrite relation where the conditions are checked without considering β-reduction and →B is the conditional rewrite

relation where β-reduction is allowed when evaluating the conditions. Then, we study the con?uence of the relations →β∪A and →β∪B , the respective combinations of →A and →B with β-reduction. This is made precise in Sect. 2 and accompanied of relevant examples. We know that adding β-reduction to a con?uent non left-linear algebraic rewriting system results in a non con?uent relation. Of course, with conditional rewriting, non-linearity can be simulated by linear systems. Extending the result of M¨ ller [19], we prove in Sect. 3 that con?uence of →β∪A follows from u con?uence of →A when conditional rules are applicative, left-linear and do not allow their condition to test for equality of open terms. Such rules are called semi-closed. We also adapt to conditional rewriting the method of Dougherty [12] and extend it to show that for a large set of weakly β-normalizing terms, the left-linearity and semi-closed hypotheses can be dropped provided the rules are algebraic and terms are arity-compliant. We then turn in Sect. 4 to the con?uence modularity of →β∪B for rules with algebraic right-hand side. In this case, we show that arity-compliance is a su?cient condition to deduce con?uence of →β∪B from con?uence of →β∪A (hence of →A ). This is done ?rst for left-linear semi-closed systems, a restriction that we also show to be super?uous when considering only weakly β-normalizing terms. The case of non-algebraic rules is handled in Sect. 5. Such rules can contain active variables and abstractions in right-hand sides or in conditions (but still not in left-hand sides). In this case, the con?uence of →β∪B no more follows from the con?uence of →A nor of →β∪A . We show that the con?uence of →β∪B holds under a syntactic condition, called orthonormality ensuring that if two rules overlap at a non-variable position, then their conditions cannot be both satis?ed. An orthonormal system is therefore orthogonal, and the con?uence of →B∪β follows using usual proof methods. We assume some familiarity with λ-calculus [3] and conditional rewriting [11, 21] but we recall the main notations in the next section. By lack of place, the main proofs are only sketched here. They are detailed in [6].

2

General de?nitions

This section introduces the main notions of the paper. We use λ-terms with curried constants. De?nition 1 (Terms). We assume given a set F of function symbols and an in?nite set X of variables. The set T of terms is inductively de?ned as follows: t, u ∈ T ::= f ∈ F | x ∈ X | tu | λx.t A term is applicative if it contains no abstraction and algebraic (“not variableapplying” in [19]) if it furthermore contains no subterm of the form xt with x ∈ X . We use t to denote a sequence of terms t1 , . . . , tn of length |t| = n.

As usual, terms are considered modulo α-conversion. Let FV(t) be the set of variables free in t. We denote by tσ the capture-avoiding application of the substitution σ to the term t. By {x → t}, we denote the substitution σ such that xi σ = ti . As usual, positions in a term are strings over {1, 2}. The subterm of t at position p is denoted by t|p . If t is applicative, the replacement of t|p by some term u is denoted by t[u]p . A context is a term with exactly one free occurrence of a distinguished variable []. If C is an applicative context then C[t] stands for C[t]p , where p is the position of [] in C. A rewrite relation is a binary relation on terms → which is closed by term formation rules : if s → t then λx.s → λx.t, su → tu and us → ut ; and by substitution : s → t implies sσ → tσ. Its inverse is denoted by ←; its re?exive closure by →= ; its re?exive and transitive closure by →? ; and its re?exive, symmetric and transitive closure by ?? . The joinability relation is ↓ = →? ←? . The β-reduction relation is the smallest rewrite relation →β such that (λx.s)t →β s{x → t}. A term t →-rewrites (or →-reduces) to u if t →? u (we omit → when clear from the context). We write →R∪S for the union of the relations →R and →S . We call parallel rewrite relation any re?exive rewrite relation ? closed by parallel application : [s ? s′ & t ? t′ ] ? st ? s′ t′ . We now introduce conditional rewriting. Let us emphasize that we consider ?rst-order syntactical matching. De?nition 2 (Conditional rewriting). A conditional rewrite system R is a set of conditional rewrite rules3 : d1 = c1 ∧ · · · ∧ dn = cn ? l → r where l is a non-variable algebraic term, di , ci and r are arbitrary terms and FV(di , ci , r) ? FV(l). A system is right-applicative (resp. right-algebraic) if all its right-hand sides are applicative (resp. algebraic). A system is applicative (resp. algebraic) if all its rules are made of applicative (resp. algebraic) terms. The join rewrite relation induced by R is usually de?ned as →A = i≥0 →Ai [21] where →A0 = ? and for all i ≥ 0, →Ai+1 is the smallest rewrite relation such that for all rule d = c ? l → r ∈ R, for all substitution σ, if dσ ↓Ai cσ then lσ →Ai+1 rσ. This relation is sometimes called the standard conditional rewrite relation. We de?ne the β-standard rewrite relation induced by R as →B = i≥0 →Bi where →B0 = ? and for all i ≥ 0, →Bi+1 is the smallest rewrite relation such that for all rule d = c ? l → r ∈ R, for all σ, if dσ ↓Bi ∪β cσ then lσ →Bi+1 rσ. If →Ai is con?uent for all i ≥ 0, we say that →A is level con?uent. It is shallow con?uent when →? i and →? j commute for all i, j ≥ 0. A A Other forms of conditional rewriting appear in the literature [11]. Natural rewriting is obtained by taking ?? instead of ↓A in the evaluation of conditions. A Oriented rewriting is obtained by taking →? . A particular case of both standard A and oriented rewriting is normal rewriting, in which the terms c are closed and in →A -normal form.

3

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

Examples. We begin by some basic functions on lists. car (x :: l) → x car [ ] → err cdr (x :: l) → l cdr [ ] → err get l 0 → car l get l (s n) → get (cdr l) n

len [ ] → 0 len (x :: l) → s (len l)

?lter p [ ] →[] p x = tt ? ?lter p (x :: l) → x :: (?lter p l) p x = ? ? ?lter p (x :: l) → ?lter p l

De?ne > with > (s x) 0 → tt, > 0 y → ? and > (s x) (s y) → > x y. We can now de?ne app such that app f n l applies f to the nth element of l. It uses ap as an auxiliary function: > (len l) n = tt ? app f n l → ap f n l > (len l) n = ? ? app f n l → err ap f 0 l → f (car l) :: cdr l ap f (s n) l → car l :: ap f n (cdr l)

We represent ?rst-order terms as trees with nodes nd y l where y is intended to be a label and l the list of sons. Positions are lists of integers and occ u t tests if u is an occurrence of t. We de?ne it with occ [ ] t → tt and > (len l) x = ? ? occ (x :: o) (nd y l) → ? > (len l) x = tt ? occ (x :: o) (nd y l) → occ o (get l x) To ?nish, rep t o s replaces by s the subterm of t at occurrence o. Its rules are occ u t = tt ? rep t o s → re t o s and occ u t = ? ? rep t o s → err. The rules re s [ ] t → s and re (nd y l) (x :: o) s → nd y (app (λz.re z o s) x l) de?ne the function re. The system Tree that consists of rules de?ning car cdr, get, len and occ is algebraic. Rules of app and ap are right-applicatives and those for ?lter contain in their conditions the variable p in active position. This de?nition of re involves a λ-abstraction in a right hand side. In Sect. 5, we prove con?uence of the relation →β∪B induced by the whole system.

3

Con?uence of →β with conditional rewriting

In this section, we study the con?uence of →β∪A . The simplest result is the preservation of con?uence when R can not check arbitrary equalities (Sect. 3.1). In Sect. 3.2, we consider more general systems and prove that the con?uence of →β∪A follows from the con?uence of →A on terms having a β-normal form of a peculiar kind. In [19], M¨ ller shows that the union of β-reduction and the rewrite relation u →A induced by a left-linear non-conditional applicative system is con?uent as soon as →A is. This result is generalized as modularity result for higher-order rewriting in [23]. The importance of left-linearity is known since Klop [16]. We exemplify it with Breazu-Tannen’s counter-example [7]. The rules ? x x → 0 and

? (s x) x → s 0 are optimization rules for minus. Together with usual rules de?ning this function, they induce a con?uent rewrite relation. With the ?xpoint combinators of the λ-calculus, we can build a term Y →? s Y . This term makes β the application of the two rules above possible on β-reducts of ? Y Y , leading to an unjoinable peak : 0 ←A ? Y Y →? ? (s Y ) Y →A s 0. β With conditional rewriting, we do not need non-linear matching to distinguish ? (s x) x from ? x x, since this can be done within the conditions. The previous system can be encoded into a left-linear conditional system with the rules x = y ? ? x y → 0 and s x = y ? ? x y → s 0. Of course, the relation →A is still con?uent. However, the same unjoinable peak starting from ? Y Y makes fail the con?uence of →β∪A . There are two ways to overcome the problem: limiting the power of rewriting or limiting the power of β-reduction. The ?rst way is treated in Sect. 3.1, in which we limit the comparison power of conditional rewriting by restricting ourselves to left-linear and semi-closed systems. This can also be seen as a way, from the point of view of rewriting, to isolate the e?ect of ?xpoints: since two distinct occurrences of Y can not be compared, they can be unfolded independently from each other. Then, in Sect. 3.2, we limit the power of →β by restricting ourselves to sets of terms having a special kind of β-normal-form. This amounts to only consider terms in which ?xpoints do not have the ability to modify the result of →β∪A . In fact, it is su?cient that they do not modify the result of →β alone. More precisely, ?xpoints are allowed when they are eliminated by head β-reductions. 3.1 Con?uence of left-linear semi-closed systems

We now introduce semi-closed systems. De?nition 3 (Semi-closed systems). A system is semi-closed if in every rule d = c ? l → r, each ci is algebraic and closed. The system Tree of Sect. 2 is left-linear and semi-closed. Given a semi-closed left-linear system, we show that con?uence of →β∪A follows from con?uence of →A . This follows from a weak commutation of →A and Tait and Martin-L¨f o β-parallel reduction relation ?β , de?ned as the smallest parallel rewrite relation (Sect. 2) closed by the rule (beta) [3]: (beta) s ? β s ′ t ? β t′ (λx.s)t ?β s′ {x → t′ }

We will use some well known properties of ?β . If σ ?β σ ′ then sσ ?β sσ ′ ; this is the one-step reduction of parallel redexes. We can also simulate β-reduction: →β ? ?β ?→? . And third, ?β has the diamond property: ?β ?β ? ?β ?β . This β corresponds to the fact that any complete development of →β can be done in one ?β -step. M¨ ller [19] uses a weaker parallelization of →β : its relation is de?ned w.r.t. u the applicative structure of terms only and does not reduces in one step nested

β-redexes. Consequently, it does not enjoy the diamond property on which we rely in Sect. 4. Nested parallelizations (corresponding to complete developments) are already used in [23] for their con?uence proof of HORS. However, our method inherits more from [19] than [23], as we use complete developments of →β only, whereas complete developments of →β and of →A are used for the modularity result of [23]. Proposition 4. Let R be a semi-closed, left-linear and right-applicative system and assume that →? i?1 commutes with →? . For any rule d = c ? l → r ∈ R A β and substitution σ, if u ?β lσ →Ai rσ, then there exists σ ′ such that u = lσ ′ →Ai rσ ′ ?β rσ. Proof Sketch. Since l is algebraic and linear, there is a substitution σ ′ such that σ ?β σ ′ and u = lσ ′ . It follows that rσ ?β rσ ′ and it remains to show that dσ ′ ↓Ai?1 cσ ′ . Since lσ →Ai rσ, there is v such that dσ →? i?1 v ←? i?1 cσ. A A Thus, dσ ?? dσ ′ and, by assumption, there is v ′ such that dσ ′ →? i?1 v ′ ?? v. A β β Since c is algebraic and closed, we have cσ = c and v in β-normal form. Hence, v ′ = v and dσ ′ ↓Ai?1 c. Lemma 5 (Commutation of →A and ?β ). If R is a semi-closed left-linear right-applicative system, then ?? →? ? →? ?? . A A β β Proof Sketch. The result follows from the commutation of →? i and ?? for A β all i ≥ 0. The case i = 0 is trivial. For i > 0, there are three steps. First, we show by induction on the de?nition of the parallel rewrite relation ?β that if u ?β s →Ai t then there exists v such that u →? i v ?β t. If u is s this is obvious. A If s is an abstraction, the result follows from induction hypothesis (IH) and the context closure of →Ai (CC). If s = s1 s2 , there are two cases: if t = t1 t2 with sk →=i tk then we conclude by (IH) and (CC). Otherwise, we use Prop. 4. A Second, use induction on the number of Ai -steps to show that ?β →? i ? A →? i ?β . Finally, to conclude that ?? →? i ? →? i ?? , use an induction on the A A A β β number of ?β -steps. A direct application of Hindley-Rosen’s Lemma o?ers then the preservation of con?uence. Theorem 6 (Con?uence of →β∪A ). Let R be a semi-closed left-linear rightapplicative system. If →A is con?uent then so is →β∪A . For the system Tree of Sect. 2, the relation →A is con?uent. As the rules are left-linear and semi-closed, Theorem 6 applies and →β∪A is con?uent. 3.2 Con?uence on weakly β-normalizing terms

We now turn to the problem of dropping the left-linearity and semi-closure conditions. As seen above, ?xpoint combinators make the commutation of →? and →? β A fail when rewriting involves equality tests between open terms. When using

weakly β-normalizing terms, we can project rewriting on β-normal forms (βnf ), thus eliminating ?xpoints as soon as they are not signi?cant for the reduction. Hence, we seek to obtain βnf (s) →? βnf (t) whenever s →? A β∪A t. This requires three important properties. First, β-normal forms should be stable by rewriting. Hence, we assume that right-hand sides are algebraic. Moreover, we re-introduce some information from the algebraic framework, giving maximal arities to function symbols in F . Second, we need normalizing β-derivations to commute with rewriting. This follows from using the leftmost-outermost strategy of λ-calculus [3]. Finally, we need rule conditions to be algebraic. Indeed, consider the rule x b = y ? f x y → a that contains an non-algebraic condition. The relation →A ? is con?uent but a ←? β∪A f (λx.x) ((λz.z)(λx.x) b) →β f (λx.x) b is an unjoinable critical peak. De?nition 7 (Arity-compliance). We assume that every symbol f ∈ F is equipped with an arity αf ≥ 0. A term is arity-compliant if it contains no subterm of the form f t with f ∈ F and |t| > αf . A rule d = c ? l → r is almost arity-compliant if l and r are arity-compliant and l is of the form f l with |l| = αf . A rule is arity-compliant if, furthermore, d and c are arity-compliant. Let U be the set of terms having an arity-compliant β-normal form. Remark that a higher-order rule (with active variables and abstractions) can be arity-compliant. Arity-compliance is useful because it prevents collapsing rules from creating β-redexes. For example, the rule id x → x forces the arity of id to be 1. Hence the term id (λx.x) y is not arity-compliant. Moreover it is a β-normal form that →A -reduces to the β-redex (λx.x)y. It is then easy to build an arity-uncompliant term that makes the preservation of con?uence to fail. Let Y = ωs ωs with ωs = λx.s x x. The term ? (id ωs ωs ) (id ωs ωs ) is an arity-uncompliant β-normal form. Reducing the id’s leads to ? Y Y which is the head of an unjoinable critical peak. However, we do not assume that every term at hand is arity-compliant. Indeed, a term that has an arity-compliant β-normal form does not need to be arity-compliant itself. More precisely, for a weakly β-normalizing term, the leftmost-outermost strategy (for →β ) never evaluates subterms that are not βnormalizing and it follows that such subterms may be arity-uncompliant without disturbing the projection on β-normal forms. The point is the well-foundedness of the leftmost-outermost strategy for →β on weakly β-normalizing terms [3]. This strategy can be described by means of head β-reductions, that are easily shown to commute with (parallel) conditional rewriting. Any λ-term can be written λx.v a0 a1 . . . an where either v ∈ X ∪F (a) or v is a λ-abstraction (b). We denote by →h the head β-step λx.(λy.b)a0 a →h λx.b{y → a0 }a. Let s ? t i? either s is of the form (b) and s →h t, or s is of the form (a) with n ≥ 1 and t = ai for some i ≥ 0. In the latter case, the free variables of t can be bound in s. Hence, t can be a subterm of a term α-equivalent to s ; for instance λx.fx ? y for all y ∈ X .

Lemma 8. Let WN be the set of weakly β-normalizing terms ; (i) if s ∈ WN and s ? t then t ∈ WN , (ii) ? is well-founded on WN . It follows that we can reason by well-founded induction on ?. For all i ≥ 0, we use a nested parallelization of →Ai . It corresponds to the one used in [23], that can be seen as a generalization of Tait and Martin-L¨f parallel relation. o As for ?β and →β , in the orthogonal case, a complete development of →Ai can be simulated by one step ?Ai -reduction. This relation is also an adaptation to conditional rewriting of the parallelization used in [12]. De?nition 9 (Conditional nested parallel relations). For all i ≥ 0, let ?Ai be the smallest parallel rewrite relation closed by: (rule) d = c ? l → r ∈ R lσ →Ai rσ lσ ?Ai rθ σ ?Ai θ

Recall that lσ →Ai rσ is ensured by dσ ↓Ai?1 cσ. These relations enjoy some nice properties: (1) →Ai ? ?Ai ? →? i , (2) s ?Ai t ? u{x → s} ?Ai u{x → t} A and (3) [s ?Ai t & u ?Ai v] ? u{x → s} ?Ai v{x → t}. The last one implies commutation of ?Ai and →h . Commutation of rewriting with head β-reduction has already been coined in [2]. We now turn to the main lemma. Lemma 10. Let R be an arity-compliant algebraic system. If s ∈ U and s →? β∪A t, then t ∈ U and βnf (s) →? βnf (t). A Proof Sketch. We show by induction on i the property for →? i . We denote β∪A by (I) the corresponding induction hypothesis. The case i = 0 is trivial. Assume that i > 0. An induction on the number of →β∪Ai -steps leads us to prove that βnf (s) ?Ai βnf (t) whenever s ?Ai t and s has an arity-compliant β-normal form. We reason by induction on ?. First (1), assume that s is of the form (a). If no rule is reduced at its head, the result follows from induction hypothesis on ?. Otherwise, there is a rule d = c ? l → r such that s = λx.lσa and t = λx.rθb with lσ?Ai rθ and dσ ↓Ai?1 cσ. Since l is algebraic, βnf (s) is of the form λx.lσ ′ a′ where σ ′ = βnf (σ) and a′ = βnf (a). Since βnf (s) is arity-compliant, a′ = ?, hence a = ? and s = λx.lσ. Therefore, because lσ ?Ai rθ, we have b = ? and t = λx.rθ. It remains to show that t has an arity-compliant normal form and that βnf (s) = λx.lσ ′ ?Ai βnf (t). Because l is algebraic, its variables are ?+ l. We can then apply induction hypothesis on σ ?Ai θ. It follows that θ has an arity-compliant normal form θ′ with σ ′ ?Ai θ′ . Since r is algebraic, λx.rθ′ is the (arity-compliant) β-normal form of t. Hence it remains to show that lσ ′ ?Ai rθ′ . Because σ ′ ?Ai θ′ , it su?ces to prove that lσ ′ →Ai rσ ′ . Thus, we are done if we show that dσ ′ ↓Ai?1 cσ ′ . Since d and c are algebraic, βnf (dσ) = dσ ′ and βnf (cσ) = cσ ′ . Now, since d is algebraic and arity-compliant and σ ′ is arity compliant, dσ ′ is arity-compliant. The same holds for cσ ′ . Hence we conclude by applying induction hypothesis (I) on dσ ↓Ai?1 cσ. Second (2), when s is of the form (b) we head β-normalize it and obtain a term s′ of the form (a) having an arity-compliant β-normal form. Using commutation

of ?Ai and →h , we obtain a term t′ such that s′ ?Ai t′ . Since s ?+ s′ , we can reason as in case (1). The preservation of con?uence is a direct consequence of the projection on β-normal forms. Theorem 11. Let R be an arity-compliant algebraic system such that →A is con?uent. Then, →β∪A is con?uent on U. Comparison with Dougherty’s work. This section is an extension of [12]. We give a further exploration of the idea that preservation of con?uence, when using hypothesis on →β , should be independent from any typing discipline for the λ-calculus. Moreover, we extend its result in three ways. First, we adapt it to conditional rewriting. Second, we allow nested symbols in lhs to be applied to less arguments than their arity. And third, we use weakly β-normalizing terms whose normal forms are arity-compliant ; whereas Dougherty uses the set of strongly normalizing arity-compliant terms which is closed by reduction.

4

Using →β in the evaluation of conditions

The goal of this section is to give conditions on R to deduce con?uence of →β∪B from con?uence of →A . We achieve this by exhibiting two di?erent criteria ensuring that →? ? →? →? ←? . (?) β∪B β A β The ?rst case concerns left-linear and semi-closed systems. This holds only on some sets of terms that, after Dougherty [12], we call R-stable, although our de?nition of stability does not require strong β-normalization (see Sect. 3.2 and Def. 12). This is an extra hypothesis compared to the result of Sect. 3.1. The second case is a direct extension of Lemma 10 to →β∪B . In both cases, we assume the rules to be algebraic and arity-compliant. We are then able to obtain con?uence of →β∪B since, in each case, our assumptions ensure that the results of Sect. 3 applies, hence that →β∪A is con?uent whenever →A is. It is important to underline the meaning of (?). Given an arity-compliant algebraic rule d = c ? l → r, every β-redex occurring in dσ or cσ also occurs in lσ. Then, (?) means that there is a β-reduction starting from lσ that reduces these redexes and produce a substitution σ ′ such that lσ →? lσ ′ →A rσ ′ ←? rσ. β β In other words, if the conditions are satis?ed with σ and →β∪B (i.e. dσ ↓β∪B cσ), then they are satis?ed with σ ′ and →A (i.e. dσ ′ ↓A cσ ′ ). We now give some examples of non arity-compliant or non algebraic rules in which, at the same time, (?) fails and →β∪B is not con?uent whereas →β∪A for (1), (3), (4) and at least →A for (2) is. (1) (2) (3) (4) gx → xc hx → x gx → x gx = d ? fx → a xc = d ? fx → a hxc = d ? fx → a hxc = d ? fx → a fx → b fx → b fx → b fx → b

hxy → gxy

The ?rst and second examples respectively contain a rule with a non algebraic right-hand side and a rule with a non algebraic condition. Examples (3) and (4) use non arity-compliant terms, in the conditional part and in the right-hand side of a rule respectively. For these four examples, the step f(λx.d) →B a is not in →? →? ←? and a ←B f(λx.d) →B b is an unjoinable peak. β A β However, (?) is by no means a necessary condition ensuring that →β∪B is con?uent when →β∪A so is. In the above examples, con?uence of →β∪B can be recovered when adding appropriate rules, yet not restoring (?). As we are interested in deducing the con?uence of →β∪B from the con?uence of →A , it is more convenient to take in Def. 2 →B = i≥0 →Bi with →B0 =→A instead of →B0 = ? (this does not change →B since →A ?→B ). 4.1 Con?uence of left-linear systems

In this paragraph, we prove (?) provided that rules are arity-compliant, algebraic, left-linear and semi-closed. This inclusion is shown on R-stable sets of terms. De?nition 12 (R-stable sets). Let R be a set of rules. A set S is almost R-stable if it contains only arity-compliant terms, is stable by subterm and βreduction, and C[rσ] ∈ S whenever C[lσ] ∈ S and d = c ? l → r ∈ R. An almost R-stable set S is R-stable if dσ, cσ ∈ S whenever C[lσ] ∈ S and d = c ? l → r ∈ R. This includes the set of strongly →β∪A -normalizable arity-compliant terms and any of its subset closed by subterm and reduction, by using a simple type discipline for instance. The inclusion (?) is proved by induction on the strati?cation of →B with ? ? ? →B0 =→A . The base case corresponds to →? β∪A ? →β →A ←β , which does not require rule conditions to be algebraic nor arity-compliant. The previous examples show however that this may fail in presence of arityuncompliant or non-algebraic right-hand sides. Note that the result is proved only on almost R-stable sets of terms. Note also that a set containing a term reducible by the ?rst rule of example (4) above is obviously not stable. Finally, note that the β-expansion steps are needed because rules can be duplicating. Lemma 13. Let R be a semi-closed left-linear right-algebraic system. On any ? ? ? almost R-stable set of terms, →? β∪A ? →β →A ←β . Proof Sketch. The proof is in four steps. We begin (1) to show that →A ?β ? ?β →? ?β , reasoning by cases on the step ?β . This inclusion relies on A an important fact of algebraic terms: if s is algebraic and sσ ?β v then v ?β sσ ′ with σ ?? σ ′ . From (1), it follows that (2) →? ?β ? ?β →? ?? , by induction A A β β on the number of →A -steps. Then (3), we obtain →? ?? ? ?? →? ?? using an A A β β β induction on the number of ?β -steps and the diamond property of ?β . Finally (4), we deduce that (?β ∪ →A )? ? ?? →? ?? by induction on the length of A β β (?β ∪ →A )? . We now turn to the main result of this subsection. As seen in the previous examples, rules have to be algebraic and arity-compliant.

Lemma 14. Let R be a semi-closed left-linear algebraic system. On any Rstable set of terms, →? ? →? →? ←? . β∪B β A β Proof Sketch. The ?rst point is to see that (1) →? 1 ?→? →? ←? . This is done B β A β by induction on the number of B1 -steps, using Lemma 13. We then deduce (2) →? 1 ?→? →? ←? , by induction on the number of →β∪B1 -steps. The result A β∪B β β follows from an induction on i showing that →Bi ?→B1 . Theorem 15. Assume that R is a semi-closed left-linear algebraic system. If →A is con?uent, then →β∪B is con?uent on any R-stable set of terms. Recall that in this case →β∪A -con?uence follows from →A -con?uence by Thm. 6. 4.2 Con?uence on weakly β-normalizing terms

This subsection concerns the straightforward extension to →B of the results of Sect. 3.2. The de?nition of ?Bi follows the same scheme as the one of ?Ai ; the only di?erence is that Bi is used everywhere in place of Ai . It follows that given a rule d = c ? l → r, to have lσ ?Bi rθ, we must have σ ?Bi θ and dσ ↓β∪Bi?1 cσ. The relations ?Bi enjoy the same nice properties as the ?Ai ’s. Lemma 16. Let R be an arity-compliant algebraic system. If s ∈ U and s →? β∪B t, then t ∈ U and βnf (s) →? βnf (t). A The only di?erence in the proof is that the case i = 0 is now ensured by Lemma 10 (since →B0 =→A ). The theorem follows easily: Theorem 17. Let R be an arity-compliant algebraic system such that →A is con?uent. Then, →β∪B is con?uent on U.

5

Orthonormal systems

In this section, we give a criterion ensuring con?uence of →β∪B when conditions and right-hand sides possibly contain abstractions and active variables. This criterion comes from peculiarities of orthogonality with conditional rewriting. In non-conditional rewriting, a system is orthogonal when it is leftlinear and has no critical pair. A critical pair comes from the superposition of two di?erent rule left-hand sides at non-variable positions. The general de?nition of orthogonal conditional systems is the same. But, in conditional rewriting, there can be superpositions of two di?erent rules left-hand sides whose conditions cannot be satis?ed with the same substitution. Such critical pairs are said infeasible and it could be pro?table to consider systems whose critical pairs are all infeasible. In [21], it is remarked that results on the con?uence of natural and normal orthogonal conditional systems should be extended to systems that have no feasible critical pair. But the results obtained this way are not directly applicable

since proving unfeasibility of critical pairs may require con?uence. In Takahashi’s work [22], conditions can be any predicate P on terms. Con?uence is proved with the assumption that they are stable by reduction: if P σ holds and σ → θ, then P θ holds. For the systems studied in this section, stability of conditions by reduction precisely follows from con?uence. Hence the results of [22] do not directly apply. The purpose of this section is to give a syntactic condition on rules that imply unfeasibility of critical pairs, hence con?uence. De?nition 18 (Conditional critical pairs). Given two rules d = c ? l → r and d′ = c′ ? l′ → r′ , if p is a non-variable position in l and σ is a most general uni?er of l|p and l′ , then dσ = cσ ∧ d′ σ = c′ σ ? (l[r′ ]p σ, rσ) is a conditional critical pair. A critical pair d = c ? (s, t) is feasible for →A (resp. →B ) if there is a substitution σ such that dσ ↓A cσ (resp. dσ ↓β∪B cσ). As an example, consider the rules used to de?ne occ in Sect. 2. There is a superposition between the left-hand sides of the last two rules giving the critical peak ? ← occ (x :: o) (nd y l) → occ o (get l x). But a peak of this form can occur only if there are two terms s, t such that tt ←? ≥ (len s) t →? ?. Using the strati?cation of →A , the con?uence of →Ai implies that this pair is not feasible. Hence the above peak cannot occur with →Ai+1 and this relation is con?uent. This method can be used on systems with higher-order terms in right-hand sides and conditions, as for example the rules de?ning app and ?lter. Hence, it is useful for proving the con?uence of →β∪B for systems where this relation does not need to be included in ?? . In this section, we generalize the method and β∪A apply it on a class of systems called orthonormal. As in the previous section, we use strati?cation of →B , but now with →B0 = ?. A symbol f ∈ F is de?ned if it is the head of a rule left-hand side. De?nition 19 (Orthonormal systems). A system is orthonormal if (1) it is left-linear; (2) in every rule d = c ? l → r, the terms in c are closed βnormal forms not containing de?ned symbols; and (3) for every critical pair d = c ? (s, t), there exists i = j such that di = dj and ci = cj . Note that an orthonormal system is left-linear and semi-closed, but does not need to be arity-compliant or algebraic. Note also that the form of the conditions leads to a normal conditional rewrite relation. The reader can check that the whole system given in Sect. 2 is orthonormal. We now prove that →β∪B is shallow con?uent (i.e. →? i and →? j comβ∪B β∪B mute for all i, j ≥ 0) when R is orthonormal. The ?rst point is that con?uence of →β∪Bi implies commutation of →? and →? i+1 . The proof is as in Sect. 3.1, B β except that in a rule d = c ? l → r, c are closed →β∪B -normal forms. The main Lemma concerns commutation of parallel relations of ?Bi and ?Bj for all i, j ≥ 0. But here, we use a weak form of parallelization: ?Bi is simply the parallel closure of →Bi . The name of the Lemma is usual for this kind of result with rewriting (see [21]). Write <mul for the multiset extension of the usual ordering on naturals numbers.

Lemma 20 (Parallel Moves). Let R be an orthonormal system. If {n, m} <mul {i, j} implies commutation of →? n and →? m , then ?Bi and ?Bj commute. β∪B β∪B Proof Sketch. The key point is the commutation of →? n and →? m for β∪B β∪B {n, m} <mul {i, j}. It implies that two rules whose respectives conditions are satis?ed with →? i and →? j are not superposable at non-variable positions. β∪B β∪B The rest of the proof follows usual schemes (see Sect. 7.4 in [21]). Now, an induction on <mul provides the commutation of →β∪Bi and →β∪Bj for all i, j ≥ 0. Shallow con?uence immediately follows. Theorem 21. If R is an orthonormal system, then →β∪B is shallow con?uent. Hence, the relation →β∪B induced by the system of Sect. 2 is con?uent.

6

Conclusion

Our results are summarized in the following table. § 3.1 3.2 Terms T U Lhs Linear Rhs Applicative Conditions Semi-Closed Result →A Con?uent ? →A∪β Con?uent

Arity-Compliant Arity-Compliant idem & Algebraic & Algebraic Semi-Closed →A Con?uent ? 4.1 R-stable Linear Algebraic & Algebraic →B∪β Con?uent Arity-Compliant Arity-Compliant 4.2 U idem & Algebraic & Algebraic →B∪β 5 T Linear Orthonormal Shallow Con?uent We provide detailed conditions to ensure modularity of con?uence 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 speci?cation side and for enriching the conversion used in logical frameworks or proof assistants, while still preserving the con?uence property. These results lead us to the following remarks and further research points. The results obtained in Sect. 3 and 4 for the standard conditional rewrite systems extend to the case of oriented systems (hence to normal systems) and to the case of level-con?uent natural systems. For natural systems, the proofs follow the same scheme, provided that level-con?uence of →A is assumed. However, it would be interesting to know if this restriction can be dropped. Problems arising from non left-linear rewriting are directly transposed to leftlinear conditional rewriting. The semi-closure condition is su?cient to avoid this, and it provides the counter part of left-linearity for unconditional rewriting. As a matter of a fact, it is well known that orthogonal standard conditional rewrite

systems are not con?uent, but con?uence of orthogonal semi-closed standard systems holds. However, two remarks have to be made about this restriction. First, it would be interesting to know if it is a necessary condition and besides, to characterize a class of non semi-closed systems that can be translated into equivalent semi-closed ones. Second, semi-closed terminating standard systems behave like normal systems. But normal systems can be easily translated in equivalent non-conditional systems. Moreover such a translation preserves good properties such as left-linearity and non-ambiguity. As many of practical uses of rewriting rely on terminating systems, semi-closed standard systems may be in practice essentially an intuitive way to design rewrite systems that can be then e?ciently implemented by non-conditional rewriting. An interesting extension of this work consists in adapting to conditional rewriting the axiomatization and the results of [23]. This should leads to a generalization of the higher-order conditional systems of [1]. Acknowledgments. We are quite grateful to the anonymous referees for their constructive and accurate comments and suggestions.

References

[1] J. Avenhaus and C. Lor? aenz. Higher order conditional rewriting and narrowia-S? ing. In Proceedings of the 1st International Conference on Constraints in Computational Logics, volume 845 of LNCS, pages 269–284. Springer Verlag, 1994. [2] F. Barbanera, M. Fern?ndez, and H. Geuvers. Modularity of Strong Normalisation a and Con?uence in the Algebraic λ-Cube. Journal of Functional Programming, 7(6):613–660, November 1997. [3] H.P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. North Holland, 1984. Second edition. [4] G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure Patterns Type Systems. In Principles of Programming Languages, New Orleans, USA. ACM, 2003. [5] F. Blanqui. De?nitions by rewriting in the calculus of constructions. Mathematical Structures In Computer Science, 15(1):37–92, 2005. [6] F. Blanqui, C. Kirchner, and C. Riba. On the con?uence of lambda-calculus with conditional rewriting. HAL technical report, Oct 2005. [7] V. Breazu-Tannen. Combining algebra and higher-order types. In 3rd IEEE Symposium on Logic in Computer Science Edinburg (UK), july 1988. [8] V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic con?uence. Information and Computation, 114(1):1–29, October 1994. [9] H. Cirstea and C. Kirchner. The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427–498, May 2001. [10] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 243–320. North-Holland, 1990. [11] N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990. [12] D.J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251–267, December 1992. [13] G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33–72, Nov 2003.

[14] Bernhard Gramlich. On termination and con?uence properties of disjoint and constructor-sharing conditional rewrite systems. Theoretical Computer Science, 165(1):97–131, September 1996. [15] J.-P. Jouannaud and M. Okada. Executable higher-order algebraic speci?cation languages. In Proceedings of LICS’91. [16] J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Center Tracts. CWI, 1980. PhD Thesis. [17] J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. TCS, 121:279–308, 1993. [18] A. Middeldorp. Completeness of Combinations of Conditional Constructor Systems. Journal of Symbolic Computation, 17(1):3–21, January 1994. [19] F. M¨ller. Con?uence of the lambda calculus with left linear algebraic rewriting. u Information Processing Letters, 41:293–299, 1992. [20] T. Nipkow. Higher-order critical pairs. In Proceedings of LICS’91. [21] E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, April 2002. [22] M. Takahashi. Lambda-calculi with conditional rules. In TLCA’93, LNCS, pages 406–417. Springer-Verlag, 1993. [23] V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies con?uence: the higher-order case. In LFCS’94, volume 813 of LNCS, 1994.

7

Proofs of Section 3.2

We begin by proving the well-foundedness of ?. Lemma 22. Let WN be the set of weakly β-normalizing terms. The set WN is stable by ? and ? is well-founded on WN . Proof. For the ?rst part, let be s ∈ WN and s ? t. If s is of the form (b), the ?rst 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 ?rst point t ∈ WN . Since s →h t, we have #(s) > #(t). Otherwise, the leftmostoutermost strategy starting from s reduces by leftmost-outermost reductions each ai (1 ≤ i ≤ n). Hence #(s) ≥ #(t). But in this case, t is a proper subterm of s, hence |s| > |t|. Then, we consider the properties (1)-(3) of the walk relations ?Ai . Proposition 23. For all i ≥ 0, 1. →Ai ? ?Ai ? →? i . A 2. s ?Ai t ? u{x → s} ?Ai u{x → t}. 3. [s ?Ai t & u ?Ai v] ? u{x → s} ?Ai v{x → t}.

Proof. The ?rst point is shown by induction on the de?nition of ?Ai ; the second by induction on u. For the last one, we also use an induction on ?Ai in u ?Ai v. If u is v, the result is trivial. If u ?Ai v was obtained by parallel application or if u is an abstraction, the result follows from induction hypothesis. Otherwise, u ?Ai v is obtained by (rule). That is, there is a rule d = c ? l → r ∈ R such that u = lσ, v = rθ, σ ?Ai θ and lσ →Ai rσ. Since →Ai is a rewrite relation, we have lσ{x → s} ?Ai rσ{x → s}. By induction hypothesis, we have σ{x → s} ?Ai θ{x → t}. Therefore lσ{x → s} ?Ai rθ{x → t}. We now turn to the commutation of ?Ai and →h . This is a direct consequence of the case (3) of the above Proposition. Lemma 24. For all i ≥ 0, ?Ai commutes with →h . Proof. Assume that s ←h λx.(λy.a0 )a1 . . . ap ?Ai t. Because rules have nonvariable algebraic left hand-sides, t = λx.(λy.b0 )b1 . . . bp with for all k ∈ {0, . . . , p}, ak ?Ai bk . On the other hand, s = λx.a0 {y → a1 }a2 . . . ap . It follows from Prop. 23.3 that a0 {x → a1 } ?Ai b0 {x → b1 } (in one step). Hence we have s ?Ai λx.b0 {y → b1 }b2 . . . bp ←h t. u

8

Proofs of Section 4.1

We begin by two technical properties. The ?rst one is a generalization of the diamond property of ?β . Proposition 25. Let be n ≥ 0 and assume that s, s1 , . . . , sn are terms such that for all 1 ≤ i ≤ n, s ?β si . Then there is a term s′ such that for all 1 ≤ i ≤ n, si ? β s′ . Proof. The proof is by induction on the structure of s. First, if s is a constant symbol or a variable, then it is a β-normal from and we are done. If s is an abstraction λx.t, then for all 1 ≤ i ≤ n, si is of the form λx.ti and we conclude by induction hypothesis on t, t1 , . . . , tn . Now assume that s is an application. There are two cases. First, s = tu where t is not an abstraction. Then, for all 1 ≤ i ≤ n, si is of the form ti ui with t ?β ti and u ?β ui and we conclude by induction hypothesis. Otherwise, s must be of the form (λx.t)u and for all 1 ≤ i ≤ n, si is either of the form (λx.ti )ui (1) or of the form ti {x → ui } (2). In both cases we have t ?β ti and u ?β ui . By induction hypothesis, there are two terms t′ , u′ such that for all 1 ≤ i ≤ n, ti ?β t′ and ui ?β u′ . Therefore, in case (1), we have (λx.ti )ui ?β t′ {x → u′ } and in case (2) ti {x → ui } ?β t′ {x → u′ }. Hence, for all 1 ≤ i ≤ n, si ?β t′ {x → u′ }. For the following Proposition, we de?ne O(t, u), the set of occurrences of t in u as : O(t, u) = ε if t = u ; otherwise O(t, u1 u2 ) = 1.O(t, u1 ) ∪ 2.O(t, u2 ), O(t, λx.u) = 1.O(t, u) and O(t, x) = O(t, f) = ?.

Proposition 26. Let s be an algebraic term. 1. If sσ ?β v then there is σ ′ such that σ ?? σ ′ and v ?β sσ ′ . β 2. If sσ ?? v then there is σ ′ such that σ ?? σ ′ and v ?? sσ ′ . β β β Note that s does not needs to be linear. Proof. 1. Since s is algebraic, every occurrence of β-redex of sσ is of the form p.d where p is the occurrence of a variable x in s and d is an occurrence in σ(x). Therefore, v is of the form s[t(x, p)]{p ; p∈O(x,s)

& x∈F V (s)}

where, for all x ∈ F V (s), for all p ∈ O(x, s), σ(x) ?β t(x, p). By Prop. 25, for all x ∈ F V (s), there exists t(x) such that for all p ∈ O(x, s), t(x, p) ?β t(x). Hence v ?β s[t(x)]{p ; p∈O(x,s)

& x∈F V (s)}

.

That is, v ?β sσ ′ with σ ′ (x) = t(x). 2. We reason by induction on the number of ?β -steps. If sσ = v the result is trivial. Otherwise, sσ ?? v is sσ ?β v ′ ?? v. By (1), there is a substitution σ ′ β β such that sσ ?β v ′ ?β sσ ′ . By strong con?uence of ?β , there is a v ′′ such that sσ ′ ?? v ′′ ?? v and the length of sσ ′ ?? v ′′ is no more than the length of v ′ ?? v. β β β β Hence, we can apply induction hypothesis on sσ ′ ?? v ′′ and thus obtain σ ′′ such β that sσ ?? v ?? sσ ′′ . β β We now turn to the inclusion →? ?→? →? ←? on almost R-stable terms. βA β A β We begin by showing that →A ?β ? ?β →? ?β . A Proposition 27. Let R be a semi-closed left-linear right-algebraic system. On any almost R-stable set of terms, →A ?β ? ?β →? ?β . A Proof. Let R be the binary relation be such that, for all t, u, R(t, u) ? ?s [ s →A t ?β u ? ?s′ t′ (s ?β s′ →? t′ ?β t) ] A We have to show that R is re?exive and compatible with terms formations rules, parallel application and with the rule (beta). Re?exivity of R is trivial. We now prove that R is compatible with termformation rules, parallel application and (beta). Term-Formation Note that compatibility with parallel application contains compatibility with application. Hence compatibility with context is only compatibility with λ-abstraction. We have to show that if R(t1 , u1 ) holds, then R(λx.t1 , λx.u1 ) holds whenever t1 ?β u1 . So assume R(t1 , u1 ), t1 ?β u1 and let s be such that s →A λx.t1 ?β λx.u1 . Write t for λx.t1 and u for λx.u1 . If the contractum of the step s →A t is in a proper subterm of t, we have s = λx.s1 with s1 →A t1 and we conclude by assumption and context compatibility of →A and ?β . Otherwise, there

is a rule d = c ? l → r such that s = lσ and t = rσ. As r is algebraic, by Prop. 26 there is a substitution σ ′ such that σ ?? σ ′ and u ?β rσ ′ . By β linearity of l, we have lσ ?β lσ ′ . We now show that lσ ′ →A rσ ′ . To this end he have to show that dσ ′ ↓A c. But dσ ?? dσ ′ and by Lem. 5 there are terms β v such that dσ ′ →? v ←? ←? c. Because terms in c and right-hand sides A β A of rules are build without abstraction symbols, there cannot be any β-step starting from an →A -reduct of c. Hence dσ ′ ↓A c and we are done. Parallel application We have to show that [ R(t1 , u1 ) & R(t2 , u2 ) ] ? R(t1 t2 , u1 u2 ) whenever t1 ?β u1 and t2 ?β u2 . So, assume R(t1 , u1 ), R(t2 , u2 ), and let s be such that s →A t1 t2 ?β u1 u2 where ti ?β ui . Write t for t1 t2 and u for u1 u2 . If the contractum of the step s →A t is in a proper subterm of t we can conclude by assumption and context compatibility of →A and ?β . Otherwise s = lσ and t = rσ for a rule d = c ? l → r and we conclude as in Case 1. (beta) rule We have to show that [ R(t1 , u1 ) & R(t2 , u2 ) ] ? R((λx.t1 )t2 , u1 {x → u2 }) whenever t1 ?β u1 and t2 ?β u2 . So assume R(t1 , u1 ), R(t2 , u2 ), and let s be such that s →A (λx.t1 )t2 ?β u1 {x → u2 } where ti ?β ui . Write t for (λx.t1 )t2 and u for u1 {x → u2 }. As above, if s →A t, is a rooted rewrite step, we refer to the Case 1. Otherwise, as s is arity-compliant, λx.t1 is not the instantiated right hand side of a rule d = c ? l → r. Indeed, if it where, we would have s = f ls2 with l = f l. But the term f ls2 is not arity-compliant, contradicting the hypothesis of stability. So we are in cases where s = (λx.s1 )t2 (resp. (λx.t1 )s2 ) with s1 →A t1 (resp. s2 →A t2 ). In both cases, we conclude by assumption and context compatibility of →A and ?β . Lemma 28. Let R be a semi-closed left-linear right-algebraic system. On any almost R-stable set of terms, →? ?→? →? ←? . A β β∪A β Proof. The proof is in three steps. We ?rst show (1) →? ?β ? ?β →? ?? , by induction on the number of A A β A-steps. Assume that s →? t′ →A t ?β u. By Lemma 27, there are v and v ′ such A that t′ ?β v →? v ′ ?β u. By induction hypothesis, there are s′ and s′′ such that A s ?β s′ →? s′′ ?? v. Then, by Lemma 5, there is t′′ such that s′′ →? t′′ ?? v ′ . A A β β Thus, s ?β s′ →? t′′ ?? u. A β We now show (2) →? ?? ? ?? →? ?? , by induction on the number of A A β β β ?β -steps. Assume that s →? t ?β u′ ?? u. After (1), there are s′ and t′ such that A β s ?β s′ →? t′ ?? u′ . By strong con?uence of ?β , there is v such that t′ ?? v ?? u, A β β β where t′ ?? v is no longer than u′ ?? u. Hence, by induction hypothesis, there β β are s′′ and t′′ such that s′ ?? s′′ →? t′′ ?? v. Therefore, s ?? s′′ →? t′′ ?? u. A A β β β β We now prove (3) (?β ∪ →A )? ? ?? →? ?? , by induction on the length β A β of (?β ∪ →A )? . Assume that s →?β ∪A t →? β ∪A u. There are two cases. First, ?

s ?β t. This case follows directly from the induction hypothesis. Second, s →A t. By induction hypothesis, there are t′ and u′ such that t ?? t′ →? u′ ?? u. After β A β (2), there are s′′ and u′′ such that s ?? s′′ →? u′′ ?? u′ . Finally, by Lemma 5, A β β there is t′′ such that u′′ →? t′′ and t′ ?? . Hence, s ?? s′′ →? t′′ ?? t. A A β β β We conclude by the fact that ?? =→? . β β We now turn to the proof of →? ? →? →? ←? on R-stables sets. A β β β∪B Lemma 29. Let R be an arity-compliant semi-closed left-linear algebraic system. On any set of R-stable terms, →? ?→? →? ←? . A β∪B β β Proof. We ?rst prove (1) →B1 ?→? →? ←? . Let R be the binary relation such A β β that for all s, t ∈ T , R(s, t) ? [ s →B1 t ? s →? →? ←? t ] . β A β We have to show that R is compatible with term-formation rules and that for all d = c ? l → r ∈ R, for all substitution σ, if dσ ↓A∪β cσ then R(lσ, rσ) holds. We only show this latter property. Let d = c ? l → r be a rule and assume that lσ →B1 rσ. Then, dσ ↓β∪A cσ. Since c is a closed algebraic term, we have ? dσ →? β∪A u ←A c with both c and u in β-normal form. Because dσ is stable, we can apply Lemma 28 and obtain v such that dσ →? v →? u. By Prop. β A 26, there is σ ′ such that v →? dσ ′ . Now, by Lemma 5, dσ ′ →? u. Therefore, A β s →A t. We now prove (2) →? 1 ?→? →? ←? , by induction on the number of β ∪B1 β∪B β A β steps. Assume that s →? 1 t →β∪B1 u. By induction hypothesis, s →? s′ →? A β∪B β t′ ←? t. There are two cases. First, t →β u. By β-con?uence, t′ →? u′ ←? u. β β β Applying Lem. 28 leads to s′ →? →? ←? u′ and we get s →? →? ←? u. Assume A A β β β β now that t →B1 u. From (1) it follows that, t →? t′ →? u′ ←? u. Then, by A β β 2 virtue of β-con?uence, t′ →? t′′ ←? t′ . Commutation of β and A (Lem. 5) β β 2 gives u′′ such that t′′ →? u′′ ←? u′ . Finally, by Lemma 28, s′ →? →? ←? u′′ . A β A β β Therefore, s →? →? ←? u. A β β We then prove by induction on i ≥ 1 that →Bi ?→B1 . Let i ≥ 1 and let Pi be the binary relation such that for all s, t ∈ T , Pi (s, t) ? [ s →Bi t ? s →B1 t ] . We have to show that Pi is compatible with term-formation rules and that for all d = c ? l → r ∈ R, for all substitution σ, if dσ ↓A∪β cσ then Pi (lσ, rσ) holds. We only show this latter property. Let d = c ? l → r be a rule and assume that lσ →Bi rσ. Then, dσ ↓β∪Bi?1 cσ. By induction hypothesis and since c is a closed algebraic term, we have dσ →? 1 u ←? c with both c and u in β-normal form. β∪B A By (2), dσ →? →? u ←A c. Therefore, lσ →B1 rσ. A β Theorem 30. Assume that R is an arity-compliant semi-closed left-linear algebraic system. If →A is con?uent then →β∪B is con?uent on any set of R-stable terms.

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

9

Proofs of Section 5

We begin by the commutation of →? and →? i . β B Lemma 31. If R is an orthonormal system and →β∪Bi is con?uent then →? i+1 B and →? commute. β Proof. The proof follows the lines of the proof of Lemma 5. It also uses the relation ?β de?ned in Sect. 3. We just prove that if d = c ? l → r is a rule such that u ?β lσ →Bi+1 rσ then there is a v such that u →? i+1 v ?β rσ. B As l is a non variable linear algebraic term, there is a substitution σ ′ such that σ ?β σ ′ and lσ ?β lσ ′ = u. Therefore, rσ ?β rσ ′ . It remains to show that lσ ′ →Bi+1 rσ ′ . Recall that dσ →? i c. As dσ →? dσ ′ , by hypothesis, there is v β∪B β such that dσ ′ →? i v ←? c. But c are β-normal forms, hence v = c. Therefore, β∪B β lσ ′ →Bi+1 rσ ′ ?β rσ. We now turn to parallel moves. Lemma 20 is decomposed into Lemmas 32 and 33. We denote by →= the re?exive closure of a rewrite relation →. Lemma 32. Let R be an orthonormal system and i, j ≥ 0. Assume that, for all n, m such that {n, m} <mul {i, j} diagram (i) commutes. Let d = c ? l → r be a conditional rewrite rule in R. Then, diagram (ii) commutes. s

β∪Bm ? β∪Bn ?

/t

? β∪Bm

lσ

?Bj

Bi

/ rσ

?Bj

u

? β∪Bn

/v

u

= Bi

/v

(i)

(ii)

Proof. The results holds if i = 0 since →B0 = ?. If j = 0, then u = lσ and take v = rσ. Assume that i, j > 0 and write q1 , . . . , qn for the (disjoint) occurrences in lσ of the redexes contracted in lσ ?Bj u. Therefore, for all k, 1 ≤ k ≤ n, there exists a rule ρk : dk = ck ? lk → rk and a substitution θk such that lσ|qk = lk θk . Thus, u = lσ[r1 θ1 ]q1 . . . [rn θn ]qn . 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 qk is a non variable occurrence in l. Hence rules ρ and ρk forms an instance of a critical pair d′ ? = c′ ? (l[rk ]qk ?, r?) and there exists a substitution ?′ such that σ = ??′ . By de?nition of orthonormal systems, |d′ ?| ≥ 2 and there is m = p such that

c′ = c′ and d′ ? = d′ ?. Let us write h for max(i, j) ? 1. As d′ ? = d′ ? we m p m p m p have d′ σ = d′ σ and it follows that c′ ←? h d′ σ = d′ σ →? h c′ . But m p m m p p β∪B β∪B {h, h} <mul {i, j} and by assumption →β∪Bh is con?uent. Therefore we must have c′ ↓β∪Bh c′ . But it is not possible since c′ and c′ are distinct normal m p m p forms. Hence, conditions of ρ and ρk can not be both satis?ed by σ and →β∪Bh and it follows that there is no non-variable superposition. Therefore, each qk is of the form uk .vk where l|uk is a variable xk . Let σ ′ be such that σ ′ (xk ) = σ(xk )[rk σ]vk and σ ′ (y) = σ(y) if y ≡ xk for all 1 ≤ k ≤ n. Then, lσ ?Bj lσ ′ and by linearity of l, u = lσ ′ . Furthermore, rσ ?Bj rσ ′ . We now show that lσ ′ →Bi rσ ′ . We have dσ →? i?1 c and dσ →? j dσ ′ . As β∪B B i, j > 0, we have {i ? 1, j} <mul {i, j}. Therefore, by assumption →? i?1 and β∪B →? j commute and there exist terms c′ such that dσ ′ →? i?1 c′ ←? j?1 c. β∪B β∪B β∪B But as terms in c are →β∪B -normal forms, we have c′ = c and it follows that lσ ′ →Bi rσ ′ . Lemma 33. Let R be an orthonormal system and i, j ≥ 0. Diagram (iii) commutes if and only if for all rule d = c ? l → r, diagrams (iv) and (v) commute. s

?Bj ?Bi

/t

?Bj

lσ

?Bj

Bi

/ rσ

?Bj

lσ

?Bi

Bj

/ rσ

?Bi

u

?Bi

/v

u

= Bi

/v

u

= Bj

/v

(iii)

(iv)

(v)

Proof. The “only if” statement is trivial. For the “if” case, let s, t, u be three terms such that u ?Bj s ?Bi t. If s is t (resp. u), then take v = u (resp. v = t). Otherwise, we reason by induction on the structure of s. If there is a rooted reduction, we conclude by commutation of diagrams (iv) and (v). Now assume that both reductions are nested. If s is an abstraction, we conclude by induction hypothesis. Otherwise s is an application s1 s2 , and by assumption u = u1 u2 and t = t1 t2 with uk ?Bj sk ?Bi tk . In this case also we conclude by induction hypothesis. We now turn to the main result with orthonormal systems. Theorem 34. If R is an orthonormal system then →β∪B is shallow con?uent. Proof. By induction on <mul , we show the commutation of →? i and →? j β∪B β∪B for all i, j ≥ 0. The least unordered pair {i, j} with respect to <mul is {0, 0}. As →β∪B0 =→β by de?nition, this case holds by con?uence of β. Now, assume that i > 0 and that the commutation of →? n and →? m β∪B β∪B holds for all n, m with {n, m} <mul {i, 0}. As {i ? 1, i ? 1} <mul {i, 0}, →β∪Bi?1 is con?uent and the commutation of →? i and →? 0 (=→? ) follows from β∪B β∪B β lemma 31. The remaining case is when i, j > 0. Using the induction hypothesis, from Lemma 32 and 33, we obtain commutation of ?Bi and ?Bj , which in turn implies

commutation of →? i and →? j . Now, as {i ? 1, i ? 1} <mul {i, j}, by Lemma 31, B B →? and →? i commute. This way, we also obtain the commutation of →? and β B β →? j . Then, the commutation of →? i and →? j easily follows. B β∪B β∪B

赞助商链接

- Confluence of Curried Term-Rewriting Systems
- Relative Undecidability in Term Rewriting Part 2 The Confluence Hierarchy
- Rewriting calculus with(out) types
- On knowledge-based programming with sensing in the situation calculus
- Confluence of Right Ground Term Rewriting Systems is Decidable
- On the formalization of the modal-calculus in the Calculus of Inductive Constructions
- autoregressive conditional heteroskedasicity with estimates of the variance of U.K.inflation
- Confluence of the BS-calculus
- Operational Semantics of Rewriting with the On-demand Evaluation Strategy
- On the Power of P Systems with Parallel Rewriting and Conditional Communication
- Covariant Hamiltonian formalism for the calculus of variations with several variables
- Higher-Order Rewriting via Conditional First-Order Rewriting in the Open Calculus of Constr
- On the modularity of confluence of constructor-sharing term rewriting systems
- The Separation of Duty with Privilege Calculus
- Confluence of Conditional Rewriting Systems with Built-in Predicates and Standard Premises

更多相关文章：
更多相关标签：