×

Full abstraction for PCF. (English) Zbl 1006.68028

Summary: 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 striking 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 [see J. M. E. Hyland and C.-H. L. Ong, ibid. 163, No. 2, 285-408 (2000; Zbl 1006.68027), above].) 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.

MSC:

68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
03D20 Recursive functions and relations, subrecursive hierarchies
18C50 Categorical semantics of formal languages
18D20 Enriched categories (over closed or monoidal categories)
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q55 Semantics in the theory of computing
03B70 Logic in computer science
91A80 Applications of game theory

Citations:

Zbl 1006.68027
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Abadi, M.; Plotkin, G., A PER model of polymorphism and recursive types, Proceedings, fifth annual IEEE symposium on logic in computer science, (1990), IEEE Computer Society Press Los Alamitos
[2] Abramsky, S., Proofs as processes, Theoret. comput. sci., 135, 5-9, (1994) · Zbl 0850.68297
[3] Abramsky, S, and, Jagadeesan, R. 1993, Game semantics for exponentials, Announcement on the types mailing list.
[4] Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, J. symbolic logic, 59, 543-574, (1994) · Zbl 0822.03007
[5] Abramsky, S.; Jung, A., Domain theory, (), 1-168
[6] Abramsky, S.; Jagadeesan, R.; Malacaria, P., Full abstraction for PCF (extended abstract), (), 1-15 · Zbl 0942.68615
[7] Abramsky, S.; McCusker, G., Games and full abstraction for the lazy λ-calculus, Proceedings, tenth annual IEEE symposium on logic in computer science, (1995), IEEE Computer Society Press Los Alamitos, p. 234-243
[8] Abramsky, S.; McCusker, G., Game semantics, (), 1-56 · Zbl 0961.68080
[9] Abramsky, S., Games in the semantics of programming languages, Proceedings of the 1997 Amsterdam colloquium, (1997)
[10] Abramsky, S., Axioms for definability and full completeness, (), 55-75
[11] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[12] Berry, G., Modèles complètement adéquats et stable de lambda-calculs, (1976), Université Paris VII
[13] Berry, G.; Curien, P.-L., Sequential algorithms on concrete data structures, Theoret. comput. sci., 20, 265-321, (1982) · Zbl 0497.68012
[14] Berry, G.; Curien, P.-L.; Lévy, J.-J., Full abstraction for sequential languages: the state of the art, Algebraic semantics, (1985), Cambridge University Press Cambridge, p. 89-132 · Zbl 0604.68033
[15] Bucciarelli, A.; Ehrhard, T., Extensional embedding of a strongly stable model of PCF, Proc. ICALP, Lecture notes in computer science, 510, (1991), Springer-Verlag Berlin/New York, p. 35-46 · Zbl 0786.68053
[16] Cartwright, R.; Felleisen, M., Observable sequentiality and full abstraction, Proc. POPL, (1992), Assoc. Comput. Mach New York, p. 328-342
[17] Crole, R., Categories for types, (1994), Cambridge University Press Cambridge
[18] Curien, P.-L., Observable sequential algorithms on concrete data structures, (), 432-443
[19] Curien, P.L., Sequentiality and full abstraction, (), 66-94 · Zbl 0798.68098
[20] Curien, P.-L., Categorical combinators, sequential algorithms and functional programming, (1993), Progress in Theoretical Computer Science Birkhäuser · Zbl 0814.68085
[21] Davey, D.A.; Priestley, H.A., Introduction to lattices and order, (1990), Cambridge University Press Cambridge · Zbl 0701.06001
[22] Ehrhard, T., Projecting sequential algorithms on the strongly stable functions, Ann. pure appl. logic, 77, 201-244, (1996) · Zbl 0852.68027
[23] Gandy, R. O. 1993, Dialogues, Blass Games and Sequentiality for Objects of Finite Type, unpublished manuscript.
[24] Ghica, D.R.; McCusker, G., Reasoning about idealized algol using regular languages, Proceedings of ICALP 2000, Lecture notes in computer science, (2000), Springer-Verlag Berlin/New York · Zbl 0973.68506
[25] Girard, J.-Y., Geometry of interaction 2: deadlock-free algorithms, (), 76-93
[26] Girard, J.-Y., Geometry of interaction 1: interpretation of system F, (), 221-260
[27] Girard, J.-Y., Towards a geometry of interaction, (), 69-108
[28] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs · Zbl 0637.68007
[29] Jung, A.; Stoughton, A., Studying the fully abstract model of PCF within its continous function model, Proc. int. conf. typed lambda calculi and applications, Lecture notes in computer science, 664, (1993), Springer-Verlag Berlin, p. 230-245 · Zbl 0788.68021
[30] Loader, R., Finitary PCF is undecidable, Theoret. comput. sci., (2000) · Zbl 0992.68017
[31] Lorenzen, P., Logik und agon, Atti del congresso internazionale di filosofia, (1960), Firenze Sansoni, p. 187-194
[32] Lorenzen, P., Ein dialogisches konstruktivitätskriterium, Infinitistic methods, Proceed. symp. foundations of math., (1961), PWN Warszawa, p. 193-200 · Zbl 0117.01303
[33] Malacaria, P., Dalle macchine a ambienti alla geometria dell’interazione, (1993)
[34] Malacaria, P.; Hankin, C., Non-deterministic games and program analysis: an application to security, Proceedings of lics ’99, (1999), p. 443-453
[35] Manes, E., Algebraic theories, Graduate texts in mathematics, 26, (1976), Springer-Verlag Berlin/New York
[36] Milner, R., Fully abstract models of typed lambda-calculi, Theoret. comput. sci., 4, 1-22, (1977) · Zbl 0386.03006
[37] Mulmuley, K., Full abstraction and semantic equivalence, (1987), MIT Press Cambridge
[38] Nickau, H., Hereditarily sequential functionals, Proceedings of the symposium on logical foundations of computer science: logic at Saint |St. Petersburg, Lecture notes in computer science, (1994), Springer-Verlag Berlin/New York · Zbl 0946.03053
[39] O’Hearn, P.W.; Riecke, J.G., Kripke logical relations and PCF, Inform. and comput., 120, 107-116, (1995) · Zbl 0912.03008
[40] Plotkin, G., LCF considered as a programming language, Theoret. comput. sci., 5, 223-255, (1977) · Zbl 0369.68006
[41] Soare, R.I., Recursively enumerable sets and degrees, Perspectives in mathematical logic, (1987), Springer-Verlag Berlin
[42] Stoughton, A., Fully abstract models of programming languages, (1988), Pitman London · Zbl 0702.68018
[43] Winskel, G., The formal semantics of programming languages, Foundations of computing, (1999), MIT Press Cambridge
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.