page 2  (60 pages)
to previous section1
3to next section

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

3 Intensional Full Abstraction 24

3.1 PCFc : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 24
3.2 Evaluation Trees : : : : : : : : : : : : : : : : : : : : : : : : : : : 24
3.3 The Bang Lemma : : : : : : : : : : : : : : : : : : : : : : : : : : 25
3.4 The Decomposition Lemma : : : : : : : : : : : : : : : : : : : : : 27
3.5 Approximation Lemmas : : : : : : : : : : : : : : : : : : : : : : : 35
3.6 Main Results : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 37

4 Extensional Full Abstraction 41

4.1 The Intrinsic Preorder : : : : : : : : : : : : : : : : : : : : : : : : 41
4.2 The Extensional Category : : : : : : : : : : : : : : : : : : : : : 46
4.3 An alternative view of E : : : : : : : : : : : : : : : : : : : : : : : 47
4.4 Full Abstraction : : : : : : : : : : : : : : : : : : : : : : : : : : : 48

5 Universality 49

5.1 Recursive Strategies : : : : : : : : : : : : : : : : : : : : : : : : : 50
5.2 Universal Terms : : : : : : : : : : : : : : : : : : : : : : : : : : : 51

1 Introduction

The Full Abstraction Problem for PCF [Plo77, Mil77, BCL85, Cur92b] is one of the longest-standing problems in the semantics of programming languages. There is quite widespread agreement that it is one of the most difficult; there is much less agreement as to what exactly the problem is, or more particularly as to the precise criteria for a solution. The usual formulation is that one wants a semantic characterization" of the fully abstract model (by which we mean the inequationally fully abstract order-extensional model, which Milner proved to be uniquely specified up to isomorphism by these properties [Mil77]). The problem is to understand what should be meant by a semantic characterization".

Our view is that the essential content of the problem, what makes it important, is that it calls for a semantic characterization of sequential, functional computation at higher types. The phrase sequential functional computation" deserves careful consideration. On the one hand, sequentiality refers to a computational process extended over time, not a mere function; on the other hand, we want to capture just those sequential computations in which the different parts or modules" interact with each other in a purely functional fashion.

There have, to our knowledge, been just four models of PCF put forward as embodying some semantic analysis. Three are domain-theoretic: the standard model" based on Scott-continuous functions [Plo77]; Berry's bidomains model based on stable functions [Ber79]; and the Bucciarelli-Ehrhard model based on strongly stable functions [BE91]. The fourth is the Berry-Curien model based on sequential algorithms [BC82].1 Of these, we can say that the standard

1Cartwright and Felleisen's model without error values turns out to be equivalent to the sequential algorithms model [CF92, Cur92a]. The main result in [CF92, Cur92a] is that the sequential algorithms model with errors is fully abstract for SPCF, an extension of PCF with a catch construct and errors. This is a fine result, but SPCF has a rather different flavour to