Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Left-Linear Completion with AC Axioms

Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp

TL;DR

The paper addresses the challenge of completion modulo equational theories for left-linear TRSs by using the normal rewrite relation and avoiding $ ext{E}$-unification. It introduces a Church–Rosser modulo framework via peak-and-cliff decreasingness and prime critical pairs, and develops two refined inference systems, Avenhaus' and Bachmair's, proving correctness for finite runs and establishing canonicity results. For the specific AC theory, it analyzes limitations of left-linear AC completion and relates it to general AC completion through simulation, supported by an implemented AC-completion tool, accompll, and experimental results. The work demonstrates that while left-linear AC completion can be faster by avoiding AC unification, it may require infinite rules in some cases, yet its simulation with general AC completion provides practical pathways to switch methods mid-completion. Overall, the article advances the theory of rewriting modulo and provides practical tooling and empirical insights into AC completion in the left-linear setting.

Abstract

We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process.

Left-Linear Completion with AC Axioms

TL;DR

The paper addresses the challenge of completion modulo equational theories for left-linear TRSs by using the normal rewrite relation and avoiding -unification. It introduces a Church–Rosser modulo framework via peak-and-cliff decreasingness and prime critical pairs, and develops two refined inference systems, Avenhaus' and Bachmair's, proving correctness for finite runs and establishing canonicity results. For the specific AC theory, it analyzes limitations of left-linear AC completion and relates it to general AC completion through simulation, supported by an implemented AC-completion tool, accompll, and experimental results. The work demonstrates that while left-linear AC completion can be faster by avoiding AC unification, it may require infinite rules in some cases, yet its simulation with general AC completion provides practical pathways to switch methods mid-completion. Overall, the article advances the theory of rewriting modulo and provides practical tooling and empirical insights into AC completion in the left-linear setting.

Abstract

We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process.
Paper Structure (28 sections, 37 theorems, 80 equations, 1 figure, 1 table)

This paper contains 28 sections, 37 theorems, 80 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Rewrite Systems
  4. Critical Peaks
  5. Rewriting Modulo
  6. Church--Rosser Criterion
  7. Peak-and-Cliff Decreasingness
  8. Prime Critical Pairs
  9. Avenhaus' Inference System
  10. Inference System
  11. Correctness Proof
  12. Bachmair's Inference System
  13. Canonicity
  14. Results for Abstract Rewriting Modulo
  15. Computing B-Canonical Term Rewrite Systems
  16. ...and 13 more sections

Key Result

Theorem 2.4

Let $\mathcal{R}$ be a terminating TRS. The TRS$\mathcal{R}$ is confluent if and only if $\mathsf{PCP}({\mathcal{R}}) \subseteq {\downarrow_{\mathcal{R}}}$. ∎

Figures (1)

  • Figure 1: Flow chart for accompll's completion procedure.

Theorems & Definitions (112)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Theorem 2.4: KMN88
  • Example 2.5
  • Example 2.6
  • Lemma 2.7: A95
  • Example 2.8
  • Example 2.9
  • Theorem 3.1: H80
  • ...and 102 more