home > publications > AGDL:LICS:19

Type-Based Complexity Analysis of Probabilistic Functional Programs

Type-Based Complexity Analysis of Probabilistic Functional Programs
M. Avanzini and A. Ghyselen and U. Dal Lago
Proceedings of the 34th Logics in Computer Science Symposium, pages 1–13, 2019.

Abstract

We show that complexity analysis of probabilistic higher-order functional programs can be carried out compositionally by way of a type system. The introduced type system is a significant extension of refinement types. On the one hand, the presence of probabilistic effects requires adopting a form of dynamic distribution type, subject to a coupling-based subtyping discipline. On the other hand, recursive definitions are proved terminating by way of Lyapunov ranking functions. We prove not only that the obtained type system, called dlRPCF, provides a sound methodology for average case complexity analysis, but also that is extensionally complete, in the sense that any average case polytime Turing machines can be encoded as a term typable in dlRPCF.

Categories

Probabilistic, Termination, Complexity Analysis, Types