PaperlayerView exact revision on arXiv

Source-linked AI summary

A new method for proving confluence on abstract reduction systems --- Confluence of non-E-overlapping weakly-shallow TRSs ---

Masahiko Sakai, Mizuhito Ogawa, Michio Oyamaguchi

arXiv:2610.09572v1cs.LO

TL;DR

Confluence is undecidable for general TRSs, and confluence of non-E-overlapping right-linear TRSs remains conjectural. The paper develops a finite-graph method for proving confluence and shows that weakly shallow, non-E-overlapping TRSs are confluent, including collapsing systems.

  • Problem

    Confluence is undecidable even for flat TRSs, and whether non-E-overlapping right-linear TRSs are confluent remains an open conjecture.

    Source: §1 · p. 2

  • Method

    The paper abstracts a finite reduction-graph construction into an ARS framework using compatibility and edge commutativity to expand graphs toward confluence.

    Source: §1 · p. 3

  • Results

    Weakly shallow, non-E-overlapping TRSs are confluent, removing the earlier non-collapsing restriction.

    Source: §1 · pp. 3, 5

  • Takeaways & Limitations

    Combining weak shallowness with the decidable non-ω-overlapping condition gives a decidable sufficient condition for confluence.

    Source: §10 · p. 63

    The result requires weak shallowness on both sides of every rule; relaxing this to right weakly-shallow TRSs remains a future direction.

    Source: §10 · p. 64

Abstract

from arXiv · show

This paper proposes a new method for proving the confluence of an abstract reduction system (ARS) by clarifying the sufficient conditions, called compatibility and edge commutativity, for expanding a given finite sub-ARS into a confluent one by adding rewrite edges. This method can be regarded as an extension of our earlier work, which showed that a weakly non-overlapping, shallow, and non-collapsing term rewriting system (TRS) is confluent. Furthermore, we apply our method to demonstrate that a non-$E$-overlapping and weakly shallow TRS is confluent. Here, a term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a TRS is weakly shallow if both sides of all its rewrite rules are weakly shallow. This drops the non-collapsing condition assumed in our previous work on weakly shallow TRSs. Moreover, since a weakly shallow TRS is non-$E$-overlapping whenever it is non-$\omega$-overlapping, and the latter property is decidable, we also obtain a decidable sufficient condition for confluence: non-$\omega$-overlapping and weakly shallow TRSs are confluent.

1 Introduction

The paper develops a graph-based framework for proving confluence in abstract reduction systems and applies it to show that weakly shallow, non-E-overlapping TRSs are confluent, without a non-collapsing restriction. This addresses an open confluence problem for non-E-overlapping right-linear TRSs through a different approach from well-founded measures.

1 Introduction

  • Confluence is undecidable even for flat TRSs, while non-E-overlapping right-linear TRSs are the subject of an open confluence conjecture.The strongest partial solution described is for simple right-linear TRSs.Source: §1 · p. 2
  • A key difficulty in the right-linear setting is that eager inner reductions may continue indefinitely, obstructing well-founded-measure arguments.The paper instead controls inner reductions by bounding them within a finite set of terms.Source: §1 · p. 3
  • The framework expands a finite reduction graph by adding rewrite edges, abstracting the construction beyond term rewriting systems to abstract reduction systems.The approach builds on reduction graphs and keeps the graph finite throughout the construction.Source: §1 · p. 3
  • Weakly shallow and non-E-overlapping TRSs are confluent, removing the non-collapsing restriction of the earlier result.The paper also presents the result as extending the CSI criterion to collapsing TRSs.Source: §1 · pp. 3, 5
  • Weak shallowness restricts defined symbols to roots or ground subterms, enabling a bottom-up construction without requiring right-linearity.The earlier result used weak shallowness with non-E-overlap and non-collapsing; the present work abstracts parts of its proof to make the argument clearer.Source: §1 · pp. 3–4
  • Non-ω-overlap is a decidable sufficient condition for non-E-overlap, yielding a decidable sufficient confluence criterion when combined with weak shallowness.Strong non-overlap is another decidable sufficient condition for non-E-overlap, but is stronger than non-ω-overlap.Source: §1 · pp. 3–4

2 Overview and intuition: A new method to prove confluence

The paper turns confluence into construction of a finite confluent reduction graph, then abstracts that construction to ARSs and applies it to broader classes of TRSs. The overview develops the induction scheme and the conditions needed to normalize edges, including for collapsing rules and systems beyond shallowness.

