Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms

TL;DR

This paper develops proof techniques for probabilistic rewriting systems to analyze their termination and the uniqueness of their normal forms, aiding the operational understanding of probabilistic calculi.

Contribution

It introduces new methods for analyzing probabilistic rewriting systems, focusing on termination and the uniqueness of limit distributions, which were previously limited in abstract tools.

Findings

Established criteria for the uniqueness of limit distributions in probabilistic rewriting

Developed comparison techniques for different reduction strategies

Enhanced tools for operational analysis of probabilistic calculi

Abstract

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a set of proof techniques to analyze and compare reduction strategies. The goal is to have tools to support the operational analysis of probabilistic calculi (such as probabilistic lambda-calculi) where evaluation allows for different reduction choices (hence different reduction paths).