A constructive model of uniform continuity

Chuangjie Xu; Martín Escardó

doi:10.1007/978-3-642-38946-7_18

A constructive model of uniform continuity

Chuangjie Xu, Martín Escardó

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

10 Citations (Scopus)

Abstract

We construct a continuous model of Gödel's system T and its logic HA^ω in which all functions from the Cantor space 2 ^ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2^ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2^ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

Original language	English
Title of host publication	Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Pages	236-349
Number of pages	114
DOIs	https://doi.org/10.1007/978-3-642-38946-7_18
Publication status	Published - 2013
Event	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands Duration: 26 Jun 2013 → 28 Jun 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7941 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Country/Territory	Netherlands
City	Eindhoven
Period	26/06/13 → 28/06/13

Keywords

Constructive mathematics
Fan functional
Gödel's system T
HA
intuitionistic type theory
sheaves
topological models
topos theory
uniform continuity

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-38946-7_18

Cite this

Xu, C., & Escardó, M. (2013). A constructive model of uniform continuity. In Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings (pp. 236-349). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7941 LNCS). https://doi.org/10.1007/978-3-642-38946-7_18

@inproceedings{86e40d178b374124b4e4ebc2b4f1a7df,

title = "A constructive model of uniform continuity",

abstract = "We construct a continuous model of G{\"o}del's system T and its logic HAω in which all functions from the Cantor space 2 ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.",

keywords = "Constructive mathematics, Fan functional, G{\"o}del's system T, HA, intuitionistic type theory, sheaves, topological models, topos theory, uniform continuity",

author = "Chuangjie Xu and Mart{\'i}n Escard{\'o}",

year = "2013",

doi = "10.1007/978-3-642-38946-7_18",

language = "English",

isbn = "9783642389450",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "236--349",

booktitle = "Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings",

note = "11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 ; Conference date: 26-06-2013 Through 28-06-2013",

}

Xu, C & Escardó, M 2013, A constructive model of uniform continuity. in Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7941 LNCS, pp. 236-349, 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, Eindhoven, Netherlands, 26/06/13. https://doi.org/10.1007/978-3-642-38946-7_18

A constructive model of uniform continuity. / Xu, Chuangjie; Escardó, Martín.
Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. p. 236-349 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7941 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A constructive model of uniform continuity

AU - Xu, Chuangjie

AU - Escardó, Martín

PY - 2013

Y1 - 2013

N2 - We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

AB - We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

KW - Constructive mathematics

KW - Fan functional

KW - Gödel's system T

KW - HA

KW - intuitionistic type theory

KW - sheaves

KW - topological models

KW - topos theory

KW - uniform continuity

UR - http://www.scopus.com/inward/record.url?scp=84884513912&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38946-7_18

DO - 10.1007/978-3-642-38946-7_18

M3 - Conference contribution

AN - SCOPUS:84884513912

SN - 9783642389450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 236

EP - 349

BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings

T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013

Y2 - 26 June 2013 through 28 June 2013

ER -

A constructive model of uniform continuity

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this