Jiaxiang Liu

Jean-Pierre Jouannaud

Mizuhito Ogawa

Confluence of layered rewrite systems

Keywords: 1998 ACM Subject Classification F.4.2 [Logic and computation]: Rewriting Keywords and phrases Layers, confluence, decreasing diagrams, critical pairs, cyclic unification Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p 1

We investigate the new, Turing-complete class of layered systems, whose lefthand sides of rules can only be overlapped at a multiset of disjoint or equal positions. Layered systems define a natural notion of rank for terms: the maximal number of non-overlapping redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right-linear. Using a novel unification technique, cyclic unification, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.

Introduction

Confluence of terminating systems is well understood: it can be reduced to the joinability of local peaks by Newman's lemma, and to that of critical ones, obtained by unifying lefthand sides of rules at subterms, by Knuth-Bendix-Huet's lemma. Confluence can thus be decided by inspecting all critical pairs, see for example [START_REF] Dershowitz | Rewrite systems[END_REF].

Many efforts notwithstanding [1, 10-12, 14, 15, 18-20, 22-25, 27, 29, 30], confluence of nonterminating systems is far from being understood in terms of critical pairs. Only recently did this question make important progress with van Oostrom's complete method for checking confluence based on decreasing diagrams, a generalization of joinability [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF][START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams converted[END_REF]. In particular, while Huet's result stated that linear systems are confluent provided their critical pairs are strongly confluent [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF], Felgenhauer showed that right-linearity could be removed provided parallel critical pairs have decreasing diagrams [START_REF] Felgenhauer | Rule labeling for confluence of left-linear term rewrite systems[END_REF]. Knuth-Bendix's and Felgenhauer's theorems can join forces in presence of both terminating and non-terminating rules [START_REF] Liu | Confluence by critical pair analysis[END_REF].

We show here that rank non-increasing layered systems are confluent provided their critical pairs have decreasing diagrams. Our confluence result for non-terminating non-linear systems by critical pair analysis is the first we know of. Further, our result holds in case critical pairs become infinite, solving a long standing problem raised in [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF]. Prior solutions to the problem existed under different assumptions that could be easily challenged [START_REF] Gomi | On the Church-Rosser property of root-E-overlapping and strongly depth-preserving term rewriting systems[END_REF][START_REF] Klein | Confluence of non-left-linear TRSs via relative termination[END_REF][START_REF] Toyama | Church-Rosser property and unique normal form property of non-duplicating term rewriting systems[END_REF].

Our results use a simplified version of sub-rewriting introduced in [START_REF] Liu | Confluence by critical pair analysis[END_REF], and a simple, but essential revisitation of unification in case overlaps generate occur-check equations: cyclic unification is based on a new, important notion of cyclic unifiers, which enjoy all good properties of unifiers over finite trees such as existence of most general cyclic unifiers, and can therefore represent solutions of occur-check equations by simple rewriting means.

Terms are introduced in Section 2, labelled rewriting and decreasing diagrams in Section 3, sub-rewriting in Section 4, cyclic unification in Section 5 and layered systems in Section 6 where our main result is developed, before concluding in Section 7.

Terms, substitutions, and rewriting

Given a signature F of function symbols and a denumerable set X of variables, T (F, X ) denotes the set of finite or infinite rational terms built up from F and X . We reserve letters x, y, z for variables, f, g, h for function symbols, and s, t, u, v, w for terms. Terms are recognized by top-down tree automata in which some ω-states, and only those, are possibly traversed infinitely many times. Terms are identified with labelled trees. See [START_REF] Hubert Comon | Tree automata techniques and applications[END_REF] for details.

Positions are finite strings of positive integers. We use o, p, q for arbitrary positions, the empty string Λ for the root position, and "•" for concatenation of positions or sets thereof. We use FPos(t) for the (possibly infinite) set of non-variable positions of t, t(p) for the function symbol at position p in t, t| p for the subterm of t at position p, and t [u] p for the result of replacing t| p with u at position p in t. We may omit the position p, writing t[u] for simplicity and calling t[•] a context. We use ≥ for the partial prefix order on positions (further from the root is bigger), p#q for incomparable positions p, q, called disjoint. The order on positions is extended to finite sets as follows: P ≥ Q (resp. P > Q) if (∀p ∈ P )(∃q ∈ max(Q)) p ≥ q (resp. p > q), where max(P ) is the set of maximal positions in P . We use p for the set {p}.

We use Var(t 1 , . . . , t n ) for the set of variables occurring in {t i } i . A term t is ground if Var(t) = ∅, linear if no variable occurs more than once in t. Given a term t, we denote by t any linear term obtained by renaming, for each variable x ∈ Var(t), the occurrences of x at positions {p i } i in t by linearized variable x ki such that i = j implies x ki = x kj . Note that Var(s) ∩ Var(t) = ∅ iff Var(s) ∩ Var(t) = ∅. Identifying x k0 with x, t = t for a linear term t.

A substitution σ is an endomorphism from terms to terms defined by its value on its domain Dom(σ) := {x : σ(x) = x}. Its range is Ran(σ) := x∈Dom(σ) Var(xσ). We use σ |V for the restriction of σ to V ⊆ Dom(σ), and σ |¬X for the restriction of σ to Dom(σ) \ X. The substitution σ is said to be finite (resp., a variable substitution) if for each x ∈ Dom(σ), σ(x) is a finite term (resp., a variable). Variable substitutions are called renamings when also bijective. A substitution γ is ground if for each x ∈ X , γ(x) is ground. We use Greek letters for substitutions and postfix notation for their application.

The strict subsumption order on finite terms (resp. substitutions) associated with the quasi-order s • ≥ t (resp. σ • ≥ τ ) iff s = tθ (resp. σ = τ θ) for some substitution θ, is well-founded. A rewrite rule is a pair of finite terms, written l → r, whose lefthand side l is not a variable and whose righthand side r satisfies Var(r) ⊆ Var(l). A rewrite system R is a set of rewrite rules. A rewrite system R is left-linear (resp. right-linear, linear) if for every rule l → r ∈ R, l is a linear term (resp. r is a linear term, l and r are linear terms). Given a rewrite system R, a term u rewrites to a term v at a position p, written u → p R v, if u| p = lσ and v = u[rσ] p for some rule l → r ∈ R and substitution σ. The term lσ is a redex and rσ its reduct. We may omit R as well as p, and also replace the former by the rule which is used and the latter by a property it satisfies, writing for example u → >P l→r v. Rewriting terminates if there exists no infinite rewriting sequence issuing from some term. Rewriting is sometimes called plain rewriting.

Consider a local peak made of two rewrites issuing from the same term u, say u → p l→r v and u → q g→d w. Following Huet [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF], we distinguish three cases: p#q (disjoint case), q > p • F Pos(l) (ancestor case), and q ∈ p • F Pos(l) (critical case). Given two, possibly different rules l → r, g → d and a position p ∈ FPos(l) such that Var(l) ∩ Var(g) = ∅ and σ is a most general unifier of the equation l| p = g, then lσ is the overlap and rσ, lσ [dσ] p the critical pair of g → d on l → r at p.

