CMU-CS-99-173Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-99-173
Lars Birkedal December 1999 Ph.D. Thesis Temporarily Unavailable Electronically
CMU-CS-99-173.ps
Keywords: Semantics, logic, type theory, category theory, 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#, which we
think of as computable realizers, there results a realizability topos
RT(A,A#), which one intuitively can think of as having ``continous objects
and computable morphisms''. We study the relationship between this topos
and the standard realizability toposes RT(A) and RT(A#) over A and 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, a new result in
topos theory. Based on this axiomatization we investigate the relationship
between the internal logics of two toposes connected via a local
map. Moreover, we suggest a modal logic for local maps. Returning to the
realizability models we show in particular that the modal logic for local
maps in the case of RT(A,A#) and RT(A#) can be seen as a 292 pages
| |

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