Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Published in 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK, 2025
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.
Recommended citation: Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, Joost-Pieter Katoen: "Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems." FSCD 2025: 6:1-6:21
Download Paper | Download Slides | Download Bibtex