On full abstraction for PCF: I, II, and III

Journal article

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 S. C Kleene (1978, in “General Recursion Theory II, Proceedings of the 1977 Oslo Symposium,” North-Holland, Amsterdam) and R. O. Gandy (1993, “Dialogues, Blass Games, Sequentiality for Objects of Finite Type,” unpublished manuscript) in one tradition, and to G. Kahn and G. D. Plotkin (1993, Theoret. Comput. Sci. 121, 187–278) and G. Berry and P.-L. Curien (1982, Theoret. Comput. Sci. 20, 265–321) 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:

1. 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.
2. 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 analyze PCF-style computations directly in terms of partial strategies based on the information available to each player when he or she 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.

Authors: Hyland, J; Ong, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Academic Press
• Journal: Information and Computation
• Volume: 163
• Issue: 2
• Pages: 285-408
• Publication date: 2000-12-01
• Edition: Publisher's version
• DOI: 10.1006/inco.2000.2917
• ISSN: 0890-5401
• Language: English
• Subjects: Computer science (mathematics); Game semantics