Rewriting extends naturally to lists of terms of the same length, hence to substitutions of the same domain. See [START_REF] Dershowitz | Rewrite systems[END_REF][START_REF]Term rewriting systems[END_REF] for surveys.

Labelled rewriting and decreasing diagrams

Our goal is to reduce confluence of a non-terminating rewrite system R to that of finitely many critical pairs. Huet's analysis of linear non-terminating systems was based on Hindley's lemma, stating that a non-terminating relation is confluent provided its local peaks are joinable in at most one step from each side [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF]. The more general analyses needed here have been made possible by van Oostrom's notion of decreasing diagrams for labelled relations.

Definition 1.

A labelled rewrite relation is a pair made of a rewrite relation → and a mapping from rewrite steps to a set of labels L equipped with a partial quasi-order whose strict part is well-founded. We write u → p,m R v for a rewrite step from u to v at position p with label m and rewrite system R. Indexes p, m, R may be omitted. We also write α l (resp. l α) if m l (resp. l m) for all m in a multiset α.

Given an arbitrary labelled rewrite step → l , we denote its projection on terms by →, its inverse by l ←, its reflexive closure by → = l , its symmetric closure by ↔ l , its reflexive, transitive closure by → → α for some word α on the alphabet of labels, and its reflexive, symmetric, transitive closure, called conversion, by ← ↔ → α . We may consider the word α as a multiset.

The triple v, u, w is said to be a

local peak if v l ← u → m w, a peak if v α ← ← u → → β w, a joinability diagram if v → → α u β ← ← w. The local peak v p,m l→r ← u → q,n g→d w is a disjoint, critical, ancestor peak if p#q, q ∈ p•FPos(l), q > p•FPos(l), respectively. The pair v, w is convertible if v ← ↔ → α w, divergent if v α ← ← u → → β w for some u, and joinable if v → → α t β ← ← w for some t. The relation → is locally confluent (resp. confluent, Church-Rosser) if every local peak (resp. divergent pair, convertible pair) is joinable.
Given a labelled rewrite relation → l on terms, we consider specific conversions associated with a given local peak called local diagrams and recall the important subclass of van Oostrom's decreasing diagrams and their main property: a relation all whose local diagrams are decreasing enjoys the Church-Rosser property, hence confluence. Decreasing diagrams were introduced in [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF], where it is shown that they imply confluence, and further developed in [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams converted[END_REF]. The first version suffices for our needs.

Definition 2 (Local diagrams).

A local diagram D is a pair made of a local peak D peak = v ← u → w and a conversion D conv = v ← ↔ → w. We call diagram rewriting the rewrite relation ⇒ D on conversions associated with a set D of local diagrams, in which a local peak is replaced by one of its associated conversions:

P D peak Q ⇒ D P D conv Q for some D ∈ D Definition 3 (Decreasing diagrams [28]). A local diagram D with peak v l ← u → m w is decreasing if its conversion D conv = v → → α s → = m s → → δ δ ← ← t l =
← t β ← ← w satisfies the following decreasingness condition: labels in α (resp. β) are strictly smaller than l (resp. m), and labels in δ, δ are strictly smaller than l or m. The rewrites s → = m s and t l = ← t are called the facing steps of the diagram. This simple corollary of Theorem 4 is a reformulation of van Oostrom's decreasing diagram theorem which is convenient for our purpose.

Sub-rewriting

Consider the following famous system inspired by an abstract example of Newman, algebraized by Klop and publicized by Huet [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF], NKH = {f (x, x) → a, f (x, c(x)) → b, g → c(g)}. NKH is overlap-free, hence locally confluent by Huet's lemma [START_REF] Gérard | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF]. However, it enjoys non-joinable non-local peaks such as a ← f (g, g) → f (g, c(g)) → b.

The main difficulty with NKH is that non-joinable peaks are non-local. To restore the usual situation for which the confluence of a relation can be characterized by the joinability of its local peaks, we need another rewrite relation whose local peaks capture the non-confluence of NKH as well as the confluence of its confluent variations. A major insight of [START_REF] Liu | Confluence by critical pair analysis[END_REF] is that this can be achieved by the sub-rewriting relation, that allows us to rewrite f (g, c(g)) in one step to either a or b, therefore exhibiting the pair a, b as a sub-rewriting critical pair. Sub-rewriting is made of a preparatory equalization phase in which the variable instances of the lefthand side l of some rule l → r are joined, taking place before the rule is applied in the firing phase. In [START_REF] Liu | Confluence by critical pair analysis[END_REF], sub-rewriting required a signature split to define layers in terms, the preparatory phase taking place in the lower layers. No a-priori layering is needed here: Definition 6 (Sub-rewriting). A term u sub-rewrites to a term v at p ∈ Pos(u) for some rule

l → r ∈ R, written u → p R R v, if u → → (>p•F Pos(l)) R u[lθ] p → p R u[rθ] p = v for some substitution θ. The term u| p is called a sub-rewriting redex.
This definition of sub-rewriting allows arbitrary rewriting below the lefthand side of the rule until a redex is obtained. This is the major idea of sub-rewriting, ensuring that R ⊆ R R ⊆ R * . A simple, important property of a sub-rewriting redex is that it is an instance of a linearized lefthand side of rule: Lemma 7 (Sub-rewriting redex). Assume u sub-rewrites to u[rσ] p with l → r at position p. Then u| p = lθ for some θ s.t. (∀x ∈ Var(l))

(∀p i ∈ Pos(l) s.t. l(p i ) = x) θ(x pi ) → → R σ(x).
We say that σ is an equalizer of l, and the rewrite steps from lθ to lσ are an equalization. Sub-rewriting differs from rewriting modulo by being directional. It differs from Klop's higher-order rewriting modulo developments [START_REF]Term rewriting systems[END_REF] used by Okui for first-order computations [START_REF] Okui | Simultaneous critical pairs and Church-Rosser property[END_REF], in that the preparatory phase uses arbitrary rewriting. Having non-left-linear rules with critical pairs at subterms seems incompatible with using developments. Sub-rewriting differs as well from relative rewriting [START_REF] Hirokawa | Decreasing diagrams and relative termination[END_REF] in that the preparatory phase must take place below variables. The latter condition is essential to obtain plain critical pairs based on plain unification.

Assuming that local sub-rewriting peaks characterize the confluence of NKH, we need to compute the corresponding critical pairs. Unifying the lefthand sides f (x, x) and f (y, c(y)) results in the conjunction x = y ∧ y = c(y) containing the occur-check equation y = c(y), which prevents unification from succeeding on finite trees but allows it to succeed on infinite rational trees: the critical peak has therefore an infinite overlap f (c ω , c ω ) and a finite critical pair a, b . At the level of infinite trees, we then have an infinite local rewriting peak a ← f (c ω , c ω ) = f (c ω , c(c ω )) → b, the properties of infinite trees making the sub-rewriting preparatory phase useless. Sub-rewriting therefore captures on finite trees some properties of rewriting on infinite trees, here the existence of a local peak. Computing the critical pairs of the sub-rewriting relation is therefore related to unification over finite trees resulting possibly in solutions over infinite rational trees. In the next section, we develop a novel view of unification that will allow us to capture both finite and infinite overlaps by finite means.

