Computer Science Department
School of Computer Science, Carnegie Mellon University
The Realizability Approach to Computable Analysis and Topology
In the first part of the dissertation, I present categories of modest sets and axiomatize their internal logic, including the computability predicate. The logic is a predicative intuitionistic first-order logic with dependent types, subsets, quotients, inductive and coinductive types.
The second part of the dissertation investigates examples of categories of modest sets. I focus on equilogical spaces, and their relationship with domain theory and Type Two Effectivity (TTE). I show that domains with totality embed in equilogical spaces, and that the embedding preserves both simple and dependent types. I relate equilogical spaces and TTE in three ways: there is an applicative retraction between them, they share a common cartesian closed subcategory that contains all countably based T0-spaces, and they are related by a logical transfer principle. These connections explain why domain theory and TTE agree so well.
In the last part of the dissertation, I demonstrate how to develop computable analysis and topology in the logic of modest sets. The theorems and constructions performed in this logic apply to all categories of modest sets. Furthermore, by working in the internal logic, rather than directly with specic examples of modest sets, we argue abstractly and conceptually about computability in analysis and topology, avoiding the unpleasant details of the underlying computational models, such as Godel encodings and representations by sequences.