A constructive manifestation of the Kleene–Kreisel continuous functionals

Martín Escardó, Chuangjie Xu

Research output: Contribution to conference (unpublished)Paperpeer-review

Abstract

We identify yet another category equivalent to that of Kleene–Kreisel continuous functionals. Reasoning constructively and predicatively, all functions from the Cantor space to the natural numbers are uniformly continuous in this category. We do not need to assume Brouwerian continuity axioms to prove this, but, if we do, then we can show that the full type hierarchy is equivalent to our manifestation of the continuous functionals. We construct this manifestation within a category of concrete sheaves, called C-spaces, which form a locally cartesian closed category, and hence can be used to model system T and dependent types. We show that this category has a fan functional and validates the uniform continuity axiom in these theories. Our development is within informal constructive mathematics, along the lines of Bishop mathematics. However, in order to extract concrete computational content from our constructions, we formalized it in intensional Martin-Löf type theory, in Agda notation.

Original languageEnglish
Pages4-6
Number of pages3
Publication statusPublished - 2014
Event11th International Conference on Computability and Complexity in Analysis, CCA 2014 - Darmstadt, Germany
Duration: 21 Jul 201424 Jul 2014

Conference

Conference11th International Conference on Computability and Complexity in Analysis, CCA 2014
Country/TerritoryGermany
CityDarmstadt
Period21/07/1424/07/14

Bibliographical note

Publisher Copyright:
© CCA 2014 - 11th International Conference on Computability and Complexity in Analysis, Proceedings. All rights reserved.

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint

Dive into the research topics of 'A constructive manifestation of the Kleene–Kreisel continuous functionals'. Together they form a unique fingerprint.

Cite this