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

Martin Avanzini (1) , Ugo Dal Lago (2, 1) , Alexis Ghyselen (3)

1 FOCUS - Foundations of Component-based Ubiquitous Systems
2 UNIBO - Alma Mater Studiorum Università di Bologna = University of Bologna
3 ENS de Lyon - École normale supérieure de Lyon

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.

Domaines: Informatique et langage [cs.CL]; Complexité [cs.CC]; Logique en informatique [cs.LO]

Martin Avanzini, Ugo Dal Lago, Alexis Ghyselen. Type-Based Complexity Analysis of Probabilistic Functional Programs (Technical Report). [Research Report] INRIA Sophia Antipolis; University of Bologna; ENS Lyon. 2019. ⟨hal-02103943⟩