Searcharxiv⌕ Search

arXiv subjects

Jonas Schöpf

Publications and source records attributed to Jonas Schöpf.

8 recordsLinked to original sources
arXiv2026

Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)

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.

cs.LO↗
arXiv2025

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version)

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.

cs.LO↗
arXiv2025

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)

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.

cs.LO↗
arXiv2024

Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)

Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data.

cs.LO↗
arXiv2024

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derive a new notion of consistency for constrained equational theories.

cs.LO↗
arXiv2024

Confluence of Logically Constrained Rewrite Systems Revisited

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.

cs.LO↗
arXiv2018

TTT2 with Termination Templates for Teaching

On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other hand, automation of such checks would save time and help to establish correctness of exam solutions, examples in lecture notes etc. To this end, we introduce a template mechanism for the termination tool TTT2 that allows us to restrict parameters of certain termination methods. In the extreme, when all parameters are fixed, such restrictions result in checks for specific proofs.

cs.LO↗