CMU-CS-00-164Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-00-164
Andrej Bauer September 2000 Ph.D. Thesis
CMU-CS-00-164.ps
Keywords: Computablity, realizability, modest sets, computable
topology, computable analysis
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 T 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. 237 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |