License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2023.37
URN: urn:nbn:de:0030-drops-185718
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18571/
Cohen, Liron ;
da Rocha Paiva, Bruno ;
Rahli, Vincent ;
Tosun, Ayberk
Inductive Continuity via Brouwer Trees
Abstract
Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, another formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of this "inductive" continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this formulation of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that this inductive continuity principle implies other forms of continuity principles.
BibTeX - Entry
@InProceedings{cohen_et_al:LIPIcs.MFCS.2023.37,
author = {Cohen, Liron and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk},
title = {{Inductive Continuity via Brouwer Trees}},
booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
pages = {37:1--37:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-292-1},
ISSN = {1868-8969},
year = {2023},
volume = {272},
editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18571},
URN = {urn:nbn:de:0030-drops-185718},
doi = {10.4230/LIPIcs.MFCS.2023.37},
annote = {Keywords: Continuity, Dialogue trees, Stateful computations, Intuitionistic Logic, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda}
}
