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#, 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 modal logic for computability. Moreover, we characterize some interesting subcategories of RT(A,A#) (in much the same way as assemblies and modest sets are characterized in standard realizability toposes) and show the validity of some logical principles in RT(A,A#).

292 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu