Abstract

Logically constrained term rewriting is a relatively new rewriting formalism
that naturally supports built-in data structures, such as integers and bit
vectors. In the analysis of logically constrained term rewrite systems
(LCTRSs), rewriting constrained terms plays a crucial role. However, this
combines rewrite rule applications and equivalence transformations in a closely
intertwined way. This intertwining makes it difficult to establish useful
theoretical properties for this kind of rewriting and causes problems in
implementations—namely, that impractically large search spaces are often
required. To address this issue, we propose in this paper a novel notion of
most general constrained rewriting, which operates on existentially constrained
terms, a concept recently introduced by the authors. We define a class of
left-linear, left-value-free LCTRSs that are general enough to simulate all
left-linear LCTRSs and exhibit the desired key property: most general
constrained rewriting commutes with equivalence. This property ensures that
equivalence transformations can be deferred until after the application of
rewrite rules, which helps mitigate the issue of large search spaces in
implementations. In addition to that, we show that the original rewriting
formalism on constrained terms can be embedded into our new rewriting formalism
on existentially constrained terms. Thus, our results are expected to have
significant implications for achieving correct and efficient implementations in
tools operating on LCTRSs.

BibTeX

@inproceedings{KTJSNNTA-PPDP25,
  author    = "Kanta Takahata and Jonas Sch{\"{o}}pf and Naoki Nishida and Takahito Aoto",
  title     = "Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations",
  booktitle = "Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming (PPDP)",
  editor    = "Ma{\l{}}gorzata Biernacka, Carlos Olarte",
  series    = "Association for Computing Machinery",
  pages     = "9:1--9:13",
  year      = 2025,
  doi       = "10.1145/3756907.3756916"
}