Here we enter into the discussion of our principal topics. Continuous lattices and domains exhibit a variety of different aspects, some are order theoretical, some are topological, some belong to topological algebra and some to category theory – and indeed there are others. We shall contemplate these aspects one at a time, and this chapter is devoted entirely to the order theory surrounding our topic.

Evidently we have first to define continuous lattices and domains. As we shall see from hindsight, there are numerous equivalent conditions characterizing them. We choose the one which is probably the simplest, but it does involve the consideration of an auxiliary transitive relation, definable in every poset, by which one can say that an element x is “way below” an element y. We will write this as x « y. We devote Section I-1 to the introduction of the way-below relation and of continuous lattices and domains. We demonstrate that the occurrence of this particular additional ordering is not accidental and explain its predominant role in the theory. We exhibit the paradigmatic examples of continuous lattices and domains; in due course we shall see many more.

In Section I-2 we show that continuous lattices have a characterization in terms of (infinitary) equations. This gives us the important information that the class of continuous lattices, as an equational class, is closed under the formation of products, subalgebras, and homomorphic images – provided we recognize from the equations which maps ought to be considered as homomorphisms.

This introductory chapter serves as a convenient source of reference for certain basic aspects of complete lattices needed in what follows. The experienced reader may wish to skip directly to Chapter I and the beginning of the discussion of the main topic of this book: continuous lattices and domains.

Section O-1 fixes notation, while Section O-2 defines complete lattices, complete semilattices and directed complete partially ordered sets (dcpos), and lists a number of examples which we shall often encounter. The formalism of Galois connections is presented in Section 3. This not only is a very useful general tool, but also allows convenient access to the concept of a Heyting algebra. In Section O-4 we briefly discuss meet continuous lattices, of which both continuous lattices and complete Heyting algebras (frames) are (overlapping) subclasses. Of course, the more interesting topological aspects of these notions are postponed to later chapters. In Section O-5 we bring together for ease of reference many of the basic topological ideas that are scattered throughout the text and indicate how ordered structures arise out of topological ones. To aid the student, a few exercises have been included. Brief historical notes and references have been appended, but we have not tried to be exhaustive.

Generalities and Notation

Partially ordered sets occur everywhere in mathematics, but it is usually assumed that the partial order is antisymmetric. In the discussion of nets and directed limits, however, it is not always so convenient to assume this property.

Background and Plan of the Work

The purpose of this monograph is to present a fairly complete account of the development of the theory of continuous lattices as it currently exists. An attempt has been made to keep the body of the text expository and reasonably self-contained; somewhat more leeway has been allowed in the exercises. Much of what appears here constitutes basic, foundational or elementary material needed for the theory, but a considerable amount of more advanced exposition is also included.

Background and Motivation

The theory of continuous lattices is of relatively recent origin and has arisen more or less independently in a variety of mathematical contexts. We attempt a brief survey in the following paragraphs in the hope of pointing out some of the motivation behind the current interest in the study of these structures. We first indicate a definition for these lattices and then sketch some ways in which they arise.

A DEfiNITION. In the body of the Compendium the reader will find many equivalent characterizations of continuous lattices, but it would perhaps be best to begin with one rather straightforward definition – though it is not the primary one employed in the main text. Familiarity with algebraic lattices will be assumed for the moment, but even if the exact details are vague, the reader is surely familiar with many examples: the lattice of ideals of a ring, the lattice of subgroups of a group.

With the exception of certain developments in Chapter II, notably Sections II-2 and II-4, we largely refrained from using category-theoretic language (even when we used its tools in the context of Galois connections). Inevitably, we have to consider various types of functions between continuous lattices, and this is a natural point in our study to use the framework of category theory.

