The quest for programming languages which are more readable and expressive has led to many developments in programming languages, one of which is the logic programming paradigm. In theory, logic programming languages are more readable and expressive because they borrow some of the expressive power of the language of mathematical logic – a language which was developed specifically in order to model some of the deductive processes of the human mind.

This theoretical goal has been achieved to only a limited extent in practice, because the implementations of logic programming languages differ from the ideal theoretical model in many ways. One of the most basic and profound of the differences is that the theory concerns languages which can be implemented completely only by parallel (breadth-first) interpreters, while most practical implementations use incomplete, sequential (depthfirst) strategies.

This incompleteness in itself would not necessarily be a problem; but unfortunately, the exact set of terminating sequential logic programs is hard to characterise in a logical way. Sequentiality also affects reasoning about programs, disrupting the hope that the identification of program with logical formula would make this straightforward. These problems tend to weaken claims that practical and truly logical programming is possible.

This thesis is intended as a step towards mending this rift between theory and practice, between parallel and sequential systems. In the thesis, I present a homogeneous operational characterisation of the parallel and sequential versions of a basic logic programming language; I then use proof systems to characterise, in a logical manner, the sets of queries which terminate in the various parallel, sequential, and mixed control disciplines.

This thesis has taken as its object of study the control-discipline variants of a simple logic programming language equivalent to Horn clause logic programming. It has classified and logically characterised the set of successful and failing queries of these variants of the language.

I have given an operational semantics, SOS, of which variants correspond to the parallel “and” and “or”, sequential “and”, sequential “or”, and sequential “and” and “or” control disciplines. This operational semantics homogenises the treatment of the control disciplines by incorporating control information (such as the failure-backtrack mechanism of seqeuntial systems) into the operational semantics. (Some of the variants of SOS have equivalent compositional operational semantics, which I have given.) I have also classified the queries into those succeeding and those failing in each of the control disciplines, and have proven the equivalence of some of these classes.

I have then used a sequent calculus framework, in which the elements of sequents are assertions about the success or failure of queries, to give a logical analysis of these classes of queries. Three calculi are given; they share a common set LKE of rules for classical logic with equality as syntactic identity, and differ in the set of axioms which characterise the behaviour of queries.

• LKE+PAR characterises the queries which succeed in parallel-or systems, and those which fail in parallel-and systems;

• LKE+SEQ characterises the queries which succeed in the sequential-and, sequential-or system, and those which fail in sequential-and systems;

• LKE+PASO characterises the queries which succeed in the parallel-and, sequential-or system.

In this chapter, I will give a characterisation of the two inner circles of the Venn diagram in Figure 2.6 in the same way as I characterised the two outer circles. That is, I will give a proof-theoretic characterisation of sequential logic programming (in particular, the operational semantics SP) in the form of a sequent calculus.

For this sequent calculus, we can use the rules LKE from the last chapter unchanged; we need only give anew group of axioms, SEQ, corresponding to PAR from the last chapter. These axioms, however, are more complex than those in PAR, have more side-conditions, and in particular involve the concept of disjunctive unfoldings of formulae.

Nevertheless, we can prove the same things about SEQ that we can about PAR: the laws are sound, and the proof system LKE+SEQ characterises sequential logic programming in several useful ways.

I will also give a characterisation of the last circle in Figure 2.6, namely the middle success circle. This set contains all queries which succeed in SOS/so, and can be characterised by a set of axioms, PASO, which combines axioms from PAR and from SEQ in a simple and intuitively clear way.

Approaches to Semantics

I begin by going into more detail about why we want a semantics for sequential logic programming, and what approaches have been taken so far to giving one.

The assumptions made about search strategies in most research on foundations of logic programming (for instance, SLD-resolution with a fair search rule) are not satisfied by sequential logic programming.

Operational (or “procedural”) semantics, as I mentioned in the Introduction, are used to provide characterisations of programming languages which meet certain “computational” criteria: giving a detailed description of the language for implementation purposes, and giving a computational model to which programmers can refer.

For logic programming, operational semantics are particularly important because it is in them that the innovations of logic programming lie. The notions of resolution and unification are not immediately apparent; unification, though defined by Herbrand in his thesis [44], was virtually ignored until Prawitz's work [62], and resolution was not defined until 1965 [66]. These notions must be explained within the context of a full description of the computational model of the language.

If we want to do such things as soundness and completeness proofs, or indeed any formal comparison of the operational semantics to other characterisations of the language, the operational semantics must also be mathematically precise – for instance, in the form of a formal system. (Plotkin [58] has explored the idea of structured operational semantics in detail, and gives a taxonomy to which I will refer in this chapter.) SLD-resolution [49], SLDNF-resolution [50], and the operational semantics in this chapter are just a few examples of formal operational semantics for logic programming. Other examples include Voda's tree-rewriting system [76], Deransart and Ferrand's [29] and Börger's [13] standardisation efforts, and the abstract computation engines for Andorra Prolog [43] and the “Pure Logic Language”, PLL [10, 52].

Although we have proven some useful completeness theorems about the proof systems in the last two chapters, we have not been able to prove absolute completeness: that every valid sequent is derivable. Because of some formal incompleteness results, we will never be able to prove such a completeness theorem, for any finitary proof system; but there are several ways in which we can, at least partially, escape the effect of these incompleteness results. In this chapter, I present the incompleteness theorems and some of the partial solutions.

