Partial Combinatory Algebras of Functions

TL;DR

This paper introduces new partial combinatory algebra structures on functions using sequential functions and interrogation, analyzing their properties and relationships with realizability toposes.

Contribution

It defines novel partial combinatory algebra structures on functions and explores their categorical properties and connections to realizability toposes.

Findings

Every realizability topos is a quotient of a topos on a total combinatory algebra

New partial combinatory algebra structures are constructed using sequential functions and interrogation

Analysis of these structures within Longley's preorder-enriched category

Abstract

We employ the notions of `sequential function' and `interrogation' (dialogue) in order to define new partial combinatory algebra structures on sets of functions. These structures are analyzed using J. Longley's preorder-enriched category of partial combinatory algebras and decidable applicative structures. We also investigate total combinatory algebras of partial functions. One of the results is, that every realizability topos is a quotient of a realizability topos on a total combinatory algebra.