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.
We show 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 continuous functions.
Comments: ISSN: 0890-540
Authors addresses: LIENS - DMI, Ecole Normale Supérieure, 45 rue d'Ulm, 75230 Paris Cédex, France. e-mail:buccia@dmi.ens.fr
IGM, Université de Marne-la-Vallée, 2 rue de la Butte Verte, 93166 Noisy-le-Grand Cédex, France. e-mail:ehrhard@dmi.ens.fr.
Steven Brookes and Shai Geva.
Stable and sequential functions on Scott domains.
June 1992.
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 development.
Steven Brookes and Shai Geva.
Sequential functions on indexed domains and full abstraction for a sub-language of PCF.
1993.
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 behavior.
Thomas Ehrhard.
Hypercoherences: a strongly stable model of linear logic.
MSCS - Mathematical Structures in Computer Science, 2:365--385, 1993.
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.
- [BE]
- 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. ehrhard@lmd.univ-mrs.fr.
Thomas Ehrhard.
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. ehrhard@lmd.univ-mrs.fr.
J. Martin E. Hyland and C.-H. Luke Ong.
On full abstraction for PCF: I, II and III (preliminary version).
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 Conversation:
- 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 mark'' condition.
- [BC82]
- G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures.Theoretical Computer Science, 20:265--321, 1982.
- [Gan93]
- R. O. Gandy. Dialogues, blass games, sequentiality for objects of finite type. unpublished manuscript, 1993.
- [Kle78]
- 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.
- [KP93]
- 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: lo@comlab.ox.ac.uk.
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
compile-time optimization. - [HO94]
- 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.
Allen Stoughton.
Lambda.
Abstract: Lambda, a program for solving lambda definability problems of order at most two.
Allen Stoughton.
Fully Abstract Models of Programming Languages, chapter Preface, Introduction, Bibliography and Index, pages i--iv, 1--7 and 119--123.
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.
Allen Stoughton.
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 as follows:
- (i)
- E is a pre-ordering with arbitrary products and coproducts and whose initial a nd terminal objects are not isomorphic.
- (ii)
- All objects of E are strongly algebraic (SFP) and all isolated elements of these models are definable by terms.
- (iii)
- 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)
- (iv)
- Objects of E that relate the same pairs of terms are isomorphic.
- (v)
- The initial object of E is also initial in the category of (not necessarily ex tensional) equationally fully abstract models.
- (vi)
- The terminal object of E is order-extensional and
inequationally fully abstract, i.e., is Milner's original model
Allen Stoughton.
Interdefinability of parallel operations in PCF.
Theoretical Computer Science - Journal of EATCS, 79:357--358, 1991.
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.
Allen Stoughton.
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 or'' operation.
Comments: IEEE Computer Society Order Number 2230; Library of Congress Number 89-641304; IEEE Catalog Number 91CH3025-4; ISBN 0-8186-2230-X
Authors address: Computer Science and Artificial Intelligence, School of Cognitive and Computing Sciences, University of Sussex, Falmer, Brighton BN1 9QH, England.
Allen Stoughton.
Studying the fully abstract model of PCF within its continuous function model.
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
Authors addresses: Fachbereich Mathematik, Technische Hochschule Darmstadt, Schloßgartenstraße 7, D-6100 Darmstadt, Germany, e-mail: jung@mathematik.th-darmstadt.de
School of Cognitive and Computing Sciences, University of Sussex, Falmer, Brighton BN1 9QH, UK, e-mail: allen@cogs.sussex.ac.uk.
Allen Stoughton.
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.
Corrected version.
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
Authors address: Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA. E-mail:allen@cis.ksu.edu.
![[BRICS symbol]](http://www.daimi.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page