Powell, Thomas - A unifying framework for continuity and complexity in higher types

lmcs:5746 - Logical Methods in Computer Science, September 9, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:17)2020
A unifying framework for continuity and complexity in higher types

Authors: Powell, Thomas

We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.

Volume: Volume 16, Issue 3
Published on: September 9, 2020
Submitted on: September 5, 2019
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Logic