Neither Miranda, Standard ML nor the enriched λ-calculus has an explicit distinction between kinds of binding times. However, for higher-order functions we can distinguish between the parameters that are available and those that are not. In standard compiler terminology this corresponds to the distinction between compile-time and run-time. The idea is now to capture this implicit distinction between binding times and then to annotate the operations of the enriched λ-calculus accordingly.

In this chapter we present such a development for the enriched λ-calculus by defining a so-called 2-level λ-calculus. To be precise, Section 3.1 first presents the syntax of the 2-level λ-calculus and the accompanying explanations indicate how it may carry over to more than two levels or a base language different from the typed λ-calculus. Next we present well-formedness conditions for 2-level λ-expressions and again we sketch the more general setting. Of the many well-formedness definitions that are possible we choose one that interacts well with the approach to combinator introduction to be presented in Chapter 4. Section 3.2 then studies how to transform binding time information (in the form of 2-level types) into an already typed λ-expression. This transformation complements the transformation developed in Section 2.2.

The 2-Level λ-Calculus

We shall use the types of functions to record when their parameters will be available and their results produced.

The functional programming style is closely related to the use of higher-order functions. In particular, it suggests that many function definitions are instances of the same general computational pattern and that this pattern is defined by a higher-order function. The various instances of the pattern are then obtained by supplying the higher-order function with some of its arguments.

One of the benefits of this programming style is the reuse of function definitions and, more importantly, the reuse of properties proved to hold for them: usually a property of a higher-order function carries over to an instance by verifying that the arguments satisfy some simple properties.

One of the disadvantages is that the efficiency is often rather poor. The reason is that when generating code for a higher-order function it is impossible to make any assumptions about its arguments and to optimize the code accordingly. Furthermore, conventional machine architectures make it rather costly to use functions as data.

We shall therefore be interested in transforming instances of higher-order functions into functions that can be implemented more efficiently. The key observation in the approach to be presented here is that an instance of a higher-order function is a function where some of the arguments are known and others are not. To be able to exploit this we shall introduce an explicit distinction between known and unknown values or, using traditional compiler terminology, between compile-time entities and run-time entities.

In this monograph we motivate and provide theoretical foundations for the specification and implementation of systems employing data structures which have come to be known as feature structures. Feature structures provide a record like data structure for representing partial information that can be expressed in terms of features or attributes and their values. Feature structures are inherently associative in nature, with features interpreted as associative connections between domain objects. This leads to natural graph-based representations in which the value of a feature or attribute in a feature structure is either undefined or another feature structure. Under our approach, feature structures are ideally suited for use in unification-based formalisms, in which unification, at its most basic level, is simply an operation that simultaneously determines the consistency of two pieces of partial information and, if they are consistent, combines them into a single result. The standard application of unification is to efficient hierarchical pattern matching, a basic operation which has applications to a broad range of knowledge representation and automated reasoning tasks.

Our notion of feature structures, as well as its implications for processing, should be of interest to anyone interested in the behavior of systems that employ features, roles, attributes, or slots with structured fillers or values. We provide a degree of abstraction away from concrete feature structures by employing a general attribute-value logic. We extend the usual attribute-value logic of Rounds and Kasper (1986, Kasper and Rounds 1986) to allow for path inequations, but do not allow general negation or implication of the sort studied by Johnson (1987, 1988), Smolka (1988), or King (1989).

The first aim of this paper is to attack a problem posed in [1] about uniform families of maps between realizable functors on PER's.

To put this into context, suppose that we are given a category C to serve as our category of types. The authors of [1] observe that the types representable in the second-order lambda; calculus and most extensions thereof can be regarded as being obtained from functors (Cop × C)n → C by diagonalisation of corresponding contra and covariant arguments. Terms in the calculus give rise to dinatural transformations. This suggests a general structure in which parametrised types are interpreted by arbitrary functors (Cop × C)n → C, and their elements by dinatural transformations. Unfortunately as the authors of the original paper point out, this interpretation can not be carried out in general since dinaturals do not necessarily compose.

However, suppose we are in the extraordinary position that all families of maps which are of the correct form to be a dinatural transformation between functors (Cop × C)n → C are in fact dinatural, a situation in which we have, so to speak, the dinaturality for free. In this situation dinaturals compose. The result is a structure for a system in which types can be parametrised by types (second-order lambda calculus without the polymorphic types). Suppose, in addition, the category in question is complete, then we can perform the necessary quantification (which is in fact a simple product), and obtain a model for the second-order lambda calculus.