There are two main incompleteness results, as discussed in the first section below. The first says that we will never be able to derive all valid closed sequents which have signed formulae in negative contexts, and follows from the non-existence of a solution to the Halting Problem. (We can deal with many of the important cases of this result by adding extra rules which I will describe.) The second result says that we will never be able to derive all valid sequents with free variables, even if they have no signed formulae in negative contexts, and is a version of Gödel's Incompleteness Theorem.

The “mathematical” solution to these problems is to bring the proof theory closer to a kind of model theory, by allowing infinitary elements into the proof systems. Though these are not adequate solutions for practical theorem proving, they are useful in that they shed light on the extent to which the proof systems in question are complete.

Introduction

In this chapter a number of existence proofs and theoretical discussions are presented. These are related to the earlier chapters, but were not presented there in order not to distract too much from the main line of those chapters. Sections 9.2 and 9.3 are related to Chapter 1. Sections 9.4 and 9.5 are related to Chapters 2 and 3, respectively. Finally Sections 9.6 and 9.7 are related to Chapter 5.

Undefinedness revisited

In this section we explain precisely how the truth and falsity of COLD-K assertions with respect to the partial many-sorted algebras is established. In particular the issue of undefinedness deserves a careful treatment. In this section we focus on the terms and assertions as presented in in Chapter 1 (see Tables 1.1 and 1.2).

Recall that a partial many-sorted Σ-algebra M is a system of carrier sets SM (one for each sort name S in Σ), partial functions fM (one for each function name f in Σ), and relations rM (one for each relation name r in Σ). The functions fM must be compatible with their typing in the following sense: if f : S1#…# Sm→ V1 #…# Vn is in £ we have that fM is a partial function from to. Similarly the predicates must be compatible with their typing, i.e. if r : S1×…× Sm is in Σ we have that rM is a relation on.

General

In this appendix a concrete syntax for COLD-K is defined. It is concerned with the full language, including the constructs presented in Chapter 10 and 11. The notions of term, expression and statement are integrated into a single syntactical category called <expression>. We give an (extended) BNF grammar defining a set of strings of ASCII characters which are used as concrete representations of the COLD-K constructs.

For user convenience, it is allowed to omit redundant type information. In the applied occurrence of a name the associated type information is generally omitted (otherwise the use of names would become very clumsy). Though in many situations the missing type information can be reconstructed from the context, there are situations where ambiguities may occur. We leave it to the parser to report such ambiguities; there is a special syntactic operator (the cast) to disambiguate the type of an expression.

In the concrete syntax defined here prefix, infix and postfix notations are used for the built-in operators of the language. For the user-defined operators (predicates, functions, procedures) only a prefix notation is provided. The main reason for not introducing infix, postfix or mixfix notations for the latter is simplicity. The possibility to define special notations for user-defined operators is typical for user-oriented versions of COLD, which can be defined as a kind of macro-extension of COLD-K.

Concrete syntax

We define the concrete syntax of COLD-K by means of a context free grammar and priority and associativity rules for the built-in operators. Below we shall define the lexical elements (tokens).

Chapters 6 and 7 deal with expansion calculi that exploit the fact that a design specification is ground confluent. First, directed expansion restricts paramodulation to left-to-right applications of prefix extensions of equational axioms (cf. Chapter 4). Narrowing (cf. Sect. 7.2) goes a step further and confines the input of expansion rules to pure axioms. Reductive expansion provides an alternative to inductive expansion, which originates from the idea of proving inductive validity by proving consistency (cf. Sect. 3.4) and reducing consistency to ground confluence (cf. Sects. 7.4 and 7.5).

Variables of a Horn clause occurring in its premise, but not in (the left-hand side of) its conclusion, called fresh variables, are usually banished as soon as one turns to a reduction calculus. This restriction cannot be maintained when arbitrary declarative programs are to be treated: if one follows the decomposition principle (cf. Sect. 2.6), then fresh variables are created automatically. They are then forbidden because they violate the usual condition that there is a Noetherian reduction ordering, i.e., that a reduction calculus admits only finite derivations. We shall see in Sect. 6.2 that other conditions on a reduction ordering can be weakened so as to often preserve the Noetherian property even if fresh variables are permitted.

Introduction

This chapter is about setting up flat algebraic specifications. This involves the introduction of more COLD-K constructs and the formulation of various methodological guidelines. At the end of the previous chapter we had to conclude that we almost succeeded in specifying the natural numbers, the only problem being that the expressive power to express the minimality of Nat was lacking. This expressive power will be available after we have introduced the inductive predicate definitions below. We shall complete the example of the natural numbers and we shall investigate various technical aspects of inductive definitions – which unfortunately are quite non-trivial. In addition to inductive predicate definitions, we shall also have inductive function definitions. We address issues like ‘proof obligations’ for inductive definitions, consistency and completeness. Finally we give a number of complete examples of flat algebraic specifications: queues, stacks, bags and symbolic expressions.

Inductive predicate definitions

An inductive predicate definition defines a predicate as the least predicate satisfying some assertion (provided that this predicate exists). Before turning our attention to the syntactic machinery available in COLD-K for expressing this, we ought to explain this notion of ‘least’. Therefore we shall formulate what we mean by one predicate being ‘less than or equal to’ another predicate.

Definition. A predicate r is less than or equal to a predicate q if for each argument x we have that r(x) implies q(x).

We illustrate this definition by means of two unary predicates p1 and p2. We assume the sort Nat with its operations zero and succ as specified before.