Chuangjie Xu - A syntactic approach to continuity of T-definable functionals

lmcs:5394 - Logical Methods in Computer Science, February 20, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:22)2020
A syntactic approach to continuity of T-definable functionalsArticle

Authors: Chuangjie Xu ORCID

    We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in Gödel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.


    Volume: Volume 16, Issue 1
    Published on: February 20, 2020
    Accepted on: October 15, 2019
    Submitted on: April 23, 2019
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    1 Document citing this article

    Consultation statistics

    This page has been seen 1337 times.
    This article's PDF has been downloaded 288 times.