2 Overview and intuition: A new method to prove confluence

  • For each divergent sequence, the method constructs a finite confluent subgraph containing it, making confluence a finite-graph property whose construction terminates by finiteness.The framework abstracts reduction graphs to ARSs and then instantiates the construction for non-E-overlapping, weakly shallow TRSs.Source: §2 · pp. 5–6

2.1 The construction in the former approach

  • The earlier construction lifts a confluent direct-subterm graph, then replaces a root edge with one starting from a normal form, preserving confluence.For R3, adding the original root edge creates distinct terminal vertices, while the normalized edge joins them.Source: §2.1 · pp. 6–7

2.2 The claim CP and the induction scheme

  • The induction scheme builds a direct-subterm graph, applies the induction hypothesis, then recovers root edges through normalization and expansion; expansions can destroy termination, so pseudo-normal forms replace normal forms.The construction drops termination and keeps the original graph included in the extension.Source: §2.2 · pp. 7–8

2.3 Compatibility and edge commutativity

  • Edge commutativity lets a root edge survive reductions of its source, while compatibility makes targets joinable within each component so one normalization per component suffices.The non-root graph must be confluent and supply enough edges to keep subterms at nonlinear variable positions in balance.Source: §2.3 · pp. 8–9

2.4 Extending the class, I: collapsing rules

  • Collapsing rules can expose subterms, so the construction uses subterm-closedness and relative compatibility and edge commutativity, with non-collapsing root edges as the auxiliary relation.Redundant collapsing edges are trimmed before the relative edge-commutativity condition is obtained.Source: §2.4 · p. 9

2.5 Extending the class, II: beyond shallowness

  • Beyond shallowness, a pseudo-normal form need not be a redex, and edge expansions can disrupt earlier normalizations; a decreasing measure proves the process terminates.Reversing the favorable order of two non-collapsing, non-shallow edge normalizations requires one additional step.Source: §2.5 · pp. 9–10

2.6 Organization of the paper

  • The final sections instantiate the ARS result for non-E-overlapping weakly shallow TRSs by closing under constructor contexts of unbounded depth before adding one layer of function symbols.The paper identifies this application with Theorem 98 and Corollary 99.Source: §2.6 · pp. 10–11

3 Abstract reduction system

This section introduces abstract reduction system terminology and develops tools for finite conservative extensions, confluence-preserving unions, and quotient systems. It also states that G// preserves confluence and is terminating for every finite ARS G.

3.1 Notation and terminology of ARS

  • An ARS is a directed graph with a reduction relation; confluence and the Church–Rosser property are equivalent, and every finite ARS is looping.The section also defines normal forms, reducts, and related graph terminology.Source: §3.1 · pp. 11–12

3.2 Edge expansion as conservative extension

  • Every finite ARS contained in an ARS has a finite conservative intermediate extension, and adding an edge preserves conservativity when it attaches to an existing vertex.The attachment condition is necessary for the resulting extension to remain conservative.Source: §3.2 · pp. 12–13

3.3 Union of ARSs that preserves confluence

  • A union is confluent when one system is confluent and the other’s edges connect vertices already mutually reachable in it; two confluent systems also have a confluent hierarchical combination.A hierarchical combination requires each edge of the first system either to start outside the second system or to connect vertices mutually reachable in the second.Source: §3.3 · p. 14

3.4 Quotient ARS

  • A quotient ARS represents equivalence classes as vertices and adds an edge between distinct classes when the original system has an edge between their members; strong determinism implies determinism.The section defines quotient systems with respect to equivalences, including connectivity-based equivalences.Source: §3.4 · p. 15
  • Quotienting by a union of relations is isomorphic to successive quotienting, and under the stated disjoint-edge and vertex-inclusion conditions, acyclicity of a deterministic union implies acyclicity of the quotient.The quotient is T2/(T1 ∪ G) in the first result and G2/G1 in the second.Source: §3.4 · pp. 15–16
  • If T ∪ G is confluent, then T//G is confluent; conversely, confluence of T//G requires peaks in T to close in T ∪ G.The section also establishes that reductions in T//G can be lifted to reductions between representatives in T ∪ G.Source: §3.4 · pp. 16–17
  • The proof uses Proposition 20 to obtain an infinite G-reduction sequence and derives a contradiction to the assumption that G is looping.Source: §3.4 · p. 17
  • The confluence of G// is equivalent to the confluence of G.Source: §3.4 · p. 17
  • Every finite ARS G is looping; hence, G// is terminating.Source: §3.4 · p. 17

4 Edge expansion of finite ARS to make it confluent

This section develops edge expansion and hierarchical combination as tools for extending finite ARSs while preserving confluence. It also gives a construction of finite confluent extensions contained in a given confluent ARS.

