On full abstraction for PCF: I, II and III (preliminary
J. Martin E. Hyland
C.-H. Luke Ong
Available as PostScript.
We present an order-extensional, order (or inequationally) fully abstract
model for Scott's language PCF. The approach we have taken is very
concrete and in nature goes back to Kleene [Kle78] and Gandy [Gan93] in one
tradition, and to Kahn and Plotkin [KP93], and Berry and Curien [BC82] in
another. Our model of computation is based on a kind of game in which each
play consists of a dialogue of questions and answers between two players who
observe the following Principles of Civil Conversation:
We analyse PCF-style computations directly in terms of
partial strategies based on the information available to each player when
he is about to move. Our players are required to play an innocent
strategy: they play on the basis of their view which is that part
of the ``history'' that interests them currently. Views are continually
updated as the play unfolds. Hence our games are neither
history-sensitive nor history-free. Rather they are view-dependent. These
considerations give expression to what seems to us to be the nub of PCF-style higher-type sequentiality in a (dialogue) game-semantical
- Justification. A question is asked only if the dialogue at that
point ``warrants'' it. An answer is proffered only if a question expecting
it has already been asked.
- Priority. Questions pending in a dialogue are answered on a
``last asked first answered'' basis. This is equivalent to Gandy's ``no
dangling question mark'' condition.
- G. Berry and P.-L. Curien. Sequential algorithms on
concrete data structures.Theoretical Computer Science, 20:265--321, 1982.
- R. O. Gandy. Dialogues, blass games, sequentiality for
objects of finite type. unpublished manuscript, 1993.
- S. C. Kleene. Recursive functionals and quantifiers of
finite types revisited I. In J. E. Fenstad, R. O. Gandy, and G. E. Sacks,
editors,General Recursion Theory II, Proceedings of the 1977 Oslo
Symposium, pages 185--222. North-Holland, 1978.
- G. Kahn and G. D. Plotkin. Concrete domains. Theoretical
Computer Science, 1993. in Böhm Festschrift Special Issue. Article
first appeared (in French) as technical report 338 of INRIA-LABORIA, 1978.
Authors addresses: Department of Pure Mathematics and
Mathematical Statistics, University of Cambridge, 16 Mill Lane, Cambridge CB2
1SB, United Kingdom
Oxford University Computing Laboratory, Wolfson
Building, Parks Road, Oxford OX1 3QD, United Kingdom and Department of
Information Systems and Computer Science, National University of Singapore,
Lower Kent Ridge Road, Singapore 0511, Republic of Singapore. e-mail:
BRICS WWW home page