Computing in Horn Clause Theories

Specification is the process of translating a problem into a formal description. This should be kept in mind even if we tend to use this term only for the final result of the process. Indeed, it is a characteristic of Western culture that it puts less emphasis on the process than on the form it creates (see Bohm; Whorf). Following Gregory Bateson, development always alternates between process and form. When the process of specification comes up with axioms defining the problem, we start the process of computation, for instance, deriving theorems. These are expected to improve our understanding of the problem so as to get closer to a solution. But theorems may also reveal flaws in our reasoning, hidden assumptions or undesired effects. In such a case we modify the specification and enter a new cycle of producing forms and initiating processes. Specification and theorem-proving tools should support this activity. However, they should not be designed with the intention of relieving us of the whole work. Many decisions are involved for which there is no proper reason to transfer them to a formal system or a machine. We think it necessary to stress this point because computer scientists sometimes ignore the limits of formal methods. Apart from ethical questions, there is no evidence at all that the heart of formal reasoning, namely deduction, plays a significant role in the problem-solving activity of our minds (Dreyfus and Dreyfus; Searle). Formal methods do not stand in their own right. They live with the people who use them (see Naur [1,2]).

Let A be a set. A binary relation R on A is irreflexive if for all <a,b> ∊ R, a ≠ b. R isNoetherian if there are no infinite sequences a₀,a₁,a₂,… of elements of A such that for all i ∊ ℕ, <a_i,a_i+1 > ∊ R.

The following Horn clause specifications are designed to illustrate the range of applications expressible within this framework. Some of them are referred to in subsequent chapters. The others should serve as material for the reader’s own investigation and assessment of Horn clause specification, programming and deduction using the concepts and calculi developed in this book. It is not the purpose of the present chapter to anticipate all problems and solutions handled in this monograph. (By the way, most of the problems first become obvious in the process of formalization.) The informal explanations given here follow a somewhat loose mode of discourse jumping between several levels which the formal exposition provided later will separate from one another. Moreover, some examples hint at questions and problem areas (e.g. issues of program transformation) which are not treated in the formal exposition. However, we think it necessary to include them here as well, at least to initiate more profound research. All this requires a little effort in the reading of this chapter, which pays off as a deeper insight into both the power and the limits of Horn clause reasoning.

This chapter deals with several theories derived from a Horn clause specification. Each theory is complete with respect to a subclass of Mod(SIG,AX) (cf. Section 2.3). Different theories represent different concepts of semantical abstraction. Some of them correspond to the theory of a single SIG-structure, say B. Vice versa, if we start out from a SIG-structure A as the formalization of a data type, an axiom set AX is called correct w.r.t. A if A coincides with B.

The previous chapter was devoted to theories of a Horn clause specification <SIG,AX> and their connection to classes of SIG-models of AX. All this was based upon the Horn clause calculus with its two simple inference rules: the Substitution and the Cut Rule (cf. Section 4.2). Derivations via the Horn clause calculus proceed bottom-up from the axioms to the goal to be proved. From an operational point of view, this might lead to a completely untractable search space. Cut and substitution capture the consequences of an axiomatization. To have these rules in mind allows us to check, more or less intuitively, whether AX is already what we want. But the pure Horn clause calculus is not appropriate to executing proofs automatically. For this purpose one should work top-down from the goal to be proved (or solved) by applying axioms backwards until a reduced (e.g. empty) goal has been achieved that indicates the validity (or solvability) of the initial goal. This is what the rules presented in Chapters 5, 7 and 8 do.

Refinements of paramodulation (cf. Section 5.3) such as goal reduction (cf. Chapter 7) and narrowing (cf. Chapter 8) are complete only if certain requirements on <SIG,AX> are fulfilled, which, in turn, depend on the division of <SIG,AX> into a base specification <BSIG,BAX> and the rest of <SIG,AX>. The base signature BSIG contains all sorts, predicates and sort-building or constructor functions of SIG. Hence the remaining part of SIG consists of operation symbols called non-constructor or, with the name indicating their meaning,destructor, inquiry, state-transition or value-returning functions. Accordingly, BAX specifies the predicates, in particular the equality predicates, with the help of constructor functions. Non-base axioms must be conditional equations and should only be used to specify non-constructor functions.

In the previous chapter, we introduced the Base Assumption (cf. Section 6.1) that is fundamental for refinements of resolution and paramodulation such as goal reduction (handled in this chapter) and narrowing (treated in the next chapter). Both rules are specializations of the Paramodulation Rule (cf. Section 5.3). Goal reduction differs from paramodulation in the following respects.

The Narrowing Rule is both a specialization of the Paramodulation Rule (cf. Section 5.3) and a generalization of the Single (goal) Reduction Rule (cf. Section 7.7). As a particular case of paramodulation narrowing applies conditional equations only from left to right and instantiates a goal only by irreducible substi tut ions. Wi th regard to goal reduction, narrowi ng adds the possibility of substituting into the variables of a goal before reducing it. However, the restriction to irreducible substitutions implies that a goal, say γ, can be narrowed only if it already contains some proper prefix of a reduction redex. An instantiation of γ is to complete the prefix to the full redex. “Proper” means that the prefix must not be a variable. Therefore reduction redices cannot be generated arbitrarily, just by substituting left-hand sides of conditional equations into variables of γ. Consequently, the number of possible narrowing steps starting out from γ is considerably smaller than the number of paramodulants of γ, even if we confine ourselves to most general paramodulation.