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

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

1 Introduction

Programming languages combining higher order features with the manipulation of local state present severe problems for the traditional techniques of programming language semantics and logics of programs. For denotational semantics, the problems manifest themselves as a lack of abstraction in existing semantic models: some expressions that are observationally equivalent (i.e. that can be interchanged in any program without affecting its behaviour when executed) are assigned different denotations in the model. For operational semantics, the problems manifest themselves partly in the fact that simple techniques for analyzing observational equivalence in the case of purely functional languages (such as Milner's `Context Lemma' [9], or more generally, notions of applicative bisimulation [1]) break down in the presence of state-based features. Furthermore, operationally based approaches to properties of programs are often inconveniently intensional, e.g. the familiar congruence properties of equational logic fail to hold. (See [7, Sect. 5(A)], for example.) These problems have been intensively studied for the case of local variables in block-structured, Algol-like languages and to a lesser extent for the case of languages involving the dynamic creation of mutable locations (such as ML-style references). See [20, 2, 8, 3, 21, 15, 16, 7, 4]. Our interest in this subject stems primarily from a desire to improve and deepen the techniques which are available for reasoning about program behaviour in the `impure' functional language Standard ML [10].

Our motivation here is to try to identify what, if any, are the difficulties created purely by locality of state, independent of other properties such as side-effects, exceptional termination and non-termination due to recursion. Accordingly we consider higher order functions which can dynamically create fresh names of things, but ignore completely what kind of thing (references, exceptions, etc.) is being named. Names are created with local scope, can be tested for equality, and are passed around via function application, but that is all. Because of this limited framework, there is some hope of obtaining definitive results|fully abstract models and complete proof techniques. As the vehicle for this study we formulate an extension of the call-by-value, simply typed lambda calculus, called the nu-calculus and introduced in Sect. 2. In ML terms, it contains higher order functions over ground types bool and unit ref|the latter being the type of dynamically created references to the unique element of type unit. This acts as a type of `names' because only one thing can be (and is) stored in such a reference, so that its only characteristic is its name. We have purposely excluded recursion from the nu-calculus and as a result any closed expression evaluates to an essentially unique canonical form. Indeed, the nucalculus appears at first sight to be an extremely simple system. On closer inspection, we find that nu-calculus expressions can exhibit very subtle behaviour with respect to an appropriate notion of observational equivalence. Thus our first contribution is somewhat in the spirit of Meyer and Seiber [8]: we observe that even for this extremely simple case of local state there are observationally equivalent expressions which traditional denotational techniques will fail to identify (Example 2.8).

In Sect. 3 we introduce a notion of `logical relation' for the nu-calculus incorporating a version of representation independence for local names. Our technique is a syntactic version of the relationally parametric semantics of O'Hearn and Tennent [16]. There are also interesting similarities with Plotkin and Abadi's parametricity schema for existential types [19, Theorem 7]. We use our version of logical relations to establish the termination properties of the nu-calculus (Theorem 3.3) and to provide a useful, notion of `applicative' equivalence between nu-calculus expressions which implies observational equivalence (The-