Jim Laird

Bidomains were introduced over twenty years ago by Berry in an attempt

to characterize sequentiality in a domain theoretic setting via the

notion of stability. Unfortunately, as is well known, the bidomain

model of PCF --- the protypical typed, sequential functional language

--- is not fully abstract because, like the Scott model, it contains

non-definable "junk". Moreover, there is no solution to the full

abstraction problem for PCF which is effectively presentable.

However, I shall argue that bidomains do give a precise and effective

characterization of sequentiality in an untyped setting, with

intensional representation of data (e.g. the Church numerals). The

basis for this claim is a proof that the "canonical" bidomain models

of the (untyped) lazy lambda-calculus and the call-by-value

lambda-calculus are fully abstract, as well as being effectively

presentable.

I shall describe these models, and sketch the proof of full

abstraction, which consists of a reduction to the problem of showing

definability of all elements of the bidomain model of unary PCF, and
a

proof of the latter fact based on an algorithm devised by

Schmidt-Schauss.