In this chapter we take up the identity conditions that are imposed on feature structures and their substructures and conclude that this is the most significant difference between feature structures and first-order terms. We then consider how more term-like identity conditions may be imposed on feature structures by enforcing extensionality conditions which identify feature structures on the basis of their feature values. Cycles pose interesting issues for determining identity conditions and we study two forms of extensionality which differ in how they treat cyclic feature structures. In the weaker system, feature structures are identified if their feature values are shared. In the stronger system, which mimics the identity conditions of Prolog II, a variant of Aczel's (1988) bisimulations are used to define identity conditions.

Identity in Feature Structures

In standard treatments of feature structures, such as those of Pereira and Shieber (1984) and Rounds and Kasper (1986), it is assumed that there are two types of feature structures: atoms, which do not take values for any features, and feature structures, which can take values for arbitrary collections of features. The standard models of these structures employ directed graphs with atoms labeling some subset of the terminal nodes (nodes without any feature arcs going out of them). It is also usually assumed that there can only be one copy of any atom in a feature structure, so that if we know that a path π1 leads to an atom a and a path π2 leads to the same atom a, then the two paths must be structure shared. In Rounds and Kasper's treatment, this is enforced by requiring the type assignment function to be one to one.

Because we think of feature structures as representing partial information, the question immediately arises as to whether the notion of total information makes sense in this framework and if so, what its relation to partial information might be. Our notions of “total” information in this chapter are decidedly relative in the sense that they are only defined with respect to a fixed type inheritance hierarchy and fixed appropriateness conditions.

Before tackling the more complicated case of feature structures, we consider the first-order terms. First-order terms can be ordered by subsumption. The maximal elements in this ordering are the ground terms, a ground term being simply a term without variables. It is well known that the semantics of logic programming systems and even first-order logic can be characterized by restricting attention to the collection of ground terms, the so-called Herbrand Universe. The reason this is true is that every first-order term is equivalent to the meet of the collection of its ground extensions (Reynolds 1970). Thus any first-order term is uniquely determined by its ground extensions. It is also interesting to note that as a corollary, a term subsumes a second term just in case its set of ground instantiations is strictly larger than the set of ground instantiations of the second term. In this chapter, we consider whether or not we can derive equivalent results for feature structures. One motivation for deriving such results is that they make life much easier when it comes time to characterize the behavior of feature structure unification-based phrase structure grammars and logic programming systems. Unfortunately, we achieve only limited success.

Up to now, our presentation of feature structures has been fairly standard. In particular, our feature structures are identical to the finite sorted feature structures introduced by Pollard and Moshier (1990) and axiomatized by Pollard (in press). In terms of the informational ordering that they produce, our feature structures (modulo alphabetic variance) are nothing more than a notational variant of the ψ-terms of Aït-Kaci (1984, 1986) (modulo tag renaming and top “smashing,” with a bounded complete partial order of types). The important thing to note about the feature structures is that although we allowed a combination of primitive information with type symbols and structured information in terms of features and their values, there was no notion of typing; arbitrary labelings of directed graphs with type symbols and features were permissible.

In this chapter we introduce our notion of typing for feature structures, which is based on the notion of typing introduced informally by Pollard and Sag (1987:38) for the HPSG grammar formalism. Pollard and Sag introduced appropriateness conditions to model the distinction between features which are not appropriate for a given type and those whose values are simply unknown. Note that since appropriateness is defined as a relation between types and features, we say both that types are appropriate for features or that features are appropriate for types. We have already seen how the type symbols themselves are organized into a multiple inheritance hierarchy and how information from the types interacts with information encoded structurally in terms of features and values.

In this chapter we briefly show how definite clause logic programs fall out as a particular instance of unification-based phrase structure grammars. The analysis is based on the realization that parse trees for unification-based grammars bear a striking resemblance to proof trees for logic programs. More significantly, the top-down analysis of unification-based grammars generalizes the notion of SLD-resolution as it is applied in definite clause logic programming, whereas the bottom-up analysis generalizes the standard notion of denotational semantics for logic programs. The results in this chapter can be taken as a generalization of the Prolog family of programming languages (though as we have said before, we put off the analysis of inequations in grammars and hence in definite clause programs until the next chapter on constraint-resolution).

