Code-free Recursion & Realizability

Abstract

This thesis is an elaborate account of the theory of partial combinatory algebras (pcas) and their associated categorical structures called categories of assemblies and realizability toposes. From the viewpoint of "abstract Turing machines'', we build up the theory of pcas, generalizing some constructions from ordinary recursion theory, such as relative computability in an oracle (of type 1 and higher). In later chapters, we show how this notion of generalized relative computability can be used to study realizability toposes, with special attention to the effective topos. We also treat geometric morphisms between realizability toposes, and fill in a gap in the theory of applicative morphisms (morphisms between pcas) in relation to geometric morphisms.