Type-Based Complexity Analysis of Probabilistic Functional Programs (Technical Report)

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 linear dependent 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 ranking functions. We prove not only that the obtained system, called dℓRPCF, provides a sound methodology for average case complexity analysis, but is also extensionally complete, in the sense that all average case polytime Turing machines can be encoded as a term typable in dℓRPCF