It has been noted in the past, most notably by Mukai (1985, 1987, Mukai and Yasukawa 1985), Aït-Kaci and Nasr (1986), and Höhfeld and Smolka (1988), that the idea of definite clause programming can be extended to domains other than first-order terms. In particular, the systems developed by Mukai and Yasukawa, Aït-Kaci and Nasr, and Hohfeld and Smolka employ a more or less standard notion of definite clauses with the simple modification of replacing first-order terms with various notions of feature structure. Of course, this move was preceded by extensions to Prolog from within the Prolog community itself by Colmerauer (1984), who developed Prolog II, a language based on definite clauses that allowed terms to contain cycles and also inequations. In this chapter, we generalize all of these systems by showing how any of our systems of feature structures can be used as the basis for defining a definite clause programming language.

Introduction

In a recent paper, Steven Vickers introduced a ‘generalized powerdomain’ construction, which he called the (lower) bagdomain, for algebraic posets, and argued that it provides a more realistic model than the powerdomain for the theory of databases (cf. Gunter). The basic idea is that our ‘partial information’ about a possible database should be specified not by a set of partial records of individuals, but by an indexed family (or, in Vickers' terminology, a bag) of such records: we do not want to be forced to identify two individuals in our database merely because the information that we have about them so far happens to be identical (even though we may, at some later stage, obtain the information that they are in fact the same individual).

There is an obvious problem with this notion. Even if the domain from which we start has only one point, the points of its bagdomain should correspond to arbitrary sets, and the ‘refinement ordering’ on them to arbitrary functions between sets, so that the bagdomain clearly cannot be a space (or even a locale) as usually understood. However, topos-theorists have long known how to handle ‘the space of all sets’ as a topos (the object classifier, cf. Johnstone and Wraith, pp. 175–6), and this is what Vickers constructs: that is, given an algebraic poset D, he constructs a topos BL(D) whose points are bags of points of D (and in the case when D has just one point, BL(D) is indeed the object classifier).

The London Mathematical Society Symposium on Applications of Categories in Computer Science took place in the Department of Mathematical Sciences at the University of Durham from 20 to 30 July 1991. Although the interaction between the mathematical theory of categories and theoretical computer science is by no means a recent phenomenon, the last few years have seen a marked upsurge in activity in this area. Consequently this was a very wellattended and lively Symposium. There were 100 participants, 73 receiving partial financial support from the Science and Engineering Research Council. The scientific aspects of the meeting were organized by Michael Fourman (Edinburgh), Peter Johnstone (Cambridge) and Andrew Pitts (Cambridge). A programme committee consisting of the three organizers together with Samson Abramsky (Imperial College), Pierre-Louis Curien (ENS, Paris) and Glynn Winskel (Aarhus) decided the final details of the scientific programme. There were 62 talks, eight of which were by the four key speakers who were Pierre-Louis Curien, Peter Freyd (Pennsylvania), John Reynolds (Carnegie-Mellon) and Glynn Winskel.

The papers in this volume represent final versions of a selection of the material presented at the Symposium, or in one case (the paper which stands last in the volume) of a development arising out of discussions which took place at the Symposium. We hope that they collectively present a balanced overview of the current state of research on the intersection between categories and computer science. All the papers have been refereed; we regret that pressure of space obliged us toexclude one or two papers that received favourable referee's reports.

Abstract

This paper collects observations about the two issues of sequentiality and full abstraction for programming languages. The format of the paper is that of an extended lecture. Some old and new results are hinted at, and references are given, without any claim to be exhaustive. We assume that the reader knows something about λ-calculus and about domain theory.

Introduction

Sequentiality and full abstraction have been often considered as related topics. More precisely, the quest of full abstraction led to the idea that sequentiality is a key issue in the semantics of programming languages.

In vague terms, full abstraction is the property that a mathematical semantics captures exactly the operational semantics of a specific language under study. Following the tradition of the first studies on full abstraction [Milner,Plotkin], the languages considered here are PCF, an extension of λ-calculus with arithmetic operators and recursion, and variants thereof. The focus on λ-calculus is amply justified by its rôle, either as a kernel (functional) programming language, or as a suitable metalanguage for the encoding of denotational semantics of a great variety of (sequential) programming languages.

It was Gérard Berry's belief that only after a detailed sudy of the syntax could one conceive the semantic definitions appropriate for reaching full abstraction. I always considered this as an illuminating idea, and this will be the starting point of this paper.

In section 2, we shall state Berry's Sequentiality Theorem: this will require us first to recall Wadsworth-Welch-Lévy's Continuity Theorem, and then to introduce a general notion of sequential function, due to Kahn-Plotkin.

In section 3, we shall abandon sequentiality for a while to define full abstraction and quote some results.