Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version)
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
TL;DR
This paper addresses the challenge of characterizing when two constrained terms in logically constrained term rewriting denote the same set of instantiated terms. It introduces existentially constrained terms as an embedding mechanism for original constrained terms, and develops syntactic characterizations of their equivalence, including renaming-based criteria and a transformation to pattern-general form (PG). The authors establish a sound and complete framework for equivalence via the PG transformation and broader, general characterizations, laying the groundwork for commutation results with constrained rewriting and enabling more tractable reasoning in LCTRSs. Overall, the work strengthens the theoretical underpinnings of constraint reasoning in LCTRSs and has potential implications for tooling and automated reasoning in this domain.
Abstract
Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role in various analyses and applications of logically constrained term rewriting. A fundamental question on constrained terms arising there is how to characterize equivalence between them. However, in the current literature only limited progress has been made on this. In this paper, we provide several sound and complete solutions to tackle this problem. Our key idea is the introduction of a novel concept, namely existentially constrained terms, into which the original form of constrained terms can be embedded. We present several syntactic characterizations of equivalence between existentially constrained terms. In particular, we provide two different kinds of complete characterizations: one is designed to facilitate equivalence checking, while the other is intended for theoretical analysis.