CONTINUE?

Expanding the text here will generate a large amount of data for your browser to display

Full Abstraction for PCF?

Samson Abramskyy Radha Jagadeesanz Pasquale Malacariax

December 7, 1995

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.

Contents

1 Introduction 2

2 The Model 5

2.1 Games : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6
2.2 Strategies : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7
2.3 Multiplicatives : : : : : : : : : : : : : : : : : : : : : : : : : : : : 9
2.4 The Category of Games : : : : : : : : : : : : : : : : : : : : : : : 10
2.5 G as an autonomous category : : : : : : : : : : : : : : : : : : : : 15
2.6 Products : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 16
2.7 Exponentials : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 17
2.8 The co-Kleisli category : : : : : : : : : : : : : : : : : : : : : : : : 19
2.9 Order-enrichment : : : : : : : : : : : : : : : : : : : : : : : : : : : 21
2.10 The model of PCF : : : : : : : : : : : : : : : : : : : : : : : : : : 22
?This research was supported by grants from UK SERC and ESPRIT Basic Research Action 6811 CLICS II". Radha Jagadeesan was supported in part by a grant from ONR. Pasquale Malacaria was supported in part by the HCM fellowship n. ERBCHBICT940947. yImperial College
zLoyola University
xImperial College