Developing Theories of Types and Computability via Realizability
Abstract
We investigate the development of theories of types and computability via realizability. In the first part of the thesis, we suggest a general notion of realizability, based on weakly closed partial cartesian categories, which generalizes the usual notion of realizability over a partial combinatory algebra. We show how to construct categories of so-called assemblies and modest sets over any weakly closed partial cartesian category and that these categories of assemblies and modest sets model dependent predicate logic, that is, first-order logic over dependent type theory. We further characterize when a weakly closed partial cartesian category gives rise to a topos. Scott's category of equilogical spaces arises as a special case of our notion of realizability namely as modest sets over the category of algebraic lattices. Thus as a consequence, we conclude that the category of equilogical spaces models dependent predicate logic; we include a concrete description of this model. In the second part of the thesis, we study a notion of relative computability, which allows one to consider computable operations operating on not necessarily computable data. Given a partial combinatory algebra A, which we think of as continuous realizers, with a subalgebra a is subset of A which we think of as computable realizers, there results a realizability topos RT(A, a), which one intuitively can think of as having continuous objects and computable morphisms. We study the relationship between this topos and the standard realizability toposes RT(A) and RT(a) over A and RT(a). In particular, we show that there is a localic local map of toposes from RT(A, a) to RT(a). To obtain a better understanding of the relationship between the internal logics of RT(A, a) and RT(a), we then provide a complete axiomatization of arbitrary local maps of toposes.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 28, 1999
- Accession Number
- ADA373423
Entities
People
- Lars Birkedal
Organizations
- Carnegie Mellon University