In Section IV-1 we discuss a duality based on the formalism of Galois connections between the categories DCPOG and DCPOD of all dcpos with upper and lower adjoints, respectively, as morphisms. We discuss in particular the categories INF and SUP, whose objects are complete lattices (in both cases) and whose morphisms are functions preserving arbitrary infs (respectively, sups). These categories are dual (IV-1.3). We saw as early as I-2.10 ff. that maps preserving arbitrary infs and directed sups play an important role in our theory. This leads us to consider the subcategory INF↑ of INF. Its dual under the INF–SUP duality is denoted by SUP0; its morphisms are precisely characterized in IV-1.4(1)–(2), but as a category in itself, SUP0 plays a minor role. More important, however, are the full subcategories AL ⊆ CL ⊆ INF↑ and ALop ⊆ CLop ⊆ SUP0, which consist of algebraic and continuous lattices, respectively.

Spectral theory plays an important and well-known role in such areas as the theory of commutative rings, lattices, and of C*-algebras, for example. The general idea is to define a notion of “prime element” (more often: ideal element) and then to endow the set of these primes with a topology. This topological space is called the “spectrum” of the structure. One then seeks to find how algebraic properties of the original structure are reflected in the topological properties of the spectrum; in addition, it is often possible to obtain a representation of the given structure in a concrete and natural fashion from the spectrum.

By means of the spectral theory of this chapter we associate with every complete lattice L a topological space, denoted by Spec L, and a representation L → O(Spec L) of the given lattice into the lattice of open subsets of the spectrum. Frequently one reduces the spectral theory in other mathematical contexts (such as those listed above) to this lattice theoretical spectral theory by considering a distinguished lattice of subobjects and identifying the spectrum of this lattice with the spectrum of the original structure in a natural way. Since the lattice of open sets of a topological space is a frame, it should be noted that a spectral representation can be an isomorphism only if L itself is a frame.

The chapter begins with an important lemma (frequently referred to as “The Lemma”) which plays a vital role in the spectral theory of continuous lattices.

As the title of the chapter indicates, we now turn our attention from the principally algebraic properties of continuous lattices to the position these lattices hold in topological algebra as certain compact semilattices. Indeed, as the Fundamental Theorem VI-3.4 shows, complete continuous semilattices are exactly the compact semilattices with small semilattices in the Lawson topology. Thus, complete continuous semilattices not only comprise an intrinsically important subcategory of the category of compact semilattices but also form the most well-understood category of compact semilattices. In fact, there are only two known examples of compact semilattices which are not complete continuous semilattices; these are presented in Section VI-4. The paucity of such examples attests to the unknown nature of compact semilattices in general.

We begin the chapter with some background remarks on compact pospaces and topological semilattices. This is followed by a order theoretic description of the topology of a compact semilattice in Section VI-2. Starting from any compact topological semilattice whatsoever, we deduce that the topology may be derived from the order. Indeed the topology is a variant “liminf” topology, one considerably more complicated than earlier ones we have considered. This allows order theoretic descriptions of continuous semilattice morphims, closed subsemilattices, etc., much in the spirit that we have already encountered for the Lawson topology is Section III-1.

Among other characteristics, an intelligent entity – whether an intelligent autonomous agent, or an intelligent assistant – must have the ability to go beyond just following direct instructions while in pursuit of a goal. This is necessary to be able to behave intelligently when the assumptions surrounding the direct instructions are not valid, or there are no direct instructions at all. For example even a seemingly direct instruction of ‘bring me coffee’ to an assistant requires the assistant to figure out what to do if the coffee pot is out of water, or if the coffee machine is broken. The assistant will definitely be referred to as lacking intelligence if he or she were to report to the boss that there is no water in the coffee pot and ask the boss what to do next. On the other hand, an assistant will be considered intelligent if he or she can take a high level request of ‘make travel arrangements for my trip to International AI conference 20XX’ and figure out the lecture times of the boss; take into account airline, hotel and car rental preferences; take into account the budget limitations, etc.; overcome hurdles such as the preferred flight being sold out; and make satisfactory arrangements. This example illustrates one benchmark of intelligence – the level of request an entity can handle.

In Chapter 4 we formulated several knowledge representation and problem solving domains using AnsProlog* and focused on the program development aspect. In this chapter we consider reasoning about actions in a dynamic world and its application to plan verification, simple planning, planning with various kinds of domain constraints, observation assimilation and explanation, and diagnosis. We do a detailed and systematic formulation – in AnsProlog* – of the above issues starting from the simplest reasoning about action scenarios and gradually increasing its expressiveness by adding features such as causal constraints, and parallel execution of actions. We also prove properties of our AnsProlog* formulations using the results in Chapter 3.

Our motivation behind the choice of a detailed formulation of this domain is twofold. (i) Reasoning about actions captures both major issues of this book: knowledge representation and declarative problem solving. To reason about actions we need to formulate the frame problem whose intuitive meaning is that objects in the worlds do not normally change their properties. Formalizing this has been one of the benchmark problems of knowledge representation and reasoning formalisms. We show how AnsProlog* is up to this task. Reasoning about actions also forms the ground work for planning with actions, an important problem solving task. We present AnsProlog encodings of planning such that the answer sets each encode a plan. (ii) Our second motivation is in regard to the demonstration of the usefulness of the results in Chapter 3.

Turing machines

This appendix is based on [Pap94] and it is recommended that the reader refer to that for detailed exposition on Turing machines, and computational complexity.

Intuitively, a deterministic Turing machine (DTM) is an automata bundled with a semi-infinite tape with a cursor to read from and write to. So, like an automata, there is a state and state transitions are based on the current state and what the cursor points to on the tape. But in addition to the state transition, there is an accompanying transition that dictates if the symbol in the tape location pointed to by the cursor should be overwritten and if the cursor should move to the left or right – by one cell – of its current position. Special symbols mark the beginning of the tape (>), the end of the input on the tape (⊔), and the output of the computation (‘halt’, ‘yes’, ‘no’). We now give a formal definition of DTMs.

Definition 151 A DTM is a quadruple M = (S, Σ, δ, s0) where S is a finite set of nonfinal states that includes s0 the initial state, Σ is a finite alphabet of symbols including the special symbols > and ⊔, and δ is a transition function that maps S × Σ to S ∪ {halt, yes, no} × Σ × {←, →, –}

Intuitively, δ is the control (or the program) of the machine that dictates how the machine behaves.

In this chapter we discuss three query answering and answer set computing systems: Smodels, dlv and PROLOG. Both Smodels and dlv are answer set computing systems and allow an input language with features and constructs not in AnsProlog*. While the Smodels system extends AnsProlog⊥ and AnsProlog⊥, ¬, the dlv system extends AnsProlog⊥,or and AnsProlog⊥,or,¬. We describe the syntax and semantics of the input language of Smodels and dlv and present several programs in their syntax. This chapter can be thought of as a quick introduction to programming in Smodels and dlv, not a full-fledged manual. At the time of writing this, both Smodels and dlv were evolving systems and readers are recommended to visit their corresponding web sites for the latest features.

After describing the Smodels and dlv systems with several small example programs, we consider several medium and large size applications and encode them using one or the other. In particular, we consider encoding of combinatorial auctions together with logical preference criteria, planning with durative actions and resources, resource constraint project scheduling, and specification and verification of active databases.

Finally, we give a brief introduction to the PROLOG interpreter and its approach to answering queries with respect to AnsProlog programs. We present conditions for AnsProlog programs and queries for which the PROLOG interpreter is sound and complete. We illustrate these conditions through several examples.

Smodels

The Smodels system is meant for computing the answer sets of AnsProlog⊥ and AnsProlog⊥,¬ programs and allows certain extensions to them.

In this chapter we formulate several knowledge representation and problem solving domains using AnsProlog*. Our focus in this chapter is on program development. We start with three well known problems from the literature of constraint satisfaction, and automated reasoning: placing queens on a chess board, determining who owns the zebra, and finding tile covering in a mutilated chess board. We show several encodings of these problems using AnsProlog*. We then discuss a general methodology for representing constraint satisfaction problems (CSPs) and show how to extend it to dynamic CSPs. We then present encodings of several combinatorial graph problems such as k-colorability, Hamiltonian circuit, and k-clique. After discussing these problem solving examples, we present a general methodology of reasoning with prioritized defaults, and show how reasoning with inheritance hierarchies is a special case of this.

Three well-known problem solving tasks

