Recursion and Sequentiality in Categories of Sheaves

TL;DR

This paper develops a fully abstract categorical model for a call-by-value language featuring higher-order functions, recursion, and natural numbers, emphasizing modularity over traditional domain-theoretic approaches.

Contribution

It introduces a novel categorical model as an exponential ideal in a topos, integrating recursion as a modular component rather than relying solely on cpo-based semantics.

Findings

Model achieves full abstraction for the language features.

Demonstrates modular construction of semantics.

Provides insights into categorical approaches to recursion.

Abstract

We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo's, we treat recursion as just one feature in a model built by combining a choice of modular components.