Full Abstraction of PCF and Related Languages
A Collection of Literature
Mon Dec 11 10:14:02 MET 1995
Initiated from a workshop of the same
This document is also available as
Antonio Bucciardelli and Thomas Ehrhard.
Sequentiality in an extensional framework.
Information and Computation, 110:265--296, 1994.
Abstract: We present a cartesian closed category of
dI-domains with coherence and strongly stable functions which
provides a new model of PCF, where terms are interpreted by functions
and where, at first order, all functions are sequential.
how this model can be refined in such a way that the theory it induces on the
terms of PCF be strictly finer than the theory induced by the Scott model of
Comments: ISSN: 0890-540
Authors addresses: LIENS - DMI,
Ecole Normale Supérieure, 45 rue d'Ulm, 75230 Paris Cédex, France.
IGM, Université de Marne-la-Vallée, 2 rue
de la Butte Verte, 93166 Noisy-le-Grand Cédex, France.
Steven Brookes and Shai Geva.
Stable and sequential functions on Scott domains.
Submitted for publication.
Abstract: The search for a general semantic characterization of
sequential functions is motivated by the full abstraction problem for
sequential programming languages such as PCF. We present here some new
developments towards such a theory of sequentiality. We give a general
definition of sequential functions on Scott domains, characterized by means
of a generalized form of topology, based on sequential open sets. Our notion
of sequential function coincides with the Kahn-Plotkin notion of sequential
function when restricted to distributive concrete domains, and considerably
expands the class of domains for which sequential functions may be defined.
We show that the sequential functions between two dI-domains, ordered stably,
form a dI-domain. The analogous property fails for Kahn-Plotkin sequential
functions. Our category of dI-domains and sequential functions is not
cartesian closed, because application is not sequential. We attribute this to
certain operational assumptions underlying our notion of sequentiality. We
show that the Scott domains satisfying a certain ``finite meet'' property are
closed under the pointwise-ordered stable function space, so that we obtain a
new stable model based on the pointwise order. We discuss some issues arising
in the search for a class of domains closed under the pointwise-ordered
sequential function space.
We discuss the relationship between our ideas
and the full abstraction problem for PCF, and indicate directions for further
Steven Brookes and Shai Geva.
Sequential functions on indexed domains and full abstraction for
a sub-language of PCF.
In Mathematical Foundations of Programming Semantics,
Proceedings of the Ninth International Conference, MFPS '93, New Orleans,
April 1993. Lecture Notes in Computer Science, vol 802. Springer-Verlag.
Abstract: We present a general semantic framework of sequential
functions on domains equipped with a parameterized notion of incremental
sequential computation. Under the simplifying assumption that computation
over function spaces proceeds by successive application to constants, we
construct a sequential semantic model for a non-trivial sub-language of PCF
with a corresponding syntactic restriction --- that variables of function
type may only be applied to closed terms. We show that the model is fully
abstract for the sub-language, with respect to the usual notion of program
Hypercoherences: a strongly stable model of linear logic.
MSCS - Mathematical Structures in Computer Science,
Slightly changed version.
Abstract: We present a model of classical linear logic based on
the notion of strong stability that was introduced in [BE], a work
about sequentiality written jointly with Antonio Bucciarelli.
- A. Bucciarelli, T. Ehrhard. Sequentiality and strong stability.
Proc. LICS 1991.
Comments: ISSN: 0960-1295
Authors address: Laboratoire
de Math'ematiques Discrètes, UPR 9016 du CNRS, 163 avenue de Luminy,
case 930, F 13288 MARSEILLE CEDEX 9. email@example.com.
Projecting sequential algorithms on strongly stable functions.
44 pp. To appear in Annals of Pure and Applied Logic, 1994.
Abstract: We relate two sequential models of PCF: the
sequential algorithm model due to Berry and Curien and the strongly stable
model due to Bucciarelli and the author. More precisely, we show that
all the morphisms arising in the strongly stable model of PCF are
sequential in the sense that they are the ``extensional projections'' of some
sequential algorithms. We define a model of PCF where morphisms are
``extensional'' sequential algorithms and prove that any equation between PCF
terms which holds in this model also holds in the strongly stable model.
Comments: Authors address: Laboratoire de Math'ematiques
Discrètes, UPR 9016 du CNRS, 163 avenue de Luminy, case 930, F 13288
MARSEILLE CEDEX 9. firstname.lastname@example.org.
J. Martin E. Hyland and C.-H. Luke Ong.
On full abstraction for PCF: I, II and III (preliminary
109 pp, 1994.
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
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
- 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
- G. Berry and P.-L. Curien.
Sequential algorithms on concrete data structures.Theoretical Computer
Science, 20:265--321, 1982.
- R. O. Gandy. Dialogues, blass
games, sequentiality for objects of finite type. unpublished manuscript,
- 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.
- 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:
J. Martin E. Hyland and C.-H. Luke Ong.
Pi-calculus, dialogue games and PCF.
In Proceedings of 7th Annual ACM Conference on Functional
Programming Languages and Computer Architecture (La Jolla, California,
June 26--28, 1995). ACM - Association for Computing Machinery, 1995.
Abstract: Game semantics is an unusual denotational semantics
in that it captures the intensional (or algorithmic) and dynamical aspects of
the computation. This makes it an ideal semantical framework in which to seek
to unify analyses of both the qualitative (correctness) as well as the
quantitative (efficiency) properties of programming languages. This paper
reports work arising from a recent construction of an order (or
inequationally) fully abstract model for Scott's functional programming
language PCF based on a kind of two-person (Player and Opponent)
dialogue game of questions and answers [HO94]. In this model types are
interpreted as games and terms as innocent strategies. The fully abstract
game model may be said to be canonical for the semantical analysis of
sequential functional languages. Unfortunately even for relatively simple
PCF-terms, precise description of their denotations as strategies in
[HO94] very rapidly becomes unwieldy and opaque. What is needed to remedy the
situation is an expressive formal language which lends itself to a succinct
and economical representation of innocent strategies. In this paper we give
just such a representation in terms of an appropriately sorted polyadic
-calculus, reading input -actions as Opponent's moves, and output
-actions as Player's moves. This correspondence captures every essential
aspect of the dialogue game paradigm so precisely that the
-representation may as well be taken to be the basis for its formal
definition. Although the -representation of strategies already gives an
encoding of PCF in the -calculus --- indirectly via the fully
abstract denotation of PCF-terms as innocent strategies, we define by
recursion a new encoding of PCF in the -calculus directly. The two
-encodings of PCF are weakly bisimilar; if the latter is regarded
as a compilation, then the former amounts to a more efficient version with
- J. M. E. Hyland
and C.-H. L. Ong. On full abstraction for PCF: I, II and III. preliminary
version, 110 pages, ftp-able at theory.doc.ic.ac.uk in directory papers/Ong,
1994. Alternatively get it, [HO94], here.
Comments: Authors addresses: DPMMS, University of Cambridge, 16
Mill Lane, Cambridge, CB2 1SB ENGLAND
Oxford University Computing
Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD ENGLAND and DISCS,
National University of Singapore.
Abstract: Lambda, a program for solving lambda definability
problems of order at most two.
Fully Abstract Models of Programming Languages, chapter
Preface, Introduction, Bibliography and Index, pages i--iv, 1--7 and
Research Notes in Theoretical Computer Science. Pitman, 1988.
Abstract: From the preface: This monograph presents a
language-independent theory of fully abstract denotational semantics of
programming languages---models that identify program fragments exactly when
they are operationally interchangeable---and uses this theory to show the
existence or nonexistence of such models for several example programming
languages. It is intended for researchers in programming language semantics,
and is mathematically self-contained: only naive set theory and some very
basic notions of category theory are assumed. Some familiarity with universal
algebra and domain theory would be helpful, however.
Comments: School of Mathematical and Physical Sciences,
University of Sussex.
Equationally fully abstract models of PCF.
In Michael Main, Austin Melton, Michael Mislove, and David Schmidt,
editors, Mathematical Foundations of Programming Semantics: 5th
International Conference (Tulane University, New Orleans, Louisiana,
1989, March/April), number 442 in Lecture Notes in Computer Science, pages
271--283, Berlin, 1990. Springer-Verlag.
Abstract: From the introduction: The paper's main results are
- E is a pre-ordering with
arbitrary products and coproducts and whose initial a nd terminal objects are
- All objects of E are strongly algebraic
(SFP) and all isolated elements of these models are definable by terms.
- There is a morphism from an object A to an object
B of E iff B relates at least as many pairs of terms as does
A (i.e., if the meaning of M is less than that of N in A,
then the meaning of M is less than that of N in B)
Objects of E that relate the same pairs of terms are isomorphic.
- The initial object of E is also initial in the category of
(not necessarily ex tensional) equationally fully abstract models.
- The terminal object of E is order-extensional and
inequationally fully abstract, i.e., is Milner's original model
Interdefinability of parallel operations in PCF.
Theoretical Computer Science - Journal of EATCS, 79:357--358,
Abstract: It is shown that the ``parallel or'' a nd ``parallel
conditional'' operations are interdefinable elements of the continuous
function model of the programming language PCF.
Comments: ISSN: 0304-3975
Authors address: Computer
Science and Artificial Intelligence, School of Cognitive and Computing
Sciences, University of Sussex, Falmer, Brighton BN1 9QH, England.
Parallel PCF has a unique extensional model.
In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer
Science, pages 146--151, Amsterdam, The Netherlands, July 15--18 1991. IEEE
Computer Society Press.
Abstract: We show that the continuous function model is the
unique extensional (but not necessarily pointwise ordered) model of the
variant of the applied typed lambda calculus PCF that includes the ``parallel
Comments: IEEE Computer Society Order Number 2230; Library of
Congress Number 89-641304; IEEE Catalog Number 91CH3025-4; ISBN
Authors address: Computer Science and Artificial
Intelligence, School of Cognitive and Computing Sciences, University of
Sussex, Falmer, Brighton BN1 9QH, England.
Studying the fully abstract model of PCF within its continuous
In Marc Bezem and Jan Friso Groote, editors, Typed Lambda
Calculi and Applications: International Conference on Typed Lambda Calculi
and Applications, TLCA '93 (Utrecht, The Netherlands, 1993, March
16-18), number 664 in Lecture Notes in Computer Science, pages 230--244,
Berlin, 1993. Springer-Verlag.
Abstract: We give a concrete presentation of the inequationally
fully abstract model of PCF as a continuous projection of the inductively
reachable subalgebra of PCF's continuous function model.
Comments: ISBN: 3-540-56517-5 / 0-387-56517-5
addresses: Fachbereich Mathematik, Technische Hochschule Darmstadt,
Schloßgartenstraße 7, D-6100 Darmstadt, Germany, e-mail:
School of Cognitive and Computing Sciences,
University of Sussex, Falmer, Brighton BN1 9QH, UK, e-mail:
Mechanizing logical relations.
In Stephen Brookes et al., editors, Mathematical Foundations of
Programming Semantics: 9th International Conference proceedings (New
Orleans, LA, USA, 1993, April 7--10), number 802 in Lecture Notes in
Computer Science, pages 359--377, Berlin, 1994. Springer-Verlag.
Abstract: We give an algorithm for deciding whether there
exists a definable element of a finite model of an applied typed lambda
calculus that passes certain tests, in the special case when all the
constants and test arguments are of order at most one. When there is such an
element, the algorithm outputs a term that passes the tests; otherwise, the
algorithm out puts a logical relation that demonstrates the nonexistence of
such an element. Several example applications of the C implementation of this
algorithm are considered.
Comments: ISBN: 3-540-58027-1 / 0-387-58027-1
address: Department of Computing and Information Sciences, Kansas State
University, Manhattan, KS 66506, USA. E-mail:email@example.com.
BRICS WWW home page