| |
VOLUME 3, ISSUE 2, PAPER 5
|
Bistable Biorders: A Sequential Domain Theory
|
©James Laird, University of Sussex
|
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.
|
Publication date: May 15, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(2:5)2007
Hit Counts: 2371 |
 Creative Commons | |
