A constructive function-theoretic approach to topological compactness

Petrakis, Iosif (2016): A constructive function-theoretic approach to topological compactness. 31st Annual ACM/IEEE Symposium on Logic in Computer Science LICS '16, New York, NY, USA, July 05 - 08, 2016. In: Proceedings of the 31St Annual Acm-Ieee Symposium On Logic in Computer Science (LICS 2016), New York: Association for Computing Machinery. pp. 605-614

Abstract

We introduce 2-compactness, a constructive function-theoretic alternative to topological compactness, based on the notions of Bishop space and Bishop morphism, which are constructive function-theoretic alternatives to topological space and continuous function, respectively. We show that the notion of Bishop morphism is reduced to uniform continuity in important cases, overcoming one of the obstacles in developing constructive general topology posed by Bishop. We prove that 2-compactness generalizes metric compactness, namely that the uniformly continuous real-valued functions on a compact metric space form a 2-compact Bishop topology. Among other properties of 2-compact Bishop spaces, the countable Tychonoff compactness theorem is proved for them. We work within BISH*, Bishop's informal system of constructive mathematics BISH equipped with inductive definitions with rules of countably many premises, a system strongly connected to Martin-Lof's Type Theory.

• Item Type: Conference or Workshop Item (Paper)
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• Place of Publication: New York
• Language: English