Probabilistic Rewriting: Relations between Normalization, Termination, and Unique Normal Forms.
Claudia Faggian · arXiv (Cornell University) · 2018
While a mature body of work supports the study of rewriting systems, even infinitary ones, abstract tools for Probabilistic Rewriting are still limited. Here, we investigate questions such as uniqueness of the result (unique limit distribution) and normalizing strategies (is there a strategy to find a result with greatest probability?). The goal is to have tools to analyse the operational properties of calculi (such as probabilistic lambda-calculi) whose evaluation is non-deterministic, where non-determinism is that of parallelism, which arises from a choice between several redexes. We investigate how the asymptotic behavior of different rewrite sequences starting from the same term compare w.r.t. normal forms, and we develop methods to study and compare strategies. Our approach is that of Abstract Rewrite Systems, i.e. we search for general properties of probabilistic rewriting, which hold independently of the specific nature of the objects.