Thomas Powell - 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 typesArticle

Authors: Thomas Powell

    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
    Accepted on: August 19, 2020
    Submitted on: September 5, 2019
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Logic

    Consultation statistics

    This page has been seen 1016 times.
    This article's PDF has been downloaded 173 times.