Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)
Takahito Aoto, Naoki Nishida, Jonas Schöpf
TL;DR
The paper introduces partial constrained rewriting for existentially constrained terms within LCTRSs, distinguishing it from existing most general constrained rewriting. It shows a direct correspondence where MG rewriting subsumes partial rewriting, and demonstrates that MG steps can simulate partial steps via subsumption and equivalence. Through novel value interpretations, the authors provide precise characterizations of partial versus MG reductions and clarify normal-form behavior under each regime. The work clarifies the theoretical landscape for constrained rewriting, enabling more robust reasoning about reachability, joinability, and equivalence in LCTRSs, with potential extensions to non-left-linear rules and commutativity with equivalence as future directions.
Abstract
Logically constrained term rewrite systems (LCTRSs) are a rewriting formalism that naturally supports built-in data structures, including integers and bit-vectors. The recent framework of existentially constrained terms and most general constrained rewriting on them (Takahata et al., 2025) has many advantages over the original approach of rewriting constrained terms. In this paper, we introduce partial constrained rewriting, a variant of rewriting existentially constrained terms whose underlying idea has already appeared implicitly in previous analyses and applications of LCTRSs. We examine the differences between these two notions of constrained rewriting. First, we establish a direct correspondence between them, leveraging subsumption and equivalence of constrained terms where appropriate. Then we give characterizations of each of them, using the interpretation of existentially constrained terms by instantiation. We further introduce the novel notion of value interpretation, that highlights subtle differences between partial and most general rewriting.