6 - Directed Expansion and Reduction

Summary

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.