Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

TL;DR

This paper introduces a weighted semiring-based semantics for abstract reduction systems, enabling provenance analysis and complexity bounds for non-deterministic and infinite reductions.

Contribution

It develops a formalism that extends ARSs with semiring weights, allowing analysis of properties like termination and complexity in a unified framework.

Findings

Provides a formal semantics for weighted ARSs.

Develops techniques for bounding weights and analyzing properties.

Enables provenance analysis for arbitrary ARSs.

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.