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

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