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 ℓ RPCF, provides a sound methodology for average case complexity analysis, but also that it is extensionally complete, in the sense that any average case nolytime Turing machines can be encoded as a term typable in ℓRPCF.
Type-based complexity analysis of probabilistic functional programs / Avanzini Martin; Dal Lago U.; Ghyselen A.. - ELETTRONICO. - 2019-:(2019), pp. 8785725.1-8785725.13. (Intervento presentato al convegno 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 tenutosi a SFU Harbour Centre in Downtown Vancouver, can nel 2019) [10.1109/LICS.2019.8785725].
Type-based complexity analysis of probabilistic functional programs
Dal Lago U.
;
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 ℓ RPCF, provides a sound methodology for average case complexity analysis, but also that it is extensionally complete, in the sense that any average case nolytime Turing machines can be encoded as a term typable in ℓRPCF.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.