Saved in:
Bibliographic Details
Main Authors: Ahrens, Emma, Kassing, Jan-Christoph, Giesl, Jürgen, Katoen, Joost-Pieter
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2505.08496
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866915286396960768
author Ahrens, Emma
Kassing, Jan-Christoph
Giesl, Jürgen
Katoen, Joost-Pieter
author_facet Ahrens, Emma
Kassing, Jan-Christoph
Giesl, Jürgen
Katoen, Joost-Pieter
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2505_08496
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Ahrens, Emma
Kassing, Jan-Christoph
Giesl, Jürgen
Katoen, Joost-Pieter
Logic in Computer Science
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.
title Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
topic Logic in Computer Science
url https://arxiv.org/abs/2505.08496