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
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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 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.
Complete list of metadatas

https://hal.archives-ouvertes.fr/hal-02103943
Contributor : Alexis Ghyselen <>
Submitted on : Friday, April 19, 2019 - 8:54:23 AM
Last modification on : Saturday, April 20, 2019 - 1:40:42 AM

File

lics-techreport.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

37

Files downloads

19