Abstract:
In this dissertation, I explore aspects of computable analysis and
topology in the framework of relative realizability. The
computational models are partial combinatory algebras with
subalgebras of computable elements, out of which categories of
modest sets are constructed. The internal logic of these categories
is suitable for developing a theory of computable analysis and
topology, because it is equipped with a computability predicate and
it supports many constructions needed in topology and analysis. In
addition, a number of previously studied approaches to computable
topology and analysis are special cases of the general theory of
modest sets.
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 specific 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 Gödel encodings and representations
by sequences.
Committee:
Dana S. Scott, chair
Steven M. Awodey
Lenore Blum
Abbas Edalat
Frank Pfenning