4.1 Pseudo-normal form and confluence of ARS

  • In a looping ARS, every vertex reaches a pseudo-normal form, and confluence is equivalent to a stated convergence implication holding for every vertex.The implication is that if w reduces to u and u converges to v, then w converges to v.Source: §4.1 · p. 18
  • Adding v → v′ to a confluent ARS preserves confluence exactly under conditions characterized by Lemma 26, extending earlier confluent expansions that assumed termination.The supplied passage does not include the full conditions in Lemma 26.Source: §4.1 · p. 18

4.2 Pseudo-normal forms after edge expansion

  • The cited cases report a normal-form count of |NFG//| + 1, a count equal to |NFG//|, and removal of exactly one equivalence class in normal form.Source: §4.2 · p. 22

4.3 Finite confluent extension of a sub-ARS in a confluent ARS

  • For a confluent ARS G, an edge expansion G′ with G ⊆c G′ is confluent whenever its source is a pseudo-normal form or its target already belongs to G.The lemma also gives conditions for the introduced target or existing pseudo-normal forms to remain pseudo-normal after expansion.Source: §4.3 · p. 22
  • Lemma 29’s extension claim requires G to be confluent; without that assumption, adding an edge can invalidate a normal-form property.For G = {a → b, a → c, c → d} and G′ = G ∪ {b → c}, b is a normal form in G but c is not a normal form in G′.Source: §4.3 · p. 23
  • The construction extends finite ARSs by edges along joins in the confluent super-ARS, decreasing the number of normal forms to enable induction.Lemma 31 adds an edge v → v′; in the case v′ is already in G1 and does not reach v, the number of normal forms strictly decreases, and the induction constructs a further extension with fewer normal forms.Source: §4.3 · p. 24
  • Every finite ARS contained in a confluent ARS has a confluent finite extension between them.Lemma 32 establishes that if G′ ⊆c G2 and G′ is finite while G2 is confluent, there is a confluent finite G with G′ ⊆c G ⊆c G2.Source: §4.3 · p. 25

5 Spanning graph and its normalization

This section defines spanning graphs and an edge-normalization relation, proving that normalization terminates when the base ARS is confluent. It also shows that a spanning graph with confluent G and measure zero yields a confluent union G∪T1∪T2.

5.1 Spanning graph and its properties

  • A spanning graph has a finite, acyclic, strongly deterministic quotient (T1 ∪ T2)/G, which makes its weight function well-defined with minimum 0.The definition also requires G ⊆c Vrt, both edge systems to have vertices in G, and T1 and T2 to be disjoint.Source: §5.1 · pp. 25–26

5.2 Normalization Step of Spanning Graphs

  • Normalization redirects edges whose source is not in pnfG, and each step is well-defined while preserving the spanning-graph conditions.The resulting graph retains finiteness and confluence of G, and the normalized edge systems remain disjoint and have an acyclic, strongly deterministic quotient.Source: §5.2 · pp. 27, 29
  • A spanning graph is normalized when every T1 or T2 edge starts at a vertex in pnfG.Normalization also yields a target vertex in pnfG′ and preserves the base graph’s confluence.Source: §5.2 · pp. 27–28

5.3 Termination of spanning-graph normalization

  • When G is confluent and G ⊆c Vrt, each normalization step strictly decreases the nonnegative measure m(S), so normalization terminates.The weight function remains stable across each step, and its nonnegative values ensure m(S) ≥ 0.Source: §5.3 · p. 30
  • Spanning-graph normalization terminates.Theorem 43 establishes termination.Source: §5.3 · p. 31
  • Each normalization step strictly decreases the finite, non-negative measure m(S), ruling out an infinite normalization sequence.An infinite sequence would yield an infinite strictly decreasing sequence of non-negative integer measures, which is impossible.Source: §5.3 · p. 31
  • If G is confluent and m(S) = 0 for S = (G, T1, T2), then G∪T1∪T2 is confluent.When m(S) > 0, if normalization steps are applicable, termination guarantees an eventual spanning graph whose components G ∪T1∪T2 are confluent.Source: §5.3 · p. 31

6 Compatibility and Edge Commutativity for Constructing Confluent Finite ARSs

The section develops compatibility and edge commutativity conditions for constructing confluent finite ARSs. It applies them by repeatedly extending a spanning graph until the remaining edges satisfy a condition guaranteeing confluence.

6.1 Compatibility for Spanning Graph Construction

  • If T1 is compatible over Vrt and T1∪T2 is T1-compatible over Vrt, the quotient is strongly deterministic and acyclic with disjoint transition relations; a spanning graph exists and can be confluent if Vrt is confluent.Source: §6.1 · pp. 33–34

6.2 Edge commutativity and its preservation by normalization

  • Edge commutativity supplies a red edge for each blue edge, and normalization preserves both ordinary and T1-relative edge commutativity.The preservation claim applies to normalization with respect to Vrt when the normalized edge belongs to Hol.Source: §6.2 · pp. 35–36

6.3 Making Finite ARSs Confluent

  • Section 6.3 frames normalization of a spanning graph as a route to making G and G ∪ T1 ∪ T2 finite and confluent (Theorem 53).Source: §6.3 · p. 36
  • Repeated applications of Lemma 51 expand a spanning graph while preserving its conditions, and the measure m strictly decreases until the process terminates.The lemma’s assumptions include edge-commutativity properties and confluence of G and Vrt.Source: §6.3 · pp. 36, 38
  • Under compatibility and edge-commutativity conditions, Theorem 53 yields a finite confluent ARS extension from finite G1, T1, and T2.The assumptions include G1 ⊆ Vrt for confluent Vrt, T1 and T2 ⊆ Hol, and the stated compatibility and edge-commutativity properties.Source: §6.3 · pp. 37–38

7 Term rewriting systems and their R-graphs

This section sets out TRS conventions and root-distinct assumptions, then develops R-graph tools for classifying edges and constructing subterm and monotonic extensions. It focuses on handling collapsing edges through compatible sets of top edges and showing how compatibility is preserved under extension.

7.1 Notation and terminology of TRS

  • Weakly shallow TRSs require defined symbols only at roots or inside ground subterms on both rule sides, and the analysis adopts three root-distinct restrictions.The restrictions allow only h(x) → x as a collapsing rule, require non-collapsing rules to change the root symbol, and require both constants and non-constant function symbols.Source: §7.1 · pp. 39–40

7.2 Top and inner edges of R-graph

  • R-graphs are ARSs over term subsets with R-rewrite edges, classified by top, inner, and non-top positions; non-top edges are inner edges in non-collapsing systems.Under the root-distinct assumptions, an edge that is both top and inner must arise from the collapsing rule h(x) → x.Source: §7.2 · pp. 40–41

7.3 Direct-subterm graph of G

  • Direct-subterm graphs extract changed child edges from inner steps, while F′-monotonic extensions lift edges into contexts and preserve confluence, finiteness, and monotonicity.The extension is defined over a selected set of function symbols F′.Source: §7.3 · p. 42

7.4 Compatibility and edge-commutativity with collapsing edges

  • With the unique collapsing rule h(x) → x, Lemma 69 selects fewer collapsing edges to achieve compatibility and edge commutativity under confluent, T-subterm-closed inner-graph conditions.T-subterm-closure requires the graph to contain T’s vertices and the direct subterms of non-top edges to lie in G ∪ T; changing this definition can invalidate Theorem 79’s subterm property.Source: §7.4 · pp. 44–45
  • The proof removes collapsing edges h(s) → s whose sources can reach a specified inner-edge path, then shows each removed edge joins with its source using non-collapsing steps.The chosen subset T′c excludes edges for which h(s) can reach h(h(t)) → h(t); the proof establishes joinability for excluded edges and uses the resulting claims to verify the compatibility and edge-commutativity conditions.Source: §7.4 · pp. 45–46
  • The selected collapsing edges satisfy the compatibility criterion because inner-edge reachability yields a term h(v) whose associated edge is available, and the selected edge joins with v.The argument uses T-subterm-closedness and the fact that the selected edges are top edges to establish the required conditions.Source: §7.4 · p. 46
  • Under the stated conditions, the union of non-collapsing top edges and a compatible subset of collapsing top edges remains compatible over the inner-edge R-graph.Lemma 70 requires the non-collapsing top edges to be compatible and the selected collapsing edges to be compatible relative to them; mixed peaks are excluded because the two kinds of top steps have sources with different root symbols.Source: §7.4 · p. 46

8 Non-E-overlapping and shallow TRS

The section applies a finite, bottom-up ARS extension method to shallow non-E-overlapping TRSs, developing compatibility and edge-commutativity conditions for extending finite graphs while preserving confluence. It establishes confluence even with collapsing rules by showing that finite input R-graphs admit finite, confluent, subterm-closed R-graphs.

8.1 Designing Vrt for shallow TRS

  • For shallow non-E-overlapping TRSs, Lemma 71 establishes compatibility of non-collapsing top edges over MF(G), and Lemma 72 establishes their edge commutativity over ⟨Vrt, IndR(VVrt)ε⟩.The construction uses Vrt = MF(G); because shallow rules have variables at depth at most 1, a single-layer extension suffices, and filler edges synchronize reductions at nonlinear variable positions.Source: §8.1 · p. 47