Cyclic unification

This section is adapted from [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Dershowitz | Rewrite systems[END_REF][START_REF] Jouannaud | Solving equations in abstract algebras: A rulebased survey of unification[END_REF] by treating finite and infinite unifiers uniformly: equality of terms is interpreted over the set of infinite rational terms when needed.

An equation is an oriented pair of finite terms, written u = v. A unification problem P is a (finite) conjunction ∧ i u i = v i of equations, sometimes seen as a multiset of pairs written u = v. A unifier (resp. a solution) of P is a substitution (resp., a ground substitution) θ such that (∀i) u i θ = v i θ. A unifier describes a generally infinite set of solutions via its ground instances. A major usual assumption, ensuring that solutions exist when unifiers do, is that the set T (F) of ground terms is non-empty. A unification problem P has a most general finite unifier mgu(P ), whenever a finite solution exists, which is minimal with respect to subsumption and unique up to variable renaming. Computing mgu(P ) can be done by the unifier-preserving transformations of Figure 1, starting with P until a solved form is obtained, ⊥ denoting the absence of solution, whether finite or infinite. Our notion of solved form therefore allows for infinite unifiers (and solutions) as well as finite ones:

Definition 8. Solved forms of a unification problem P different from ⊥ are unification problems S = x = u ∧ y = v such that (i) P = Var(P ) \ ( x ∪ y) is the set of parameters of S;
(ii) variables in x ∪ y (i.e. variables at lefthand sides of equations) are all distinct;

(iii

) (∀ x = u ∈ x = u), Var(u) ⊆ P; (iv) (∀ y = v ∈ y = v), Var(v) ⊆ P ∪ y, Var(v) ∩ y = ∅ and v ∈ X .
Equations y = v ∈ y = v are called cyclic (or occur-check, the vocabulary originating from [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF] used so far), x is the set of finite variables, and y is the set of (infinite) cyclic (or occur-check) variables. A solved form is a set of equations since x ∪ y is itself a set and an equation x = y between variables can only relate a finite variable x with a parameter y.

Remove s = s ∧ P → P Decomp f ( s) = f ( t) ∧ P → s = t ∧ P Conflict f ( s) = g( t) ∧ P → ⊥ if f = g Choose y = x ∧ P → x = y ∧ P if x ∈ V ar(P ), y ∈ Var(P ) Coalesce x = y ∧ P → x = y ∧ P {x → y} if x, y ∈ V ar(P ), x = y Swap u = x ∧ P → x = u ∧ P if u ∈ X Merge x = s ∧ x = t ∧ P → x = s ∧ s = t ∧ P if x ∈ X , 0 < |s| ≤ |t| Replace x = s ∧ P → x = s ∧ P {x → s} if x ∈ V ar(P ), x ∈ Var(s), s ∈ X Merep y = x ∧ x = s ∧ P → y = s ∧ x = s ∧ P if x ∈ V ar(s), s ∈ X , y ∈ Var(s, P )
and no other rule applies

Figure 1 Unification Rules Example 9 (NKH). f (x, x) = f (y, c(y)) → Decomp x = y ∧ x = c(y) → Coalesce x = y ∧ y = c(y) → Merep x = c(y) ∧ y = c(y). Alternatively, f (x, x) = f (y, c(y)) → Decomp x = y ∧ x = c(y) → Replace c(y) = y ∧ x = c(y) → Swap y = c(y) ∧ x = c(y).
Choose and Swap originate from [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF]. Replace and Coalesce ensure that finite variables (but parameters) do not occur in equations constraining the infinite ones. Merep is a sort of combination of Merge and Replace ensuring condition v ∈ X in Definition 8, item (iv). Unification over finite trees has another failure rule, called Occur-check, fired in presence of cyclic equations.

Theorem 10. Given an input unification problem P , the unification rules terminate, fail if the input has no solution, and return a solved form

S = x = u ∧ y = v otherwise.
Proof. Termination, characterization of solved forms, soundness, are all adapted from [START_REF] Jouannaud | Solving equations in abstract algebras: A rulebased survey of unification[END_REF].

Termination. Solved form. We show by contradiction that the output P , which is in normal form with respect to the unification rules, is a solved form in case Conflict never applies. First, P must be a conjunction of equations x = s, since otherwise Decomp or Swap would apply. Let P = Var(P ) \ ( x ∪ y).

Condition (i) is a definition. Condition (ii). Let P = x = s ∧ x = t ∧ P .
Either s or t is a variable, since otherwise Merge would apply. Assume without loss of generality that s ∈ X , call it y. If x = y, Remove applies. If y ∈ Var(t, P ), then Choose applies. Otherwise, Coalesce applies. Hence x, y are all different sets, and P is therefore itself a set. Let now x = u be a maximal (with respect to inclusion) set of equations in P such that Var( u) ⊆ P, and y = v be the remaining set of equations. Condition (iii). It is ensured by the definition of x = u. Condition (iv). Let y = v ∈ y = v. Let now x = u ∈ x = u, hence x ∈ Var(u). Assume x ∈ Var(v). If u ∈ X , then Replace applies. Otherwise, if u has no other occurrence in P , then Choose applies, else Coalesce applies. Therefore Var(v) ∩ x = ∅ by contradiction. Assume Var(v) ∩ y = ∅. Then Var(v) ⊆ P, which contradicts the maximality of x = u. We are left to show that v is not a variable. If it were, then v ∈ y. First, v = y, otherwise Remove applies. Let P = (y = v) ∧ P with v ∈ y \ {y}. Let v = z, there must exist (z = w) ∈ P for some w, otherwise z ∈ P. Hence P = (z = w) ∧ P . Now, y ∈ Var(w, P ), otherwise Coalesce applies. Then we show z ∈ Var(w): firstly, w = z, otherwise Remove applies; secondly, w is not a variable, otherwise w ∈ Var(y, P ) lets Choose apply, while w ∈ Var(y, P ) makes Coalesce available; then if z ∈ Var(w), Replace applies. Thus z ∈ Var(w), allowing Merep, which contradicts that we have indeed a solved form.

Soundness. The set of solutions is an invariant of the unification rules. This is trivial for all rules but Coalesce, Merge, Replace, Merep, for which it follows from the fact that substitutions are homomorphisms and equality is a congruence.

The solved form is a tree solved form if y = ∅, and otherwise an Ω solved form whose solutions are infinite substitutions taking their values in the set of infinite (rational) terms. We shall now develop our notion of cyclic unifier capturing both solved forms by describing the infinite unifiers of a problem P as a pair of a finite unifier σ and a set of cyclic equations E constraining those variables that require infinite solutions. In case E = ∅, then P is a tree solved form and σ = mgu(P ). To avoid manipulating infinite unifiers when E = ∅, we shall work with the cyclic equations themselves considered as a ground rewrite system. Definition 11 ([21]). Given a set of equations E, we denote by = cc E the equational theory in which the variables in Var(E) are treated as constants, also called congruence closure E.

We are interested in the congruence closure defined by cyclic equations, seen here as a set R of ground rewrite rules. We may sometimes consider R as a set of equations, to be either solved or used as axioms, depending on context. Definition 12. A cyclic rewrite system is a set of rules R = { y → v} such that the unification problem y = v is its own solved form with y as the set of infinite cyclic variables. Variables in R are treated as constants.

Lemma 13. A cyclic rewrite system R is ground and critical pair free, hence Church-Rosser.

We now introduce our definition of cyclic unifiers and solutions: Definition 14. A cyclic unifier of a unification problem P is a pair η, R made of a substitution η and a cyclic rewrite system R = { y → v}, satisfying: We shall use (iii.a) or (iii.b) indifferently, depending on our needs, by referring to (iii). The idea of cyclic unifiers is that the need for infinite values for some variables is encoded via the use of the cyclic rewrite system R, which allows us to solve the various occurcheck equations generated when unifying P . Finite variables are instantiated by the finite substitution η, which ensures that cyclic unification reduces to finite unification in the absence of infinite variables. The technical restrictions on Dom(η) and Ran(η) aim at making η idempotent. In (iii), parameters occurring in R are instantiated by η before rewriting takes place: cyclic unification is nothing but rigid unification modulo the cyclic equations in R [START_REF] Gallier | Theorem proving using rigid E-unification equational matings[END_REF]. Instantiation of the infinite variables y is delegated to cyclic solutions via the additional substitution ρ which may also instantiate the variables introduced by η. The set of cyclic unifiers of a problem P is closed under substitution instance, provided the variable conditions on its substitution part are met, as is the set of its unifiers. Cyclic unifiers have indeed many interesting properties similar to those of finite unifiers, of which we are going to investigate only a few which are relevant to the confluence of layered systems.

We now focus our attention on specific cyclic unifiers sharing a same cyclic rewrite system.

Definition 16. Given a unification problem P with solved form S = x = u ∧ y = v, let -its set of parameters P = Var(P ) \ ( x ∪ y), -its cyclic rewrite system R S = { y → v} and canonical substitution η S = { x → u}, -its S-based cyclic unifiers η, R S , among which η S , R S is said to be canonical.

We now show a major property of S-based cyclic unifiers, true for any solved form S:

Lemma 17. Given a unification problem with solved form S, the set of S-based cyclic unifiers is preserved by the unification rules.

Proof. The result is straightforward for Remove, Choose, and Swap. It is true for Decomp and Conflict since, using formulation (iii.b) of Definition 14, the rules in Rη cannot apply at the root of F-headed terms. Next comes Coalesce. We need to prove that η, R is a cyclic unifier for x = y ∧ P iff it is one for x = y ∧ P {x → y}. Let u = v ∈ P . For the only if case, we have u{x

→ y}η = uη{xη → yη} = cc Rη uη = cc Rη vη = cc Rη vη{xη → yη} = v{x → y}η.
The if case is similar. Replace is similar to Coalesce. Consider now Merge (Merep is similar). Showing that η, R is a cyclic unifier for x = s ∧ x = t ∧ P iff it is one for x = s ∧ s = t ∧ P is routine by using transitivity of the congruence closure = cc Rη .

We can now conclude: This result, which suffices for our needs, is easily lifted to cyclic solutions, as they are instances of a cyclic unifier. We can further prove that η S is more general than any S -based cyclic unifiers, for any solved form S of P . This is where our conditions on Ran(η) become important. We conjecture that it is most general among the set of all cyclic unifiers.

6

Layered systems

NKH is non-confluent, but can be easily made confluent by adding the rule a → b (giving NKH 1 ), or removing the rule g → c(g) (giving NKH 2 ). It can be made non-right-ground by making the symbols a, b unary (using a(c(x)) and b(c(x)) in the righthand sides of rules, giving NKH 3 ), or even non-right-linear by making them binary (giving NKH 4 ). There are classes of systems containing NKH for which it is possible to conclude its non-confluence. The following classes succeed for NKH 1 : simple-right-linear [START_REF] Toyama | Church-Rosser property and unique normal form property of non-duplicating term rewriting systems[END_REF], strongly depth-preserving [START_REF] Gomi | On the Church-Rosser property of root-E-overlapping and strongly depth-preserving term rewriting systems[END_REF], and relatively terminating [START_REF] Klein | Confluence of non-left-linear TRSs via relative termination[END_REF]. As for NKH 3 , it is neither simple-right-linear nor strongly depth-preserving: only [START_REF] Klein | Confluence of non-left-linear TRSs via relative termination[END_REF] can cover it. When it comes to NKH 4 , relative termination becomes hard to satisfy in presence of non-right-linearity [START_REF] Klein | Confluence of non-left-linear TRSs via relative termination[END_REF]. Our goal is to define a robust, Turing-complete class of rewrite systems capturing NKH and its variations, for which confluence can be analyzed in terms of critical diagrams. Definition 19. A rewrite system R is layered iff it satisfies the disjointness assumption (DLO) that linearized overlaps of some lefthand sides of rules upon a given lefthand side l can only take place at a multiset of disjoint or equal positions of FPos(l):

(DLO) := (∀l → r ∈ R) (∀p ∈ FPos(l)) (∀g → d ∈ R s.t. Var(l) ∩ Var(g) = ∅) (∀σ : Var(l| p , g) → T (F, X ) s.t. l| p σ = gσ) SOF(l| p ) ∧ SOF(g) SOF(u) := (∀q ∈ FPos(u)\{Λ}) OF(u| q ) OF(v) := (∀g → d ∈ R s.t. Var(v) ∩ Var(g) = ∅) (∀o ∈ FPos(v))(∀σ : Var(v, g) → T (F, X )) v| o σ = gσ
SOF stands for subterm overlap-free, and OF for overlap-free. In words, if two lefthand sides of rules in R overlap (linearly) a lefthand side l of a rule in R at positions p and q respectively, then either p = q or p#q. Overlaps at different positions along a path from the root to a leaf of l are forbidden. Layered systems is a decidable class that relates to overlay systems [START_REF] Dershowitz | Confluence of conditional rewrite systems[END_REF], for which overlaps computed with plain unification can only take place at the root of terms -hence their name-, and generalizes strongly non-overlapping systems [START_REF] Sakai | Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent[END_REF] which admit no linearized overlaps at all. All these classes are Turing-complete since they contain a complete class [START_REF] Willem | Term rewriting systems[END_REF].

Example 20. NKH is a layered system, which is also overlay. {h(f (x, y)) → a, f (x, c(x)) → b} is layered but not overlay. {h(f (x, x)) → a, f (x, c(x)) → b, g → c(g)} is layered, but not strongly non-overlapping. {f (h(x)) → x, h(a) → a, a → b} is not overlay nor layered: SOF(h(x)) succeeds while SOF(h(a)) fails, hence their conjunction fails.

Layering

We define the rank of a term t as the maximum number of non-overlapping linearized redexes traversed from the root to some leaf of t, which differs from the usual redex-depth. Definition 21. Given a layered rewrite system R, the rank rk(t) of a term t is defined by induction on the size of terms as follows:

-the maximal rank of its immediate subterms if t is not a linearized redex ; otherwise, -1 plus max{rk(σ) : (∃l → r ∈ R) t = lσ}, where rk(σ) := max{rk(σ(x)) : x ∈ Var(l)}.

Definition 22.

A rewrite system R is rank non-increasing if for all terms u, v such that u → R v, then rk(u) ≥ rk(v).

The rewrite system {f (x) → c(f (x))} is rank non-increasing while {f (x) → f (f (x))} is rank increasing. The system {f ib(0) → 0, f ib(S(0)) → S(0), f ib(S(S(x))) → f ib(S(x)) + f ib(x)} calculating the Fibonacci function is rank non-increasing. NKH is rank non-increasing. The coming decidable sufficient condition for rank non-increasingness captures our examples (but Fibonacci, for which an even more complex decidable property is needed):

Lemma 23. A layered rewrite system R is rank non-increasing if each rule g → d in R satisfies the following properties: (i) ((∀l → r ∈ R)(∀l → r ∈ R) s.t. Var(d), Var(l), Var(l ) are pairwise disjoint) (∀p, q ∈ FPos(d) s.t. q > p • F Pos(l)) (∀σ : Var(g, l, l ) → T (F)) (d| p σ = lσ) ∨ (d| q σ = l σ) ; (ii) ((∀l → r ∈ R) s.t. Var(g) ∩ Var(l) = ∅)(∀p ∈ FPos(l) \ Λ) (∀σ : Var(g, l) → T (F) s.t. dσ = l| p σ) ((∃l → r ∈ R) s.t. Var(l ) ∩ Var(g, l) = ∅)(∃x ∈ Var(l, l , g)) l[x] p • ≥ l .
Corollary 29. Let l → r, g → d ∈ R and p ∈ FPos(l) such that Var(l) ∩ Var(g) = ∅, and l| p θ = gθ are terms in T n+1 . Then, unification of l| p = g succeeds, returning a solved form S s.t., for each z = s ∈ S, Conv θ n (z,s), OF(s), Equalize n (s) θ σ for all σ satisfying (lθ → → (>F Pos(l)) lσ) ∧ (gθ → → (>F Pos(g)) gσ), and further, SOF(l| p η S )∧SOF(gη S ).

Proof. Unification applies first Decomp. Conclude by Lemmas 27 and Corollary 25.

Corollary 30. Assume t = lσ for some l → r ∈ R. Then, rk(t) = 1 + rk(σ).

Proof. Let t = l i σ i = l i θγ (note that γ does not depend on i), where θ = mgu(= i l i ). Then, rk(t) = 1 + max i {rk(σ i )} = 1 + max i {rk(θγ)} = 1 + rk(γ) = 1 + rk(σ i ) since θ satisfies OF at all non-variable positions by Lemma 27.

Example 31 (NKH). Consider f (c(g), c(g)) of rank 2, using either linearized lefthand side f (x 1 , x 2 ) or f (y 1 , c(y 2 )) to match f (c(g), c(g)). Corresponding substitutions have 1.

A major consequence is that the preparatory phase of sub-rewriting operates on terms of a strictly smaller rank. This would not be true anymore, of course, with a conversion-based preparatory phase. More generally, we can also show that the rank of terms does not increase -but may remain stable-when taking a subterm, a property which is not true of non-layered systems. Consider the system {f (g(h(x))) → x, g(x) → x, h(x) → x}. The redex f (g(h(a))) has rank 1 with our definition, but its subterm g(h(a)) has rank 2.

Testing confluence of layered systems via their cyclic critical pairs

Since R is rank non-increasing we shall prove confluence by induction on the rank of terms. Since rewriting is rank non-increasing, the set of T n -conversions is closed under diagram rewriting, hence allowing us to use Corollary 5. This is why we adopted this restricted, but complete, form of decreasing diagram rather than the more general form described in [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams converted[END_REF].

Definition 32 (Cyclic critical pairs). Given a layered rewrite system R, let l → r, g → d ∈ R and p ∈ FPos(l) such that Var(l) ∩ Var(g) = ∅, and l| p = g is unifiable with canonical cyclic unifier η

S = { x → u}, R S = { y → v} . Then, rη S R ← lη S = cc R S η S l[g] p η S → R l[d] p η S
is a cyclic critical peak, and rη S , l[d] p η S is a cyclic critical pair, which is said to be realizable by the substitution θ iff (∀y

→ v ∈ R S ) yθ → → R R ← ← vθ.
The relationship between critical peaks and realizable cyclic critical pairs, usually called critical pair lemma, is more complex than usual:

Lemma 33 (Cyclic critical pair lemma). Let l → r, g → d ∈ R such that Var(l) ∩ Var(g) = ∅. Let rσ Λ l→r ← lσ (>F Pos(l)) ← ← lθ = lθ[gθ] p → → (>p•F Pos(g)) lθ[gσ] p → p g→d lθ[dσ]
p be a subrewriting local peak in T n+1 , satisfying p ∈ FPos(l) and Var(lθ) ∩ Var(l, g) = ∅. Assume further that R is Church-Rosser on the set T n . Then, there exists a cyclic solution γ, R S such that S is a solved form of the unification problem l| p = g, γ = η S ρ for some ρ of domain included in Var(l, g), σ → → R γ, and R S is realizable by γ.

Proof. Corollary 29 asserts the existence of a solved form S = x = u ∧ y = v of the problem l| p = g. But σ, R S may not be a cyclic solution. We shall therefore construct a new substitution γ such that σ → → R R γ and γ, R S is a cyclic solution of the problem, obtained as an instance by some substitution ρ of the most general cyclic unifier η S , R S by Theorem 18.

The construction of γ has two steps. The first aims at forcing the equality constraints given by S. This step will result in each parameter having possibly many different values. The role of the second step will be to construct a single value for each parameter.

We start equalizing independently equations z = s ∈ S. Since Equalize n (z j ) θ σ , Equalize n (s) θ σ and Conv θ n (z j ,s), zσ and sσ are n-convertible by Lemma 26. By assumption, zσ and sσ are joinable, hence there exists a term t s z such that zσ → → R t s z R ← ← sσ. Since OF(s) by Corollary 29, the derivation from sσ to t s z must occur at positions below FPos(s). Maintaining equalities in sσ between different occurrences of each variable in Var(s), we get t s z = sτ s z for some τ s z . For each parameter p, pσ → → R pτ s z , hence the elements of the non-empty set {pτ s z : p ∈ Var(s) for some z = s ∈ S} are n-convertible thanks to rank non-increasingness. By our Church-Rosser assumption, they can all be rewritten to a same term t p . We now define γ:

(i) parameters. Given p ∈ P, we define

γ(p) = t p . By construction, pσ → → R t p = pγ. (ii) finite variables. Given x = u ∈ x = u, let γ(x) = uγ |P , thus xγ = uγ. By construction, xσ → → R uτ u x → → R uγ, hence xσ → → R xγ. (iii) cyclic variables. Given y = v ∈ x = u, let γ(y) = yσ, making yσ → → R yγ trivial.
(iv) variables in Var(l, g) \ Var(l| p , g), that is, those variables from the context l[•] p which do not belong to the unification problem l| p = g, hence to the solved form S. Given z ∈ Var(l, g) \ Var(l| p , g), let γ(z) = zσ, making zσ → → R zγ trivial.

Therefore σ → → R γ. We proceed to show γ, R S is a cyclic solution of l| p = g. Take ρ = γ| ¬ x . It is routine to see γ = η S ρ, and to check that η S , R S is a cyclic unifier of S by Definition 14, hence of l| p = g by Lemma 17. Hence the statement.

We end up the proof by noting that γ is a realizer of R S .

In case of NKH, the lemma is straightforward since solved forms have no parameters.

Our proof strategy for proving confluence of layered systems is as follows: assuming that n-convertible terms are joinable, we show that (n + 1)-convertible terms are (n + 1)-joinable by exhibiting appropriate decreasing diagrams for all their local peaks. To this end, we need to define a labelling schema for sub-rewriting. Assuming that rules have an integer index, different rules having possibly the same index, a step u → p R R v with the rule l i → r i is labelled by the pair rk(u| p ), i . Pairs are compared in the order = (≥ N , ≥ N ) lex whose strict part is well-founded. Indexes give more flexibility (shared indexes give even more) in finding decreasing diagrams for critical pairs, this is their sole use.

Definition 34. Let l → i r, g → j d ∈ R and p ∈ FPos(l) such that l| p = g has a solved form S. Then, the cyclic critical pair rη S , l [d]

p η S has a cyclic-joinable decreasing diagram if rη S → → 1,I R s = cc R S η S t 1,J R ← ← l[d] p η S ,
whose sequences of indexes I and J satisfy the decreasing diagram condition, with the additional condition, in case Var(l[•] p ) = ∅, that all steps have a rule index k < i.

By Corollary 29, the ranks of lη S and l[g] p η S are 1. Thanks to rank non-increasingness and Definition 21, the cyclic-joinable decreasing diagram -but the congruence closure partis made of terms of rank 1 except possibly s and t which may have rank 0. It follows that all redexes rewritten in the diagram have rank 1. The decreasing diagram condition is therefore ensured by the rule indexes, which justifies our formulation.

Note further that the condition Var(l[•] p ) = ∅ is automatically satisfied when p = Λ, hence no additional condition is needed in case of a root overlap. In case where Var(l[•] p ) = ∅, implying a non-root overlap, the additional condition aims at ensuring that the decreasing diagram is stable under substitution. It implies in particular that there exists no i-facing step. This may look restrictive, and indeed, we are able to prove a slightly better condition: (i) there exists no i-facing step, and (ii) each step u → q k v using rule k at position q satisfies k < i or Var(u| q ) ⊆ Var(gη S ). We will restrict ourselves here to the simpler condition which yields a less involved confluence proof.

We can now state and prove our main result: Theorem 35. Rank non-increasing layered systems are confluent provided their realizable cyclic critical pairs have cyclic-joinable decreasing diagrams.

Proof. Since → R ⊆ → R R ⊆ → → R ,
R-convertibility and R R -convertibility coincide. We can therefore apply van Oostrom's theorem to R R -conversions, and reason by induction on the rank. We proceed by inspection of the sub-rewriting local peaks v p (l→r) R ← u → q (g→d) R w, with Var(l) ∩ Var(g) = ∅. We also assume for convenience that Var(l, g) ∩ Var(u, v, w) = ∅. This allows us to consider u, v, w as ground terms by adding their variables as new constants. We assume further that variables x, y ∈ Var(l, g) become linearized variables x i , y j in l, g, and that ξ is the substitution such that ξ(x i ) = x and ξ(y j ) = y, hence implying Var(l)∩Var(g) = ∅.

By definition of sub-rewriting, u| p = lθ → →

(>F Pos(l)) R v | p = lσ and v = u[rσ] p ,
where for all positions o ∈ Pos(l) such that l| o = x and l| o = x i , then

x i θ → → R xσ. Similarly, u| q = gθ → → (>F Pos(g)) R
w | q = gσ and w = u[dσ] q , where for all positions o ∈ Pos(g) such that g| o = y and g| o = y j , then y j θ → → R yσ. There are three cases:

1. p#q. The case of disjoint redexes is as usual. 2. q > p • F Pos(l), the so-called ancestor peak case, for which sub-rewriting shows its strength. W.l.o.g. we assume u| p has some rank n + 1 and note that u| q has some rank m ≤ n by Corollary 30. Since the sub-rewriting steps from u to w occur strictly below p • FPos(l), then q = p • o • q where l| o = ξ(y j ) and l| o = y j . It follows that w = lτ for some τ which is equal to θ for all variables in l except y j for which τ (y j ) = θ(y j )[dσ] q . We proceed as follows: we equalize all n-convertible terms {xσ : x ∈ Var(r)} in v and {yτ : y ∈ Var(l)} in w by induction hypothesis, yielding s, t. Note that steps from v to s have ranks strictly less than the rank n + 1 of the step u → R R v by Corollary 30 and rank non-increasingness. Then, t is an instance of l by some γ, and s is the corresponding instance of r, hence t rewrites to s with l → r. The equalization steps from w to t have ranks which are not guaranteed to be strictly less than m, hence cannot be kept to build a decreasing diagram. But they can be absorbed in a sub-rewriting step from w to s whose first label is at most n + 1, hence faces the step from u → R R v: sub-rewriting allows us to rewrite directly from w to s, short-cutting the rewrites from w to t that would otherwise yield a non-decreasing diagram. The proof is depicted at Figure 2 (left), assuming p = Λ for simplicity. Black color is used for the given sub-rewriting local peak, blue for arrows whose redexes have ranks at most n + 1, and red when redex has rank at most n. 3. q ∈ p • F Pos(l), the so-called critical peak case, whose left and right rewrite steps have labels n + 1, i and m, j respectively, with rules l → r and g → d having indexes i and j. Assuming without loss of generality that p = Λ, the proof is depicted at Figure 2 (right). Most technical difficulties here originate from the fact that the context l[•] q may have variables. In this case, we first rewrite w to t = lσ[dσ] q = l[d] q σ by replaying those equalization steps, of rank at most n, used in the derivation from u to v , which apply to variable positions in Var(l[•] q ). Now, since lθ = lθ[gθ] q , by Lemma 33, there is a substitution γ and a solved form S of the unification problem l| q = g, such that σ → → R γ, γ = η S ρ for some ρ, and R S is realizable by γ. By assumption, the cyclic critical pair rη S , l [d] q η S has a cyclic-joinable decreasing diagram (modulo = cc R S η S ). We can now lift this diagram to the pair s, t by instantiation with the substitution ρ. The congruence closure used in the lifted diagram becomes therefore = cc R S η S ρ . We are left showing that the obtained diagram for the pair v, w is decreasing with respect to the local peak v ← u → w. The assumption that I, J satisfy the decreasing diagram condition for the critical peak ensures that these rewrites do satisfy the decreasing diagram condition with respect to the local peak v ← u → w as well. b. Var(l[•] q ) = ∅. By Corollary 30, the right equalization steps w → →t → →t have redexes of rank at most n, making their labels strictly smaller than n + 1, i . Consider now the middle part. Thanks to rank non-increasingness and the additional condition on the cyclic-joinability assumption of the cyclic critical pair, all labels n , k in the middle part satisfy n ≤ n + 1 and k < i, hence are strictly smaller than n + 1, i .

u = lθ C C v = lσ c x n + 1 v = rσ s m ≤ n w = lτ Ancestor peak c c ≤ n s = rγ c c t = lγ ' W ≤ n + 1 u = lθ = lθ[gθ] q C C v = lσ c n + 1 v = rσ s s w = lθ[gσ] q c C m ≤ n + 1 w = lθ[dσ] q Critical peak lη S = cc RS ηS l[g]qη S © d d rη S l[d]qη S r r r r j r r r j % % = cc R S η S c c s = rγ c c t = l[d] q σ c c t = l[d] q γ r r r r r j r r r r r j % % = cc R S η S ρ d d d d © ©
We are left with the congruence closure steps. Given

y = v ∈ R S , yγ → → R R ← ← vγ since R S
is realizable by γ. By Lemma 27, OF(v) holds, hence yγ and vγ are n-convertible by rank non-increasingness. We are left with replacing the = cc yγ= vγ -steps by a joinability diagram whose all steps have rank at most n. The obtained diagram is therefore decreasing, which ends the proof.

Using the improved condition of cyclic-joinability mentioned after Definition 34 requires modifying the discussion concerning the (green-)middle-part rewrite steps. Although this does not cause any conceptual difficulties, it is technically delicate. The interested reader can of course reconstruct this proof for himself or herself.

Our result gives an answer to NKH: confluence of critical pair free rewrite systems can be analyzed via their sub-rewriting critical pairs, which are actually the cyclic critical pairs. NKH is critical pair free but non-confluent. Indeed, it has the Ω solved form x = c(y) ∧ y = c(y) obtained by unifying f (x, x) = f (y, c(y)). The cyclic critical peak is then a ← f (x, x) = cc f (y, c(y)) → b yielding the cyclic critical pair a, b which is not joinable modulo {x = c(y), y = c(y)}.

We now give a slight modification of NKH making it confluent:

Example 36. The system R = {f (x, x) → 2 a(x, x), f (x, c(x)) → 2 b(x), f (c(x), c(x)) → 3 f (x, c(x)), a(x, x) → 1 e(x), b(x) → 1 e(c(x)), g → 0 c(g)} is confluent. Showing that R satisfies (DLO)
is routine, and it is rank non-increasing by Lemma 23. There are three cyclic critical pairs, which all have a cyclic-joinable decreasing diagram. For instance, the unification f

(x, x) = f (y, c(y)) returns a canonical cyclic unifier η S = ∅, R S = {x → c(y), y → c(y)} , the corresponding cyclic critical peak a(x, x) 1,2 ← f (x, x) = cc R S η S f (y, c(y)) → 1,2 b(y) has a cyclic-joinable decreasing diagram a(x, x) → 1,1 e(x) = cc R S η S e(c(y)) 1,1 ← b(y). The unification f (x, x) = f (c(y), c(y)) returns η S = {x = c(y)}, R S = ∅ , the correspond- ing (normal) critical peak a(c(y), c(y)) 1,2 ← f (c(y), c(y)) → 1,3 f (y, c(y)) decreases by a(c(y), c(y)) → 1,1 e(c(y)) 1,1 ← b(y) 1,2 ← f (y, c(y)). By Theorem 35, R is confluent.
Theorem 35 can be easily used positively: if all cyclic critical pairs have cyclic-joinable decreasing diagrams, then confluence is met. This was the case in Example 36. But there is another positive use that we illustrate now: showing that {f (x, x) → a, f (x, c(x)) → b, g → d(g)} is confluent requires proving that the cyclic critical pair given by unifying the first two rules is not realizable. Although realizability is undecidable in general, this is the case here since there is no term s convertible to c(s). Theorem 35 can also be used negatively by exhibiting some realizable cyclic critical pair which is not joinable: this is the case of example NKH. In general, if some realizable cyclic critical pair leading to a local peak is not joinable, then the system is non-confluent. Whether a realizable cyclic critical pair always yields a local peak is still an open problem which we had no time to investigate yet.

A main assumption of our result is that rules may not increase the rank. One can of course challenge this assumption, which could be due to the proof method itself. The following counter-example shows that it is not the case.

Example 37. Consider the critical pair free system R = {d(x, x) → 0, f (x) → d(x, f (x)), c → f (c)}, which is layered but whose second rule is rank increasing since d(x 1 , x 2 ) unifies with d(y, f (y)). This system is non-confluent, since f (f c) → d(f c, f f c) → d(f f c, f f c) → 0 while f (f c) → f (d(c, f c)) → f (d(f c, f c)) → f 0 which generates the regular tree language {S → d(0, S), S → f 0} not containing 0. Note that replacing the second rule by the right linear rule f (x) → d(x, f (c)) yields a confluent system [START_REF] Sakai | Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent[END_REF].

Releasing rank non-increasingness would indeed require strengthening another assumption, possibly imposing left-or right-linearity.

Conclusion

Decreasing diagrams opened the way for generalizing Knuth and Bendix's critical-pair test for confluence to non-terminating systems, re-igniting these questions.

Our results answer open problems by allowing non-terminating rules which can also be non-linear on the left as well as on the right. The notion of layered systems is our first conceptual contribution here. Another, technical contribution of our work is the notion of sub-rewriting, which can indeed be compared to parallel rewriting. Both relations contain plain rewriting, and are included in its transitive closure. Both can therefore be used for studying confluence of plain rewriting. Tait and Martin-Löf's parallel rewriting -as presented by Barendregt in his famous book on Lambda Calculus [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics[END_REF]-has been recognized as the major tool for studying confluence of left-linear non-terminating rewrite relations when they are not right-linear. We believe that sub-rewriting will be equally successful for studying confluence of non-terminating rewrite relations that are not left-linear. In the present work where no linearity assumption is made, assumption (DLO) ensuring the absence of stacked critical pairs in lefthand sides makes the combined use of sub-rewriting and parallel rewriting superfluous. Without that assumption, as is the case in [START_REF] Liu | Confluence by critical pair analysis[END_REF], their combined use becomes necessary.

A last contribution, both technical and conceptual, is the notion of cyclic unifiers. Although their study is still preliminary, we have shown that they constitute a powerful new tool to handle unification problems with cyclic equations in the same way we deal with unification problems without cyclic equations, thanks to the existence of most general cyclic unifiers which generalize the usual notion of mgu. This indeed opens the way to a uniform treatment of problems where unification, whether finite or infinite, plays a central role.

Our long-term goal goes beyond improving the current toolkit for carrying out confluence proofs for non-terminating rewrite systems. We aim at designing new tools for showing confluence of complex type theories (with dependent types, universes and dependent elimination rules) directly on raw terms, which would ease the construction of strongly normalizing models for typed terms. Since redex-depth, the notion of rank used here, does not behave well for higher-order rules, appropriate new notions of rank are required in that setting.

Theorem 4 (Corollary 5 .

 45 [START_REF] Jouannaud | Diagrammatic confluence and completion[END_REF]). The relation ⇒ D terminates for any set D of decreasing diagrams. Assume that T ⊆ T (F, X ) and D is a set of decreasing diagrams in T such that the set of T -conversions is closed under ⇒ D . Then, the restriction of → to T is Church-Rosser if every local peak in T has a decreasing diagram in D.

  (i) Dom(η) ⊆ Var(P ) \ y, Ran(η) ∩ y = ∅, and Ran(η) ∩ Dom(η) = ∅ ; (ii) P and P ∧ R have identical sets of solutions ; and (iii.a) (∀u = v ∈ P ) uη = cc Rη vη, or equivalently by Lemma 13, (iii.b)(∀u = v ∈ P ) uη → → Rη Rη ← ← vη .A cyclic solution of P is a pair ηρ, R made of a cyclic unifier η, R of P and an additional substitution ρ.

Example 15 .

 15 Consider the equation f (x, z, z) = f (a, y, c(y)). A cyclic unifier is {x → a}, {y → c(z), z → c(z)} , and a cyclic solution is {x → a, y → a, z → c(a)}, {y → c(z), z → c(z)} ,which is clearly an instance of the former by the substitution {y → a, z → c(a)}. For the former, f (a, z, z) = cc {y=c(z),z=c(z)} f (a, y, c(y)). Another cyclic unifier is {x → a}, {z → c(y), y → c(y)} , for which f (a, z, z) = cc {z=c(y),y=c(y)} f (a, y, c(y)).

Theorem 18 .

 18 Given a unification problem P with solved form S = x = u ∧ y = v, the canonical S-based cyclic unifier is most general among the set of S-based cyclic unifiers of P . Proof. Let η, R S be a cyclic unifier of P based on S. Let x = u ∈ x = u. By definition of cyclic unification, xη → → R S η R S η ← ← uη. By definition of a solved form and cyclic unifiers, we have: Var(xη, uη) ⊆ ( x ∪ P ∪ Ran(η)), ( x ∪ P) ∩ y = ∅, Ran(η) ∩ y = ∅, and y ∩ Dom(η) = ∅. Therefore, xη and uη are irreducible by R S η. Hence xη = uη. Since xη S = u, it follows that xη = uη = (xη S )η = x(η S η).Let now z ∈ Var(P ) \ x. Since z ∈ Dom(η S ), then η(z) = zη = (zη S )η = z(η S η). Therefore, η = η S η and we are done.

Figure 2

 2 Figure 2 Ancestor and Critical Peaks

  The quadruple nu, |P |, nvre, nvle is used to interpret a unification problem P , where nu is the number of unsolved variables (0 for ⊥), where a variable x is solved in x = s∧P if x ∈ Var(s, P ); -|P | is the multiset (∅ for ⊥) of natural numbers {max(|s|, |t|) : s = t ∈ P } ; nvle (resp. nvre) is the number of equations in P whose lefthand (resp., righthand) side is a variable and the other side is not. Remove, Decomp and Conflict decrease |P | without increasing nu. Choose and Coalesce both decrease nu. Swap decreases nvre without increasing nu and |P |. Merge decreases nvle without increasing nu, |P | and nvre. Replace decreases nu. Now, when Merep applies, no other rule can apply, and we can check that no rules can apply either after Merep (except another possible application of Merep). This can happen only finitely many times, by simply reasoning on the number of equations whose both sides are variables.

We can now index term-related notions by the rank of terms. Let T n (F, X ) (in short, T n ) be the set of terms of rank at most n. Two terms in T n are n-convertible (resp. n-joinable) if their R-conversion (resp. R-joinability) involves terms in T n only.

Acknowledgment: This research is supported in part by NSFC Programs (No. 91218302, 61272002) and MIIT IT funds (Research and application of TCN key technologies) of China, and in part by JSPS, KAKENHI Grant-in-Aid for Exploratory Research 25540003 of Japan.

Closure properties

Call a term u an OF-term if u satisfies OF(u), and a substitution an OF-substitution if it maps variables to OF-terms. OF-terms enjoy several important closure properties. Given two substitutions θ, σ and rank n, let Conv θ n (u,v) iff uθ and vθ are n-convertible, and Equalize n (u) θ σ iff uθ → → R R uσ with terms of rank at most n.

Lemma 24. For all OF-terms u and substitutions γ, uγ cannot sub-rewrite at a position p ∈ FPos(u).

Assume further that n-convertible terms are joinable. Then, unification of P succeeds, and returns a solved form whose all equations satisfy these five properties.

In this lemma and coming proof, we assume that linearizations are propagated by the unification rules, implying in particular that u| p = u| p . P defines the initial linearization.

Proof. We show that these five properties are invariant by the unification rules. The claim follows since the unification rules terminate. We use notations of Figure 1.

Remove, Choose, Swap are straightforward. Decomp. By assumption, Conv θ n (f ( s),f ( t)), hence f ( s)θ and f ( t)θ are joinable by using terms of rank at most n, since R is rank non-increasing. By assumption OF(f ( s)) and OF(f ( t)), hence no rewrite can take place at the root. The result follows. Conflict. By the same token, f = g, a contradiction.

y) → Swap y = c(y) ∧ x = c(y). Successive linearizations yield f (x 1 , x 2 ) = f (y 1 , c(y 2 )), x 1 = y 1 ∧ x 2 = c(y 2 ), c(y 2 ) = y 1 ∧ x 2 = c(y 2 ) and y 1 = c(y 2 ) ∧ x 2 = c(y 2 ). The announced properties of the solved form can be easily verified.