# Developing Theories of Types and Computability via Realizability

## PhD Thesis

### L. Birkedal

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