8.2 Confluence without collapsing rules

  • Non-E-overlapping, shallow, non-collapsing TRSs are confluent, and every finite R-graph extends to a finite confluent R-graph.The paper presents the result as an alternative proof of Theorem 5 in.Source: §8.2 · pp. 48, 50

8.3 Confluence with collapsing rules

  • For shallow non-E-overlapping TRSs, Lemma 77 extends a finite R-graph to a finite confluent, subterm-closed R-graph when its subterms lie in a finite confluent, subterm-closed graph.Subterm closure is needed when collapsing rules alter the depth of confluent sequences.Source: §8.2 · p. 49, §8.3 · p. 50
  • For any finite R-graph, a non-E-overlapping and shallow TRS admits a finite, confluent, subterm-closed R-graph.The proof follows Theorem 75’s approach, replacing Lemma 73 with Lemma 77 and incorporating subterm-closedness for G0 and G.Source: §8.3 · p. 52
  • Non-E-overlapping and shallow TRSs are confluent.The result follows from the existence of a finite, confluent, subterm-closed R-graph for a finite input R-graph.Source: §8.3 · p. 52

9 Non-E-overlapping and weakly shallow TRSs

This section develops constructor expansion, compatibility, and edge commutativity to extend finite graphs toward confluence proofs for non-E-overlapping weakly shallow TRSs. It establishes finite confluent graph extensions and derives a decidable sufficient condition using non-ω-overlap.

9 Non-E-overlapping and weakly shallow TRSs

  • The section relaxes Theorem 79’s shallowness condition to weak shallowness, first constructing a suitable Vrt structure and then proving confluence.The construction introduces the novel constructor expansion in Section 9.1, before the confluence proof in Section 9.3.Source: §9 · p. 52

9.1 Designing Vrt for weakly shallow TRSs

  • The constructor-expansion operator MC preserves subterm-closedness and preserves confluence when applied to a confluent graph.The section introduces constructor expansion to design Vrt for weakly shallow TRSs.Source: §9 · p. 52, §9.1 · p. 54

9.2 Compatibility and edge commutativity of non-collapsing rules in non-E-overlapping and weakly shallow TRSs

  • Under the section’s graph conditions, non-collapsing rule edges are compatible over G∞ and edge-commutative over (G∞, IndR(VG∞)ε).The proof uses non-E-overlap and weak shallowness; the cited remark says the left-hand-side assumption can be relaxed to non-E-overlap, while weak shallowness is essential on right-hand sides.Source: §9.2 · p. 57

9.3 Confluence of non-E-overlapping and weakly shallow TRS

  • For a weakly shallow, non-E-overlapping TRS, every finite R-graph G0 with sub(G0) ⊆ G for a finite confluent subterm-closed G has a finite confluent subterm-closed extension G′ containing G0.This is the finite-extension result used to prove confluence.Source: §9.3 · p. 58
  • Every finite R-graph for a non-E-overlapping, weakly shallow TRS has a finite, confluent, subterm-closed R-graph extension.The extension contains the original graph.Source: §9.3 · p. 63
  • Non-E-overlapping and weakly shallow TRSs are confluent.Source: §9.3 · p. 63
  • Non-ω-overlapping and weakly shallow TRSs are confluent, giving a decidable sufficient condition for confluence.This follows because weakly shallow TRSs are weak monadic, so non-ω-overlap implies non-E-overlap [28, Theorem 4.18]; non-ω-overlap is decidable, whereas non-E-overlap is undecidable for weakly shallow TRSs.Source: §9.3 · p. 63

10 Conclusion

The paper introduces a method based on edge compatibility and commutativity, proving confluence for non-E-overlapping weakly shallow TRSs. It also derives a decidable sufficient condition and identifies weaker shallowness conditions for future work.

10 Conclusion

  • The method proves confluence for non-E-overlapping and weakly shallow TRSs using edge compatibility and edge commutativity.Source: §10 · p. 63
  • Non-ω-overlapping and weakly shallow TRSs form a decidable sufficient condition for confluence.Source: §10 · p. 63
  • One future direction is to allow at most one defined function symbol on each root-to-variable path.This is the paper’s almost weakly shallow condition.Source: §10 · p. 64
  • Another proposed direction requires weak shallowness only on rule right-hand sides; the paper expects this condition to suffice.The rationale is that the relevant correspondence also holds on left-hand sides of non-E-overlapping rules.Source: §10 · p. 64
Loading 2610.09572v1…