Lars Birkedal

Developing Theories of Types and Computability via Realizability Degree Type: Ph.D. in Computer Science
Advisor(s): Dana Scott
Graduated: December 1999

Abstract:

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#).

Thesis Committee:
Dana S. Scott (Chair)
Steven Awodey
Stephan Brookes
John C. Reynolds
Giuseppe Rosolini (Università di Genova, Italy)

Randy Bryant, Head, Computer Science Department
James Morris, Dean, School of Computer Science

Keywords:
Semantics, logic, type theory, category theory, realizability