Developing theories of types and computability via realizability

Research output: Book/anthology/dissertation/reportBook

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. 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#). This book is a slight revision of the author's Ph.D. thesis, written at Carnegie Mellon University, Pittsburgh, under the guidance of Prof. Dana S. Scott. This book is available in two formats: pdf and postscript. The pdf version has active hyper-references. May 23, 2000 Lars Birkedal
Original languageEnglish
PublisherElsevier
DOIs
Publication statusPublished - 1 Dec 2000
Externally publishedYes
SeriesElectronic Notes in Theoretical Computer Science
Volume34
ISSN1571-0661

See relations at Aarhus University Citationformats

ID: 81389922