Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, Joost-Pieter Katoen

TL;DR

This work introduces weighted abstract reduction systems (wARS) by enriching ARSs with semiring weights assigned to reductions, enabling provenance-like analyses for termination, complexity, safety, and beyond. The framework uses complete lattice semirings to handle possibly infinite nondeterminism and reductions, representing reduction outcomes as weighted trees and taking supremums over schedulers. It demonstrates broad expressivity through sections on termination/complexity, size bounds, probabilistic rewriting, formal languages, and multi-property combinations, while providing methods to prove upper and lower bounds via interpretations, approximations, and loop-based unboundedness. The approach unifies disparate analyses under a single, composable semantic foundation, with potential for automation and applications to TRSs and probabilistic systems. Limitations are acknowledged (e.g., starvation-freedom requires extensions), and future work targets enhanced automated boundedness proofs and broader property coverage.

Abstract

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.

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

TL;DR

This work introduces weighted abstract reduction systems (wARS) by enriching ARSs with semiring weights assigned to reductions, enabling provenance-like analyses for termination, complexity, safety, and beyond. The framework uses complete lattice semirings to handle possibly infinite nondeterminism and reductions, representing reduction outcomes as weighted trees and taking supremums over schedulers. It demonstrates broad expressivity through sections on termination/complexity, size bounds, probabilistic rewriting, formal languages, and multi-property combinations, while providing methods to prove upper and lower bounds via interpretations, approximations, and loop-based unboundedness. The approach unifies disparate analyses under a single, composable semantic foundation, with potential for automation and applications to TRSs and probabilistic systems. Limitations are acknowledged (e.g., starvation-freedom requires extensions), and future work targets enhanced automated boundedness proofs and broader property coverage.

Abstract

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.
Paper Structure (21 sections, 18 theorems, 9 equations, 3 figures, 2 algorithms)

This paper contains 21 sections, 18 theorems, 9 equations, 3 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Semiring Semantics for Abstract Reduction Systems
  4. Expressivity of Semiring Semantics
  5. Termination and Complexity
  6. Size Bounds
  7. Probabilistic Rewriting
  8. Formal Languages
  9. Combinations of Semirings
  10. Limitations
  11. Proving Upper Bounds on Weights
  12. Guaranteed Boundedness
  13. Proving Boundedness via Interpretations
  14. Proving Lower Bounds on Weights
  15. Approximating the Weight
  16. ...and 6 more sections

Key Result

Corollary 15

For any wARS $(A, \to, \mathbb{S}, \mathsf{f}_{\mathtt{NF}}, \mathsf{Aggr}_{a\to B})$, the weight $\llbracket a \rrbracket^{}_{}$ is well defined for every object $a\in A$.

Figures (3)

  • Figure 1: Non-exhaustive list of complete lattice semirings $\mathbb{S} = (S,\oplus,\odot,\mathbf{0},\mathbf{1})$.
  • Figure 2: Two example reduction trees, where each node $v$ is labeled with $a_v\in A$ and the small numbers are the corresponding weights $\llbracket \mathfrak{T} \rrbracket^{v}_{}$. Colored nodes are labeled by normal forms.
  • Figure 3: An example of a finite reduction tree containing a loop from $\mathsf{idle}(\varepsilon)$ to itself. The corresponding evaluation of the induced weight polynomial for the runtime is depicted in red above the nodes, and for the space of the waiting list in blue below the nodes.

Theorems & Definitions (54)

  • Example 1: Provenance Analysis in Databases
  • Example 2: Provenance Analysis for ARSs
  • Definition 3: Abstract Reduction System, Normal Form, Determinism
  • Definition 4: Reduction Sequence, Termination
  • Definition 5: Semiring
  • Definition 6: Natural Order
  • Definition 7: Complete Lattice
  • Definition 8: Infinite Sums and Products
  • Definition 9: Sequence Abstract Reduction System
  • Definition 10: Reduction Tree
  • ...and 44 more