A well-known methodology for declarative problem solving is the generate and test methodology whereby possible solutions to the problem are generated and non-solutions are eliminated by testing. This is similar to the common way of showing that a problem is in the class NP, where it is shown that after the non-deterministic choice the testing can be done in polynomial time. The ‘generate’ part in an AnsProlog* formulation of a problem solving task is achieved by enumerating the possibilities, and the ‘test’ part is achieved by having constraints that eliminate the possibilities that violate the test conditions. Thus the answer sets of the resulting program correspond to solutions of the given problem.

Earlier in Chapter 3 we discussed several results and properties of AnsProlog* programs that are useful in analyzing and step-by-step building of these programs. In this chapter we consider some broader properties that help answer questions such as: (a) how difficult is it to compute answer sets of various sub-classes of AnsProlog*? (b) how expressive are the various sub-classes of AnsProlog*? (c) does the use of AnsProlog* lead to compact representation or can it be compiled to a more tractable representation? and (d) what is the relationship between AnsProlog* and other knowledge representation formalisms?

The answers to these questions are important in many ways. For example, if we know the complexity of a problem that we want to solve then the answer to (a) will tell us which particular subset of AnsProlog* will be most efficient, and the answer to (b) will tell us the most restricted subset that we can use to represent that problem. With respect to (c) we will discuss results that show that AnsProlog* leads to a compact representation. This clarifies the misconception that since many AnsProlog* classes belong to a higher complexity class, they are not very useful. For specifications where AnsProlog* leads to (exponentially) compact representation the fact that they are computationally harder is canceled out and they become preferable because compact representation means that the programmer has to write less. So the burden is shifted from the programmer to the computer, which is often desirable.

In this chapter we present several small AnsProlog* programs corresponding to several declarative problem solving modules or knowledge representation and reasoning aspects. Although in general we may have intermingling of the declarative problem solving, and the knowledge representation and reasoning aspects, they can be differentiated as follows.

Normally a problem solving task is to find solutions of a problem. A declarative way to do that is to declaratively enumerate the possible solutions and the tests such that the answer sets of the resulting program correspond to the solutions of the problem. The declarative problem solving modules that we consider in this chapter include modules that enforce simple constraints, modules that enumerate interpretations with respect to a set of atoms, modules that uniquely choose from a set of possibilities, modules that encode propositional satisfiability, modules that represent closed first-order queries, modules that check satisfiability of quantified boolean formulas with up to two quantifiers, modules that assign a linear ordering between a set of objects, modules that can represent various aggregations of facts (such as minimization, maximization, sum and average), modules that encode classical disjunction conclusions, modules that encode exclusive-or conclusions, and modules that encode cardinality and weight constraints.

By knowledge representation and reasoning aspects we mean representing particular benchmark aspects of nonmonotonic and common-sense reasoning that we want to be encoded by AnsProlog* programs.

So far in the book we have considered sub-classes of AnsProlog* which have been well-studied in the literature and two additional extensions AnsPrologsm and AnsPrologdlv which are the input language of the answer set computing systems Smodels and dlv. There have been several additional proposals for extending AnsProlog*, which are not that well-studied. Also, there have been many alternative proposals to characterize programs in the syntax of AnsProlog* and its sub-classes. In this chapter we give a brief overview of the above two aspects.

Some of the extensions that we consider are: (i) enriching the rules by allowing not in the head of rules, (ii) allowing nesting in the head and body of rules; (iii) allowing additional operators such as knowledge and belief operators; (iv) enriching the framework by allowing abduction; (v) allowing explicit specification of intent to use domain closure and its impact on the universal query problem; (vi) allowing set constructs; and (vii) allowing specification preferences between rules of a program.

In regard to alternative characterizations of programs in the syntax of AnsProlog* and its sub-classes, we focus mostly on AnsProlog and AnsProlog¬ syntax, and the well-founded semantics. In the process we define notions such as the 3-valued stable models, and stable classes which are related to both the well-founded characterization and the answer sets. We also briefly discuss the framework of argumentation which can be used in defining both answer sets and the well-founded characterization of programs in AnsProlog syntax.