Fully abstract bidomain models of the lambda-calculus.

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.