Confluence of Logically Constrained Rewrite Systems Revisited

TL;DR

This paper investigates confluence for logically constrained rewrite systems (LCTRSs) and shows that local confluence for terminating LCTRSs is undecidable even over decidable theories, challenging prior assumptions about the ease of transferring TRS techniques. It introduces a lightweight, left-linear transformation from LCTRSs to TRSs that preserves rewrite behavior, enabling the application of TRS confluence criteria to the constrained setting. The authors extend advanced TRS criteria, such as almost development-closed and parallel critical-pair conditions, to LCTRSs by lifting them through the transformation and establish left-linear confluence results for LCTRSs via development-closedness and parallel-closedness arguments. They also discuss subtleties in the constrained-term equivalence notions and provide a framework that supports confluence provers and formal verification efforts, demonstrating the practical reach of these theoretical results.

Abstract

We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.