[Prev][Next][Index][Thread]
Full abstraction for PCF
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
A complete version of the paper
"Full Abstraction for PCF"
by S.Abramsky, R.Jagadeesan and P.Malacaria
is now available by anonymous ftp at Imperial
ftp theory.doc.ic.ac.uk
Name: anonymous
Password: <<your e-mail address>>
ftp> cd papers/Malacaria
ftp> binary
ftp> get PCFfullabs.dvi.Z
(or ftp> get PCFfullabs.ps.Z)
ftp> quit
====ABSTRACT====
An intensional model for the programming language PCF is described, in
which the types of PCF are interpreted by games, and the terms by
certain ``history-free'' strategies.
This model is shown to capture definability in PCF. More precisely,
every compact strategy in the model is definable
in a certain simple extension of PCF. We then introduce an intrinsic
preorder on strategies, and show that it
satisfies some remarkable properties, such that the intrinsic preorder
on function types coincides with the pointwise preorder. We then obtain
an order-extensional fully abstract model of PCF by quotienting the
intensional model by the intrinsic preorder. This is the first
syntax-independent description of the fully abstract model for PCF.
(Hyland and Ong have obtained very similar results by a somewhat
different route, independently and at the
same time.) We then consider the effective version of our model, and
prove a Universality Theorem: every element of the effective extensional
model is definable in PCF. Equivalently, every recursive strategy is
definable up to observational equivalence.