From the outside, our feature structures look much like the ψ-terms of Aït-Kaci (1984, 1986) or the feature structures of Pollard and Sag (1987), Moshier (1988) or Pollard and Moshier (1990). In particular, a feature structure is modeled by a possibly cyclic directed graph with labels on all of the nodes and arcs. Each node is labeled with a symbol representing its type, and the arcs are labeled with symbols representing features. We think of our types as organizing feature structures into natural classes. In this role, our types are doing the same duty as concepts in a terminological knowledge representation system (Brachman and Schmolze 1985, Brachman, Fikes, and Levesque 1983, Mac Gregor 1988) or abstract data types in object-oriented programming languages (Cardelli and Wegner 1985). Thus it is natural to think of the types as being organized in an inheritance hierarchy based on their generality. Feature structure unification is then modified so that two feature structures can only be unified if their types are compatible according to the primitive hierarchy of types.

In this chapter, we discuss how type inheritance hierarchies can be specified and the restrictions that we impose on them that allow us to define an adequate notion of type inference, which is necessary during unification. These restrictions were first noted by Aït-Kaci (1984) in his unification-based reasoning system. The polymorphism allowed in our type system is based on inheritance in which a subtype inherits information from all of its supertypes. The possibility of more than one supertype for a given type allows for multiple inheritance.

In this chapter we consider the addition of variables ranging over feature structures to our description language. It turns out that the addition of variables does not increase the representational power of the description language in terms of the feature structures which it can distinguish. Of course, this should not be surprising given the description theorem, which tells us that every feature structure can be picked out as the most general satisfier of some description. On the other hand, we can replace path equations and inequations in favor of variables and equations and inequations between variables if desirable. We prove a theorem to this effect in the latter part of this chapter. The reason that we consider variables now is that they have shown up in various guises in the feature structure literature, and are actually useful when considering applications such as definite clause programming languages based on feature structures. Our treatment of variables most closely follows that of Smolka (1988, 1989), who treats variables as part of the language for describing feature structures. Aït-Kaci (1984, 1986) also used variable-like objects, which he called tags. Due to the fact that he did not have a description language, Aït-Kaci had to consider variables to be part of the feature structures themselves, and then factor the class of feature structures with respect to alphabetic variance to recover the desired informational structure. We have informally introduced tags in our attribute value matrix diagrams, but did not consider them to be part of the feature structures themselves.

We assume that we have a countably infinite collection Var of variables.

In our development up to this point, we have treated feature structures logically as models of descriptions expressed in a simple attribute-value language. In the last chapter, we extended the notion of description to include variables; in this chapter, we generalize the notion of model to partial algebraic structures. An algebraic model consists of an arbitrary collection of domain objects and associates each feature with a unary partial function over this domain. In the research of Smolka (1988, 1989) and Johnson (1986, 1987, 1990), more general algebraic models of attribute-value descriptions are the focus of attention. We pull the rabbit out of the hat when we show that our old notion of satisfaction as a relation between feature structures and descriptions is really just a special case of a more general algebraic definition of satisfaction. The feature structures constitute an algebraic model in which the domain of the model is the collection of feature structures, and the features pick out their natural (partial) value mappings. What makes the feature structure model so appealing from a logical perspective is that it is canonical in the sense that descriptions are logically equivalent if and only if they are logically equivalent for the feature structure model. In this respect, the feature structure model plays the same logical role as term models play in universal algebra. This connection is strengthened in light of the most general satisfier and description theorems, which allow us to go back and forth between feature structures and their normal form descriptions.

Introduction

In recent joint work with A. Edalat[ES91] we developed a general approach to the solution of domain equations, based on information system ideas. The basis of the work was an axiomatization of the notion of a category of information systems, yielding what we may call an “information category”, or I-category for short. We begin this paper with an exposition of the I-category work. In the remainder of the paper we consider duality in I-categories, as the setting for studying initial algebra/final algebra coincidence. We then look at induction and coinduction principles in the light of these ideas.

