Laird, James - Bistable Biorders: A Sequential Domain Theory

lmcs:2222 - Logical Methods in Computer Science, May 15, 2007, Volume 3, Issue 2
Bistable Biorders: A Sequential Domain Theory

Authors: Laird, James

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.

Source :
DOI : 10.2168/LMCS-3(2:5)2007
Volume: Volume 3, Issue 2
Published on: May 15, 2007
Submitted on: December 20, 2005
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,F.3.2


Consultation statistics

This page has been seen 49 times.
This article's PDF has been downloaded 46 times.