PROBABILISTIC TERM REWRITING

Martin Avanzini (INRIA Sophia Antipolis Méditerranée)

Randomized computation has been one of the most fruitful extensions of the standard, deterministic, computational model, since the birth of the computer.

Indeed, randomization is nowadays pervasive in computer science and sometimes even essential, e.g. in the design of efficient algorithms, in cryptography, machine learning, or, robotics. In contrast, the development of a proper theory of randomized programming languages has been unarguably much slower than its adaption, and is still a very active research area.

Among the many research directions, inspired by the seminal works of Bournez, Garnier and Kirchner, the community has taken several steps forward in the development of a probabilistic rewriting theory, serving also as a foundational theory of randomized programming languages. While, unarguably, the probabilistic rewriting theory is much less developed than the standard rewriting theory, several interesting results have been achieved so far.

This lecture will give an introduction to probabilistic rewriting, its established theory and reasoning techniques, and its application in randomized programming language semantics. It is divided into four parts:

1. Basics: Probabilistic (abstract) reduction systems, Markov chain vs multi-distribution reductions.

2. Probabilistic programming semantics: Modeling programming languages and randomization via probabilistic reduction systems.

3. A probabilistic rewriting theory: termination, normalization, unique normal forms, etc., as quantitative, asymptotic properties and their known relation ships.

4. Verification and analysis: termination, expected (i.e. average) complexity and weakest-precondition reasoning.

Bibliography:

• Martin Avanzini, Ugo Dal Lago, Akihisa Yamada: On probabilistic term rewriting. Sci. Comput. Program. 185 (2020)

• Olivier Bournez, Florent Garnier: Proving Positive Almost-Sure Termination. RTA 2005: 323-337

• Claudia Faggian: Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms. FSCD 2019: 19:1-19:25

• Annabelle McIver, Carroll Morgan: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer 2005, ISBN 978-0-387-40115-7, pp. 1-310

Basics in probability theory are helpful but not required; the lecture is self-contained.