To amplify the preceding a little, we note that the existing treatments of information systems, following [Sco82] and [LW84], make use of a global ordering of the objects of the category (the information systems) in order to “solve” domain equations by the ordinary cpo fixed point theorem. In the I-category approach, an initial algebra characterization of the solutions is obtained, by making use of a global ordering ⊆ of morphisms in addition to the ordering ⊴ of objects. (In the usual cases, where morphisms are “approximable relations” between tokens, the global ordering is essentially set inclusion; more precisely, we have that (f : A → B) ⊆ (f′ : A′ → B′) if A ⊴ A′, B ⊴ B′ and f ⊆ f′.) Moreover the axiomatic formulation enables us to handle many examples besides the usual categories of domains, in a unified manner: for example, “domain equations” over Stone spaces, via Boolean algebras as information systems. In the present exposition, we attempt to clarify the relation between the I-category approach and an established method of domain equation solution, namely the O-category method,usingthe Basic Lemma of [SP82] as a key.

In Algebraically Complete Categories (in the proceedings of the Category theory conference in Como '90) an ALGEBRAICALLY COMPLETE CATEGORY was defined as one for which every covariant endofunctor has an initial algebra. This should be understood to be in a 2-category setting, that is, in a setting in which the phrase “every covariant endofunctor” refers to an understood class of endofunctors.

Given an endofunctor T the category of T- INVARIANT objects is best defined as the category whose objects are triples <A,f, g> where f:TA →A, g:A→TA and fg and gf are both identity maps. T-Inv appears as a full subcategory of both T-Alg and T-Coalg, in each case via a forgetful functor. The Lambek lemma and its dual say that the initial object in T-Alg and the final object in T-Coalg may be viewed as objects in T-Inv wherein they easily remain initial and final. Of course there is a canonical map from the initial to the final. I will say that T is ALGEBRAICALLY BOUNDED if this canonical map is an isomorphism, equivalently if T-Inv is a punctuated category, that is one with a biterminator, an object that is both initial and final.

An algebraically bicomplete category is ALGEBRAICALLY COMPACT if each endofunctor is algebraically bounded. (As with algebraic completeness this should be understood to be in a 2-category setting.) In this context I will use the term FREE T-ALGEBRA rather than either initial algebra or final coalgebra.

With our definition of inheritance, we have a notion of consistency and unification for our smallest conceptual unit, the type. We now turn to the task of developing structured representations that can be built out of the basic concepts, which we call feature structures. The reason for the qualifier is that even though feature structures are defined using our type symbols, they are not typed, in the sense that there is no restriction on the co-occurrence of features or restrictions on their values. We introduce methods for specifying appropriateness conditions on features and a notion of well-typing only after studying the ordered notion of feature structures. We also hold off on introducing inequations and extensionality conditions. Before introducing these other topics, we concentrate on fully developing the notion of untyped feature structure and the logical notions we employ. Most of the results that hold for feature structures can be immediately generalized to well-typed feature structures by application of the type inference mechanism.

Our feature structures are structurally similar to the more traditional form of feature structures such as those used in the patr-ii system and those defined by Rounds and Kasper. The next major development after these initial systems was introduced by Moshier (1988). The innovation of Moshier's system was to allow atomic symbols to label arbitrary nodes in a feature structure. He also treated the identity conditions for these atoms fully intensionally. Both patr-ii and the Rounds and Kasper systems treated feature structures intensionally, but enforced extensional identity conditions on atoms.

In this chapter, we consider a phrase structure grammar formalism, or more precisely, a parameterized family of such formalisms, in which non-terminal (category) symbols are replaced by feature structures in both rewriting rules and lexical entries. Consequently, the application of a rewriting rule must be mediated by unification rather than by simple symbol matching. This explains why grammar formalisms such as the one we present here have come to be known as unification-based. Although our presentation of unification-based phrase structure grammars is self contained, for those unfamiliar with unification-based grammars and their applications, we recommend reading Shieber's excellent introduction (Shieber 1986). Shieber lays out the fundamental principles of unification-based phrase structure formalisms along with some of their more familar incarnations, as well as providing a wide variety of linguistic examples and motivations. Another good introductory source is the text by Gazdar and Mellish (1989).

The early development of unification-based grammars was intimately connected with the development of logic programming itself, the most obvious link stemming from Colmerauer's research into Q-systems (1970) and Metamorphosis Grammars (1978). In fact, Colmerauer's development of Prolog was motivated by the desire to provide a powerful yet efficient implementation environment for natural language grammars. The subsequent popularity of Prolog led to the development of a number of so-called logic grammar systems. These grammar formalisms are typically variations of first-order term unification phrase structure grammars such as the Definite Clause Grammars (DCGS) of Pereira and Warren (1980), the Extraposition Grammars of Pereira (1981), the Slot Grammars of McCord (1981) and also the Gapping Grammars of Dahl and Abramson (1984, Popowich 1985).

Introduction

In these circumstances it seems appropriate to set down those old ideas after all, and to complete them in various ways, in particular as regards enriched monads.

In this chapter we introduce the logical attribute-value language that we employ to describe feature structures. Our description language is the same (in the sense of containing exactly the same descriptions) as that of Rounds and Kasper (1986), but following Pollard (in press) our interpretations are based on our feature structures rather than the ones provided by Rounds and Kasper. One way to look at the language of descriptions is as providing a way to talk about feature structures; the language can be displayed linearly one symbol after another and can thus be easily used in implementations. Other researchers, namely Johnson (1987, 1988), Smolka (1988) and King (1989), use similar, but much more powerful, logical description languages and take a totally different view of the nature of interpretations or models for these languages. The main difference in their descriptions is the presence of general description negation, implication, and variables. The interpretations they use are based on a domain of objects with features interpreted as unary partial functions on this domain. In the system we describe here, we view feature structures themselves as partial objects; descriptions are just a particularly neat and tidy notation for picking them out. Our view thus corresponds to Aït-Kaci's treatment of his ψ-terms, which were also taken to be partial descriptions of empirical objects. Johnson (1988:72), on the other hand, is at pains to point out that he does not view feature structures as partial models or descriptions of total linguistic objects, but rather as total objects themselves.

In this chapter we generalize our notion of feature structure to allow for the possibility of having countably infinite collections of nodes. When we considered algebraic models in the last chapter, we implicitly allowed models with objects from which infinitely many distinct objects were accessible by iteratively applying feature value functions. In the case of feature structures as we have previously taken them, the set of substructures of a feature structure was always in one-to-one correspondence with the nodes of the feature structure and hence finite. In the case of finite feature structures, we were guaranteed joins or unifications for consistent finite sets of (finite) feature structures. We also saw examples of infinite sets of consistent finite feature structures which did not have a finite least upper bound. When we allow for the possibility of countably infinite feature structures, we have least upper bounds for arbitrary (possibly infinite) consistent sets of (possibly infinite) feature structures. In fact, the collection of feature structures with countable node sets turn out to form a predomain in the sense that when we factor out alphabetic variance, we are left with an algebraic countably based BCPO. Luckily, in the feature structure domain, the compact domain elements are just the finite feature structures, thus giving us a way to characterize arbitrary infinite feature structures as simple joins of finite feature structures. One benefit of such a move is that infinite or limit elements in our domains provide models for non-terminating inference procedures such as total type inference over an appropriateness specification with loops or extensionalization when non-maximal types are allowed to be extensional.

In this chapter we consider acyclic feature structures and their axiomatization. In standard first-order logic resolution theorem provers (see Wos et al. 1984 for an overview), it is necessary to make sure that when a variable X is unified with a term t, there is no occurrence of X in t. This is the so-called occurs check and dates back to Robinson's (1965) original algorithm for unification. Without the occurs check, resolution produces unsound inferences. The problem with the occurs check is that it is often expensive to compute in practical unification algorithms. Unification algorithms have been developed with built in occurs checks that are linear (Paterson and Wegman 1978) and quasi-linear (Martelli and Montanari 1982), but the data structures employed for computing the occurs check incur a heavy constant overhead (Jaffar 1984). Rather than carry out the occurs check, implementations of logic programming languages like Prolog simply omit it, leading to interpreters and compilers which are not sound with respect to the semantics of first-order logic and may furthermore cause the interpreters to hang during the processing of cyclic structures which are accidentally created. Rather than change the interpreters, the move made in Prolog II (Colmerauer 1984, 1987) was to change the semantics to allow for infinite rational trees, which correspond to the infinite unfoldings of the terms that result from unifications of a variable with a term that contains it. Considering the pointer-based implementation of unification (Jaffar 1984, Moshier 1988), infinite trees are more naturally construed as finite graphs containing cycles.

Abstract

Introduction

One of the cornerstones of programming language semantics is the correspondence between simply-typed λ-calculi and cartesian closed categories established by Lambek and Scott [LS86]. It provides a clean algebraic semantics for λ-terms, which helps us to reason effectively about the values of programs. Of equal interest to the implementer, however, is the reduction process which computes these values, i.e. the operational semantics. One of the most satisfying approaches to date is Plotkin's structural operational semantics [Plo75, Plo81] which uses a sequent calculus to describe the reduction process and provide a rigorous specification for computation.

In spite of their separate virtues, it is difficult to relate the logic (of operational semantics) to the categorical algebra (of denotational semantics); the usual approach, using computational adequacy, is rather unwieldy.

Introduction

In his seminal paper [Plo77], Plotkin introduced the functional language PCF (‘programming language for computable functions’) together with the standard denotational model of cpo's and continuous functions. He proved that this model is computationally adequate for PCF, but not fully abstract.

In order to obtain full abstraction he extended PCF by a parallel conditional operator. The problem with this operator is, that it changes the nature of the language. All computations in the original language PCF can be executed sequentially, but the new operator requires expressions to be evaluated in parallel.

Here we address the problem of full abstraction for the original sequential language PCF, i. e. instead of extending the language we try to improve the model. Our approach is to cut down the standard model with the aid of certain logical relations, which we call sequentiality relations. We give a semantic characterization of these relations and illustrate how they can be used to reason about sequential (i. e. PCF-definable) functions. Finally we prove that this style of reasoning is ‘complete’ for proving observational congruences between closed PCF-expressions of order ≤ 3. Technically, this completeness can be expressed as a full abstraction result for the sublanguage which consists of these expressions.

Sequential PCF

In [Plo77], PCF is defined as a simply typed λ-calculus over the ground types ι (of integers) and o (of Booleans).

Abstract

Fibrations have been widely used to model polymorphic λ-calculi. In this paper we describe the additional structure on a fibration that suffices to make it a model of a polymorphic λ-calculus with subtypes and bounded quantification; the basic idea is to single out a class of maps, the inclusions, in each fibre. Bounded quantification is made possible by a imposing condition that resembles local smallness. Since the notion of inclusion is not stable under isomorphism, some care must be taken to make everything strict.

We then show that PER models for λ-calculi with subtypes fit into this framework. In fact, not only PERs, but also any full reflective sub category of the category of modest sets (‘PERs’ in a realizability topos), provide a model; hence all the small complete categories of ‘synthetic domains’ found in various realizability toposes can be used to model subtypes.

Introduction

What this paper is about

At the core of object-oriented programming, and related approaches to programming, are the notions of subtyping and inheritance. These have proved to be very powerful tools for structuring programs, and they appear—in one form or another—in a wide variety of modern programming languages.

One way of studying these notions formally is to use the framework of typed λ-calculus. That is, we start with a formal system (say, a version of the polymorphic λ-calculus) and extend it by adding a notion of type inclusion, together with suitable rules; we obtain a larger system. We can then use the methods of mathematical logic to study the properties of the system.