On full abstraction for PCF: I, II and III (preliminary version)

J. Martin E. Hyland
C.-H. Luke Ong

109 pp

Abstract:

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:
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.
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 setting.
[BC82]
G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures.Theoretical Computer Science, 20:265--321, 1982.
[Gan93]
R. O. Gandy. Dialogues, blass games, sequentiality for objects of finite type. unpublished manuscript, 1993.
[Kle78]
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.
[KP93]
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.

Comments:
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: lo@comlab.ox.ac.uk.

BRICS WWW home page