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

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 \emph{uniqueness of the result} (unique limit distribution), and develop a set of proof techniques to analyze and compare \emph{reduction strategies}. The goal is to have tools to support the \emph{operational} analysis of \emph{probabilistic} calculi (such as probabilistic lambda-calculi) whose evaluation is also non-deterministic, in the sense that different reductions are possible.