home > publications > AGDL:LICS:19

Type-Based Complexity Analysis of Probabilistic Functional Programs

Type-Based Complexity Analysis of Probabilistic Functional Programs
Martin Avanzini, Ugo Dal Lago and Alexis Ghyselen
34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, 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

, , ,