Bistable Biorders: A Sequential Domain Theory

TL;DR

This paper introduces bistable biorders, a new order-theoretic framework for modeling sequential functions, proving universality and full abstraction results for the simply-typed lambda calculus and SPCF language.

Contribution

It presents the novel concept of bistable biorders and demonstrates their effectiveness in modeling sequential computation and establishing universality and full abstraction.

Findings

Bistable biorders form a Cartesian closed category of sequential functions.

Monotone and bistable functions are strongly sequential.

The semantics of SPCF is shown to be fully abstract.

Abstract

We give a simple order-theoretic construction of a Cartesian closed category of sequential functions. It is based on bistable biorders, which are sets with a partial order -- the extensional order -- and a bistable coherence, which captures equivalence of program behaviour, up to permutation of top (error) and bottom (divergence). We show that monotone and bistable functions (which are required to preserve bistably bounded meets and joins) are strongly sequential, and use this fact to prove universality results for the bistable biorder semantics of the simply-typed lambda-calculus (with atomic constants), and an extension with arithmetic and recursion. We also construct a bistable model of SPCF, a higher-order functional programming language with non-local control. We use our universality result for the lambda-calculus to show that the semantics of SPCF is fully abstract. We then establish a direct correspondence between bistable functions and sequential algorithms by showing that sequential data structures give rise to bistable biorders, and that each bistable function between such biorders is computed by a sequential algorithm.