Left-Linear Completion with AC Axioms

TL;DR

This paper introduces a new approach to completion modulo equational theories for left-linear term rewrite systems, avoiding unification and ensuring correctness and canonicity of the resulting systems.

Contribution

It provides a new correctness proof, establishes simulation results between inference systems, and shows how to switch between left-linear AC and general AC completion.

Findings

Correctness of finite runs established

Simulation between inference systems proven

Canonicity results for unique rule representations

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.