Weighted Rewriting
摘要
We introduce the notion of weighted abstract reduction systems (weighted ARSs), generalising standard and relative ARSs by allowing non-uniform weights on transition steps. Weighted ARSs give rise to a theory of rewriting where quantitative properties—noteworthy complexity related properties—can be more directly studied. Unlike these standard notions, weighted ARSs permit the study of quantitative properties of reduction systems of non-uniform weight, such as the analysis of expectation-based properties of probabilistic systems. We establish ranking functions as a means to analyse (strong) boundedness of weighted ARSs, i.e., the property that weights of reductions are bounded from above. We showcase their applicability by instantiating them to weighted term rewrite systems and probabilistic reduction systems, the latter generalising Lyapunov ranking functions to reason about expected derivation heights.