HIGHER-ORDER HORN CLAUSES

GOPALAN NADATHUR Duke University, Durham, North Carolina

DALE MILLER University of Pennsylvania, Philadelphia, Pennsylvania

Abstract: A generalization of Horn clauses to a higher-order logic is described and examined as a basis for logic programming. In qualitative terms, these higher-order Horn clauses are obtained from the first-order ones by replacing first-order terms with simply typed λ-terms and by permitting quantification over all occurrences of function symbols and some occurrences of predicate symbols. Several proof-theoretic results concerning these extended clauses are presented. One result shows that although the substitutions for predicate variables can be quite complex in general, the substitutions necessary in the context of higher-order Horn clauses are tightly constrained. This observation is used to show that these higher-order formulas can specify computations in a fashion similar to first-order Horn clauses. A complete theorem proving procedure is also described for the extension. This procedure is obtained by interweaving higher-order unification with backchaining and goal reductions, and constitutes a higher-order generalization of SLD-resolution. These results have a practical realization in the higher-order logic programming language called λProlog.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory — syntax; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic — logic programming; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving — logic programming General Terms: Languages, Theory Additional Key Words and Phrases: Higher-order logic, higher-order unification, Horn clauses, Prolog, SLD-resolution

The work of G. Nadathur was funded in part by NSF grant MCS-82-19196 and a Burroughs contract. The work of D. Miller was funded by NSF grant CCR-87-05596 and DARPA grant N000-14-85-K-0018. Authors’ current addresses: G. Nadathur, Computer Science Department, Duke University, Durham, NC 27706; D. Miller, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104-6389.

1. Introduction A principled analysis of the nature and role of higher-order notions within logic pro-

gramming appears to be absent from the literature on this programming paradigm. Some attempts, such as those in [34], have been made to realize higher-order features akin to those in functional programming languages, and have even been incorporated into most existing versions of the language Prolog. These attempts are, however, unsatisfactory from two perspectives. First, they have relied on the use of ad hoc mechanisms and hence are at variance with one of the strengths of logic programming, namely its basis in logic. Second, they have not taken full cognizance of the difference between the functional and logic programming paradigms and, consequently, of potential differences between higher-order notions in these paradigms.

Towards filling this lacuna, this paper initiates investigations into a logical basis for higher-order features in logic programming. The principal concern here is that of describing an extension to Horn clauses [33], the basis of languages such as Prolog [32], by using a higher-order logic. The use of the term “extension” clearly signifies that there is some character of Horn clauses that is to be retained. This character may most conveniently be enunciated in the context of a generalized version of Horn clauses that is, in some senses, closer to actual realizations of logic programming. Letting A represent an atomic formula, we identify goal formulas as those given by the rule

G ::= A | G_{1} ∨ G_{2} | G_{1} ∧ G_{2} | ∃xG,

and definite sentences as the universal closure of atomic formulas and of formulas of the form G ⊃ A; the symbol G is used in each case as a syntactic variable for a goal formula. These formulas are related to Horn clauses in the following sense: Within the framework of classical first-order logic, the negation of a goal formula is equivalent to a set of negative Horn clauses and, similarly, a definite sentence is equivalent to a set of positive Horn clauses. Now, if P is a set of definite sentences and ⊢ denotes provability in (classical) first-order logic, then the following properties may be noted:

(i) P ⊢ ∃xG only if there is a term t such that P ⊢ G[t/x], where G[t/x] represents the result of substituting t for all the free occurrences of x in G.

(ii) P ⊢ G_{1} ∨ G_{2} only if P ⊢ G_{1} or P ⊢ G_{2}. (iii) P ⊢ G_{1} ∧ G_{2} only if P ⊢ G_{1} and P ⊢ G_{2}. (iv) If A is an atomic formula, then P ⊢ A only if either (a) A is a substitution instance of

a formula in P, or (b) there is a substitution instance of the form G ⊃ A of a definite sentence in P such that P ⊢ G. While the converse of each property above follows from the meanings of the logical

connectives and quantifiers, these properties themselves are a consequence of the special structure of goal formulas and definite sentences. The importance of these properties is in the role they play in the computational interpretation accorded to these formulas. Logic programming is based on construing a collection, P, of definite sentences as a program and a goal formula, G, as a query. The idea of a computation in this context is that of constructing a proof of the existential closure of G from P and, if this process is successful, of extracting from this proof a substitution instance of G that is provable from P. The consistency of this view is apparently dependent on (i). In a more fine-grained analysis, (i)–(iv) collectively support a feature of importance to logic programming, namely the ability to construe each formula as contributing to the specification of a search, the nature of the search being described through the use of logical connectives and quantifiers. Thus, (ii) and (iii) permit the interpretation of the propositional connectives ∨ and ∧ as primitives for specifying non-deterministic or and and branches in a search, and (i) warrants the conception of the existential quantifier as the means for describing an infinite (non-deterministic) or branch where the branches are parameterized by the set of terms. Similarly, (iv) permits us to interpret a definite sentence as partially defining a procedure: For instance, the formula G ⊃ A corresponds to the description that an attempt to solve a procedure whose name is the predicate head of A may be made by trying to solve the goal G. As a final observation, we see that (i)–(iv) readily yield a proof procedure, closely related to SLD-resolution [2], that, in fact, forms the computational machinery for realizing this programming paradigm.

The properties discussed above thus appear to play a central role in the context of logic programming, and it is desirable to retain these while extending the formulas underlying this programming paradigm. This paper provides one such extension. The formulas described here may, in an informal sense, be characterized as those obtained from firstorder goal formulas and definite sentences by supplanting first-order terms with the terms of a typed λ-calculus and by permitting quantification over function and predicate symbols. These formulas provide for higher-order features of two distinct kinds within logic programming. The first arises out of the presence of predicate variables. Given the correspondence between predicates and procedures in logic programming, this facilitates the writing of procedures that take other procedures as arguments, a style of programming often referred to as higher-order programming. Occurrences of predicate variables are restricted and so also are the appearances of logical connectives in terms, but the restrictions are well motivated from a programming perspective. They may, in fact, be informally understood as follows. First, the name of a procedure defined by a definite sentence, i.e. the head of A in a formula of the form G ⊃ A, must not be a variable. Second, only those logical connectives that may appear in the top-level logical structure of a goal formula are permitted in terms; the picture here is that when a predicate variable in the body of a procedure declaration is instantiated, the result is expected to be a legitimate goal formula or query. The quantification over predicate variables that is permitted and the corresponding enrichment to the term structure are however sufficient to allow a direct emulation within logic programming of various higher-order functions (such as the map and reduce functions of Lisp) that have been found to be useful in the functional programming context.

The second, and truly novel, feature of our extension is the provision of λ-terms as data structures. There has been a growing interest in recent years in programming environments in which complex syntactic objects such as formulas, programs and proofs can be represented and manipulated easily [6, 11, 31]. In developing environments of this kind, programming languages that facilitate the representation and manipulation of these kinds of objects play a fundamental role. As is evident from the arguments provided elsewhere [16, 22, 30, 28], the representation of objects involving the notion of binding, i.e. objects such as formulas, programs and proofs, is best achieved through the use of a term language based on the λ-calculus. The task of reasoning about such objects in turn places an emphasis on a programming paradigm that provides primitives for examining the structure of λ-terms and that also supports the notion of search in an intrinsic way. Although the logic programming paradigm is a natural choice from the latter perspective, there is a need to enrich the data structures of a language such as Prolog before it is genuinely useful as a “metalanguage”. The analysis in this paper provides for a language with such an enrichment and consequently leads to a language that potentially has several novel applications. Detailed experiments in some of the application realms show that this potential is in fact borne out. The interested reader may refer, for instance, to [7, 13, 20, 22, 25, 29] for the results of these experiments.

It should be mentioned that the extension to first-order Horn clauses described in this paper is not the only one possible that preserves the spirit of properties (i)–(iv). The primary aim here is that of examining the nature and role of higher-order notions within logic programming and this underlies the focus on enriching only the nature of quantification within (first-order) Horn clauses. It is possible, however, to consider other enrichments to the logical structure of these formulas, perhaps after explaining what it means to preserve the spirit of properties (i)–(iv) if a richer set of connectives is involved. Such a task is undertaken in [23]. Briefly, a proof-theoretic criterion is presented therein for determining when a logical language provides the basis for logic programming and this is used to describe a family of extensions to first-order Horn clauses. The “richest” extension described in [23] replaces definite sentences by a class of formulas called higherorder hereditary Harrop or hohh formulas. The higher-order definite sentences of this paper are a subclass of the latter class of formulas. Further, the use of hohh formulas provides for notions such as modules, abstract data types and lexical scoping in addition to higherorder features within logic programming. There is, however, a significant distinction to be made between the theory of the higher-order Horn clauses presented in this paper and of the hohh formulas presented in [23]. The distinction, expressed informally, is that the programming interpretation of higher-order definite sentences accords well with classical logic, whereas a shift to intuitionistic logic is required in the context of hohh formulas. This shift in semantic commitment may not be acceptable in some applications of logic programming. Despite this difference, it is to be noted that several of the proof-theoretic techniques presented in this paper have been generalized and utilized in [23]. It is in fact a perceived generality of these techniques that justifies their detailed presentation here.

This rest of this paper is organized as follows. In the next section we describe the higher-order logic used in this paper, summarizing several necessary logical notions in the process. The axiomatization presented here for the logic is in the style of Gentzen [9]. The use of a sequent calculus, although unusual in the literature on logic programming (see [4] for an exception), has several advantages. One advantage is the simplification of prooftheoretic discussions that we hope this paper demonstrates. In another direction, it is the casting of our arguments within such a calculus that has been instrumental in the discovery of the “essential” character of logic programming and thereby in the description of further logical extensions to it [18, 23]. In Section 3, we outline the classes of formulas within this logic that are our generalizations to first-order goal formulas and definite sentences. Section 4 is devoted to showing that these formulas satisfy properties (i)–(iv) above when ⊢ is interpreted as provability in the higher-order logic. The main problem here is the presence of predicate variables; substitutions for these kinds of variables may, in general, alter the logical structure of formulas in which they appear and thus complicate the nature of proofs. Fortunately, as we show in the first part of Section 4, predicate variable substitutions can be tightly constrained in the context of our higher-order formulas. This result is then used to show that these formulas provide a satisfactory basis for a logic programming language. In Section 5 we describe a theorem-proving procedure that provides the basis for an interpreter for such a language. This procedure interweaves higher-order unification [15] with backchaining and goal reductions and constitutes a higher-order generalization to SLD-resolution. These results have been used to describe a logic programming language called λProlog. A presentation of this language is beyond the scope of this paper but may be found in [21, 25, 27].

2. A Higher-Order Logic The higher-order logic used in this paper is derived from Church’s formulation of the

simple theory of types [5] principally by the exclusion of the axioms concerning infinity, choice, extensionality and description. Church’s logic is particularly suited to our purposes since it is obtained by superimposing logical notions over the calculus of λ-conversion. Our omission of certain axioms is based on a desire for a logic that generalizes first-order logic by providing a stronger notion of a variable and a term, but at the same time encompasses only the most primitive logical notions that are relevant in this context; only these notions appear to be of consequence from the perspective of computational applications. Our logic is closely related to that of [1], the only real differences being the inclusion of η-conversion as a rule of inference and the incorporation of a larger number of propositional connectives and quantifiers as primitives. We describe this logic below, simultaneously introducing the logical vocabulary used in the rest of the paper.

The Language. The language used is based on a typed λ-calculus. The types in this context are determined by a set S of sorts, that contains at least the sort o and one other sort, and by a set C of type constructors each member of which has a unique positive arity: The class of types is then the smallest collection that includes (i) every sort, (ii) (c α_{1} … α_{n}), for every c ∈ C of arity n and every α_{1}, …, α_{n} that are types, and (iii) (α → β) for every α and β that are types. We refer to the types obtained by virtue of (i) and (ii) as atomic types and to those obtained by virtue of (iii) as function types. In an informal sense, each type may be construed as corresponding to a set of objects. Understood in this manner, (α_{1} → α_{2}) corresponds to the collection of functions each of whose domain and range is determined by α_{1} and α_{2}, respectively. In writing types, the convention that → associates to the right is often used to omit parentheses. In this paper, the letters α and β are used, perhaps with subscripts, as syntactic variables for types. An arbitrary type is occasionally depicted by an expression of the form (α_{1} → ⋯ → α_{n} → β) where β is assumed to be an atomic type. When a type is displayed in this form, we refer to α_{1}, …, α_{n} as its argument types and to β as its target type. The use of such a notation for atomic types is justified by the convention that the argument types may be an empty sequence.

We now assume that we are provided with a denumerable set, Var_{α}, of variables for each type α, and with a collection of constants of arbitrary given types, such that the subcollection at each type α is denumerable and disjoint from Var_{α}. The latter collection is assumed to contain at least one member of each type, and to include the following infinite list of symbols called the logical constants: ⊤ of type o, ∼ of type o → o, ∧, ∨ and ⊃ of type o → o → o, and, for each α, Σ and Π of type (α → o) → o. The remaining constants are referred to as parameters. The class of formulas or terms is then defined inductively as follows:

(i) A variable or a constant of type α is a formula of type α. (ii) If x is a variable of type α_{1} and F is a formula of type α_{2} then [λx.F] is a formula of

type α_{1} → α_{2}, and is referred to as an abstraction that binds x and whose scope is F. (iii) If F_{1} is a formula of type α_{1} → α_{2} and F_{2} is a formula of type α_{1} then [F_{1} F_{2}], referred

to as the application of F_{1} to F_{2}, is a formula of type α_{2}.

Certain conventions concerning formulas are employed in this paper. First, lower-case letters are used, perhaps with subscripts, to denote formulas that are variables; such a usage may occur at the level of either the object or the meta language. Similarly, uppercase letters are used to denote parameters at the object level and arbitrary formulas in the meta language. Second, in the interest of readability, the brackets that surround expressions formed by virtue of (ii) and (iii) above are often omitted. These may be restored by using the conventions that abstraction is right associative, application is left associative and application has smaller scope than abstraction. Finally, although each formula is specified only in conjunction with a type, the types of formulas are seldom explicitly mentioned. Such omissions are justified on the basis that the types are either inferable from the context or inessential to the discussion at hand.

The rules of formation serve to identify the well-formed subparts of each formula. Specifically, G is said to occur in, or to be a subformula of, F if (a) G is F, or (b) F is λx.F_{1} and G occurs in F_{1}, or (c) F is [F_{1} F_{2}] and G occurs in either F_{1} or F_{2}. An occurrence of a variable x in F is either bound or free depending on whether it is or is not an occurrence in the scope of an abstraction that binds x. x is a bound (free) variable of F if it has at least one bound (free) occurrence in F. F is a closed formula just in case it has no free variables. We write F(F) to denote the set of free variables of F. This notation is generalized to sets of formulas and sets of pairs of formulas in the following way: F(D) is ⋃{F(F) | F ∈ D} if D is a set of formulas and ⋃{F(F_{1}) ∪ F(F_{2}) | ⟨F_{1}, F_{2}⟩ ∈ D} if D is a set of pairs of formulas.

The type o has a special significance. Formulas of this type correspond to propositions, and a formula of type α_{1} → ⋯ → α_{n} → o is a predicate of n arguments whose i^{th} argument is of type α_{i}. In accordance with the informal interpretation of types, predicates may be thought of as representing sets of n-tuples or relations. The logical constants are intended to be interpreted in the following manner: ⊤ corresponds to the tautologous proposition, the (propositional) connectives ∼, ∨, ∧, and ⊃ correspond, respectively, to negation, disjunction, conjunction, and implication, and the family of constants Σ and Π are, respectively, existential and universal quantifiers, viewed as propositional functions of propositional functions. There are certain notational conventions pertaining to the logical constants that find use below. First, disjunction, conjunction and implication are written as infix operations; e.g. [∨ F G] is usually written as [F ∨G]. Second, the expressions [∃x.F] and [∀x.F] serve as abbreviations for [Σ λx.F] and [Π λx.F]; these abbreviations illustrate the use of Σ and Π along with abstractions to create the operations of existential and universal quantification familiar in the context of first-order logic. Finally x̄ is sometimes used as an abbreviation for a sequence of variables x_{1}, …, x_{n}. In such cases, the expression ∃x̄.F serves as a shorthand for ∃x_{1}…. ∃x_{n}.F. Similar interpretations are to be bestowed upon ∀x̄.F and λx̄.F.

The Calculus of λ-Conversion. In the interpretation intended for the language, λ is to correspond to the abstraction operation and juxtaposition to the operation of function application. These intentions are formalized by the rules of λ-conversion. To define these rules, we need the operation of replacing all free occurrences of a variable x in the formula F by a formula G of the same type as x. This operation is denoted by S_{G}^{x} F and may be made explicit as follows:

(i) If F is a variable or a constant, then S_{G}^{x} F is G if F is x and F otherwise. (ii) If F is of the form λy.C, then S_{G}^{x} F is F if y is x and λy.S_{G}^{x} F otherwise. (iii) If F is of the form [C D], then S_{G}^{x} F = [(S_{G}^{x} C) (S_{G}^{x} D)]. In performing this operation of replacement, there is the danger that the free variables of G become bound inadvertently. The term “G is free for x in F ” describes the situations in which the operation is logically correct, i.e. those situations where x does not occur free in the scope of an abstraction in F that binds a free variable of G. The rules of α-conversion, β-conversion and η-conversion are then, respectively, the following operations on formulas:

(1) Replacing a subformula λx.F by λy.S_{y}^{x} F provided y is free for x in F and y is not free in F.

(2) Replacing a subformula [λx.F] G by S_{G}^{x} F provided G is free for x in F and vice versa.

(3) Replacing a subformula λx.[F x] by F provided x is not free in F and vice versa. The rules above, collectively referred to as the λ-conversion rules, are used to define

the following relations on formulas. 2.1. Definition. F λ-conv (β-conv, ≡) G just in case there is a sequence of applications of the λ-conversion (respectively α- and β-conversion, α-conversion) rules that transforms F into G.

The three relations thus defined are evidently equivalence relations. They correspond, in fact, to notions of equality between formulas based on the following informal interpretation of the λ-conversion rules: α-conversion asserts that the choice of name for the variable bound by an abstraction is unimportant, β-conversion relates an application to the result of evaluating the application, and η-conversion describes a weak notion of extensionality for formulas. In this paper we use the strongest of these notions, i.e. we consider F and G equal just in case F λ-conv G. There are certain distinctions to be made between formulas by omitting the rules of η-conversion, but we feel that these are not important in our context.

A formula F is said to be a β-normal form if it does not have a subformula of the form [λx.A] B, and a λ-normal form if, in addition, it does not have a subformula of the form λx.[A x] with x not occurring free in A. If F is a β-normal form (λ-normal form) and G β-conv (λ-conv) F, then F is said to be a β-normal (λ-normal) form of G. From the Church-Rosser Theorem, described in, e.g., [3] for a λ-calculus without type symbols but applicable to the language under consideration as well, it follows that a β-normal (λ-normal) form of a formula is unique up to a renaming of bound variables. Further, it is known [1, 8] that a β-normal form exists for every formula in the typed λ-calculus; this may be obtained by repeatedly replacing subformulas of the form [λx.A] B by S_{B}^{x} A, preceded, perhaps, by some α-conversion steps. Such a formula may be converted into a λ-normal form by replacing each subformula of the form λx.[A x] where x does not occur free in A by A. In summary, any formula F may be converted into a λ-normal form that is unique up to α-conversions. We denote such a form by λnorm(F). Occasionally, we need to talk of a unique normal form and, in such cases, we use ρ(F) to designate what we call the principal normal form of F. Determining this form essentially requires a naming convention for bound variables and a convention such as that in [1] will suffice for our purposes.

The existence of a λ-normal form for each formula provides a mechanism for determining whether two formulas are equal by virtue of the λ-conversion rules. These normal forms also facilitate the discussion of properties of formulas in terms of a representative for each of the equivalence classes that has a convenient structure. In this context, we note that a β-normal form is a formula that has the structure

λx_{1}…. λx_{n}.[A F_{1} … F_{m}]

where A is a constant or variable, and, for 1 ≤ i ≤ m, F_{i} also has the same form. We refer to the sequence x_{1}, …, x_{n} as the binder, to A as the head and to F_{1}, …, F_{m} as the arguments of such a formula; in particular instances, the binder may be empty, and the formula may also have no arguments. Such a formula is said to be rigid if its head, i.e. A, is either a constant or a variable that appears in the binder, and flexible otherwise. A formula having the above structure is also a λ-normal form if F_{m} is not identical to x_{n} and, further, each of the F_{i}s also satisfy this constraint. In subsequent sections, we shall have use for the structure of λ-normal forms of type o. To describe this, we first identify an atom as a λ-normal form whose leftmost symbol that is not a bracket is either a variable or a parameter. Then, a λ-normal form of type o is one of the following: (i) ⊤, (ii) an atom, (iii) ∼F, where F is a λ-normal form of type o, (iv) [F ∨ G], [F ∧ G], or [F ⊃ G] where F and G are λ-normal forms of type o, or (v) Σ P or Π P, where P is a λ-normal form.

Substitutions. A substitution is a set of the form {⟨x_{i}, F_{i}⟩ | 1 ≤ i ≤ n}, where, for 1 ≤ i ≤ n, each x_{i} is a distinct variable and F_{i} is a formula in principal normal form of the same type as, but distinct from, x_{i}; this substitution is a substitution for {x_{1}, …, x_{n}}, and its range is {F_{1}, …, F_{n}}. A substitution may be viewed as a type preserving mapping on variables that is the identity everywhere except the points explicitly specified. This mapping may be extended to the class of all formulas in a manner consistent with this view: If θ = {⟨x_{i}, F_{i}⟩ | 1 ≤ i ≤ n} and G is any formula, then

θ(G) = ρ([λx_{1}…. λx_{n}.G] F_{1} … F_{n})

This definition is independent of the order in which we take the pairs from θ. Further, given our notion of equality between formulas, the application of a substitution to a formula G is evidently a formalization of the idea of replacing the free occurrences of x_{1}, …, x_{n} in G simultaneously by the formulas F_{1}, …, F_{n}.

We need certain terminology pertaining to substitutions, and we summarize these here. A formula F is said to be an instance of another formula G if it results from applying a substitution to G. The restriction of a substitution θ to a set of variables V, denoted by θ ↑ V, is given as follows

θ ↑ V = {⟨x, F ⟩ | ⟨x, F ⟩ ∈ θ and x ∈ V}.

It is evident that θ(G) = (θ ↑ F(G))(G). The composition of two substitutions θ_{1} and θ_{2}, written as θ_{1} ∘ θ_{2}, is precisely the composition of θ_{1} and θ_{2} when these are viewed as mappings: θ_{1} ∘ θ_{2}(G) = θ_{1}(θ_{2}(G)). Two substitutions, θ_{1} and θ_{2} are said to be equal relative to a set of variables V if it is the case that θ_{1} ↑ V = θ_{2} ↑ V; this relationship is denoted by θ_{1} =_{V} θ_{2}. θ_{1} is said to be less general than θ_{2} relative to V, a relationship denoted by θ_{1} ⪯_{V} θ_{2}, if there is a substitution σ such that θ_{1} =_{V} σ ∘ θ_{2}. Finally, we shall sometimes talk of the result of applying a substitution to sets of formulas and to sets of pairs of formulas. In the first case, we mean the set that results from applying the substitution to each formula in the set, and, in the latter case, we mean the set of pairs that results from the application of the substitution to each element in each pair.

The Formal System. The notion of derivation used in this paper is formalized by means of the sequent calculus LKH that is a higher-order extension to the logistic classical calculus LK of [9]. A sequent within the calculus LKH is an expression of the form

F_{1}, …, F_{n} ⟶ G_{1}, …, G_{m}

where n ≥ 0, m ≥ 0, and, for 1 ≤ i ≤ n and 1 ≤ j ≤ m, F_{i} and G_{j} are formulas; the listing F_{1}, …, F_{n} is the antecedent of the sequent, and G_{1}, …, G_{m} forms its succedent. The initial sequents or axioms of the calculus are ⟶ ⊤ and the sequents of the form A ⟶ A′ where A and A′ are atomic formulas such that A ≡ A′. The inference figures are the arrangements of sequents that result from the schemata in Figures 2.1 and 2.2 by replacing (i) the Γs and Δs by finite sequences of formulas of type o, (ii) A and B by formulas of type o, (iii) A′, in the schemata designated by λ, by a formula resulting by a sequence of λ-conversions from the formula that replaces A in the lower sequent of the schema, and, finally, (iv) P, C, and y in the schemata designated by Σ−IS, Π−IS, Σ−IA, and Π−IA by, respectively, a formula of type α → o, a formula of type α, and a parameter or variable of type α that does not occur free in any formulas substituted into the lower sequent, for some choice of α. An inference figure is classified as a structural or an operational one, depending on whether it results from a schema in Figure 2.1 or 2.2. In the operational inference figures, we designate the formula substituted for the expression containing the logical constant as the principal formula of the figure. Some operational inference figures contain two upper sequents, and these are referred to, respectively, as the left and right upper sequents of the figure.

Thinning: in the antecedent

\begin{matrix}Γ ⟶ Δ \\ A, Γ ⟶ Δ \end{matrix}

in the succedent

\begin{matrix}Γ ⟶ Δ \\ Γ ⟶ Δ, A \end{matrix}

Contraction: in the antecedent

{A, A, Γ ⟶ Δ \atop A, Γ ⟶ Δ}

in the succedent

\begin{matrix}Γ ⟶ Δ, A, A \\ Γ ⟶ Δ_{1}, F, Δ_{2} \end{matrix}

Interchange: in the antecedent

\begin{matrix}Γ_{1}, B, A, Γ_{2} ⟶ Δ \\ Γ_{1}, A, B, Γ_{2} ⟶ Δ \end{matrix}

in the succedent

\begin{matrix}Γ ⟶ Δ_{1}, A, B, Δ_{2} \\ Γ ⟶ Δ_{1}, B, A, Δ_{2} \end{matrix}

λ: in the antecedent

{A′, Γ ⟶ Δ \atop A, Γ ⟶ Δ}

in the succedent

{Γ ⟶ Δ, A′ \atop Γ ⟶ Δ, A}

Figure 2.1: The LKH Structural Inference Figure Schemata

Intrinsic to a sequent calculus is the notion of a derivation or proof figure. These are tree-like arrangements of sequents that combine to form inference figures such that (i) each sequent, with the exception of one called the endsequent, is the upper sequent of exactly one inference figure, (ii) each sequent is the lower sequent of at most one inference figure and those sequents that are not the lower sequents of any inference figure are initial sequents. Such an arrangement constitutes a derivation for its endsequent. If there is a

\begin{aligned}Γ ⟶ Δ, A \\ & ∼−IA \\ ∼A, Γ ⟶ Δ \end{aligned}  \begin{aligned}A, Γ ⟶ Δ \\ & ∼−IS \\ Γ ⟶ Δ, ∼A \end{aligned}
A, Γ ⟶ Δ  B, Γ ⟶ Δ ∨−IA

A ∨ B, Γ ⟶ Δ

\begin{aligned}Γ ⟶ Δ, A \\ & ∨−IS \\ Γ ⟶ Δ, A ∨ B \end{aligned}  \begin{aligned}Γ ⟶ Δ, B \\ & ∨−IS \\ Γ ⟶ Δ, A ∨ B \end{aligned}

\begin{aligned}A, Γ ⟶ Δ \\ & ∧−IA \\ A ∧ B, Γ ⟶ Δ \end{aligned}  \begin{aligned}B, Γ ⟶ Δ \\ & ∧−IA \\ A ∧ B, Γ ⟶ Δ \end{aligned}
Γ ⟶ Δ, A  Γ ⟶ Δ, B ∧−IS

Γ ⟶ Δ, A ∧ B

Γ_{1} ⟶ Δ_{1}, A  B, Γ_{2} ⟶ Δ_{2} ⊃−IA

A ⊃ B, Γ_{1}, Γ_{2} ⟶ Δ_{1}, Δ_{2}

A, Γ ⟶ Δ, B ⊃−IS

Γ ⟶ Δ, A ⊃ B

ρ([P y]), Γ ⟶ Δ Σ−IA

Σ P, Γ ⟶ Δ

Γ ⟶ Δ, ρ([P C]) Σ−IS

Γ ⟶ Δ, Σ P

ρ([P C]), Γ ⟶ Δ Π−IA

Π P, Γ ⟶ Δ

Γ ⟶ Δ, ρ([P y]) Π−IS

Γ ⟶ Δ, Π P

Figure 2.2: The LKH Operational Inference Figure Schemata

derivation for Γ ⟶ A, where A is a formula, then A is said to be provable from Γ. A path in a derivation is a sequence of sequents whose first member is the endsequent and whose last member is an initial sequent, and of which every member except the first is the upper sequent of an inference figure whose lower sequent is the preceding member. The height of the proof figure is the length of the longest path in the figure. Each sequent occurrence† in a derivation is on a unique path, and we refer to the number of sequents that precede it on this path as its distance from the endsequent. The notion of a derivation is relativized to particular sequent calculi by the choice of initial sequents and inference figures, and we use this observation in Section 4. Our current focus is on the calculus LKH, and we intend unqualified uses of the term “derivation” below to be read as LKH-derivation.

It is of interest to note that if η-conversion is added as a rule of inference to the system T of [1], then the resulting system is equivalent to the calculus LKH in the sense described in [9]. Specifically, let us say that the associated formula of the sequent Γ ⟶ Δ is ∧Γ ⊃ ∨Δ if neither the antecedent nor the succedent is empty, ∨Δ if only the antecedent is empty, ∧Γ ⊃ p ∧ ∼p if only the succedent is empty, and p ∧ ∼p if the antecedent and the succedent are both empty; p is a designated propositional variable here, and [∧Γ] and [∨Δ] are to be read as conjunctions and disjunctions of the formulas in Γ and Δ respectively. It is then the case that a derivation exists for Γ ⟶ Δ if and only if its associated formula is a theorem of T with the rule of η-conversion; we assume here that the symbols ∧, ⊃ and Σ are introduced via abbreviations in T .

The reader familiar with [9] may notice several similarities between the calculi LK and LKH. One difference between these is the absence of the Cut inference figure in LKH. This omission is justified by the cut-elimination result for the version of higherorder logic under consideration [1]. Another, apparently superficial, difference is in the use in LKH of λ-conversion to capture the notion of substitution in inference figures pertaining to quantifiers. The only significant difference, then is in the richer syntax of formulas and the presence of the λ inference figures in LKH. We note in particular that the presence of predicate variables in formulas of LKH enables substitutions to change their logical structure. As a result, it is possible to describe several complex derivations in a concise form in this higher-order logic. However, this facet makes the task of constructing satisfactory proof procedures for this logic a difficult one. In fact, as we shall see shortly, considerable care must be taken even in enunciating and verifying the proof-theoretic properties of our higher-order formulas.

3. Higher-Order Definite Sentences and Goal Formulas Using the higher-order logic of the previous section, the desired generalizations to first-

order definite sentences and goal formulas may be identified. Intrinsic to this identification is the notion of a positive formula. As made precise by the following definition, these are the formulas in which the symbols ∼, ⊃ and Π do not appear.

† The qualification “occurrence” will henceforth be assumed implicitly where necessary.

3.1. Definition. The class of positive formulas, PF, is the smallest collection of formulas such that (i) each variable and each constant other than ∼, ⊃ and Π is in PF, and (ii) the formulas λx.A and [A B] are in PF if A and B are in PF. The Positive Herbrand Universe, H^{+}, is the collection of all λ-normal formulas in PF, and the Herbrand Base, HB, is the collection of all closed formulas in H^{+}.

As will become apparent shortly, HB in our context plays the same role as the Herbrand Universe does in the context of other discussions of logic programming: it is the domain of terms that is used in describing the results of computations. 3.2. Definition. A higher-order goal formula is a formula of type o in H^{+}. A positive atom is an atomic goal formula, i.e. an atom in H^{+}. A higher-order definite formula is any formula of the form ∀x̄.G ⊃ A where G is a goal formula, A is a rigid positive atom; in particular, x̄ may be an empty sequence, i.e. the quantification may be absent. Such a formula is a higher-order definite sentence if it is closed, i.e. if x̄ contains all the variables free in G and A. The qualification “higher-order” used in this definition is intended to distinguish the formulas defined from the first-order formulas of the same name and may be omitted if, by so doing, no confusion should arise.

A formula is a positive atom if it is either ⊤ or of the form [A F_{1} … F_{n}] where A is a parameter or a variable and, for 1 ≤ i ≤ n, F_{i} is a positive formula, and is a rigid positive atom if, in the latter case, A is also a parameter. It is easily verified that a goal formula must be one of the following: (i) a positive atom, (ii) A ∨ B or A ∧ B, where A and B are goal formulas, or (iii) Σ P where P is a predicate in H^{+}; in the last case, we observe that it is equivalent to a formula of the form ∃x.G where G is a goal formula. Thus, we see that the top-level logical structure of definite sentences and goal formulas in the higher-order setting is quite similar to those in the first-order context. The first-order formulas are, in fact, contained in the corresponding higher-order formulas under an implicit encoding that essentially assigns types to the first-order terms and predicates. To be precise, if i is a sort other that o, the encoding assigns the type i to variables and constants, the type i → ⋯ → i → i, with n + 1 occurrences of i, to each n-ary function symbol, and the type i → ⋯ → i → o, with n occurrences of i, to each n-ary predicate symbol. Looked at differently, our formulas contain within them a many-sorted version of first-order definite sentences and goal formulas. However, they do embody a genuine generalization to the first-order formulas in that they may contain complex terms that are constructed by the use of abstractions and applications and, further, may also include quantifications over variables that correspond to functions and predicates. The following examples serve to illustrate these additional facets. 3.3. Example. Let list be a 1-ary type constructor and let int be a sort. Further, let nil and cons be parameters of type (list int) and int → (list int) → (list int) respectively, and let mapfun be a parameter of type (int → int) → (list int) → (list int) → o. Then the two formulas below are definite sentences:

∀f.[⊤ ⊃ [mapfun f nil nil]],
∀f.∀x.∀l_{1}.∀l_{2}.[[mapfun f l_{1} l_{2}] ⊃ [mapfun f [cons x l_{1}] [cons [f x] l_{2}]]];

f is evidently a function variable in these formulas. If 1, 2, and and g are parameters of type int, int, and int → int → int respectively, the following is a goal formula:

∃l.[mapfun [λx.[g x 1]] [cons 1 [cons 2 nil]] l].

Observe that this formula contains the higher-order term λx.[g x 1].

3.4. Example. Let primrel be a parameter of type (i → i → o) → o and let rel, wife, mother, jane, and mary be parameters of appropriate types. The following are then definite sentences:

[⊤ ⊃ [mother jane mary]], [⊤ ⊃ [wife john jane]],
[⊤ ⊃ [primrel mother]], [⊤ ⊃ [primrel wife]], ∀r.[[primrel r] ⊃ [rel r]],
∀r.∀s.[[[primrel r] ∧ [primrel s]] ⊃ [rel [λx.λy.∃z.[[r x z] ∧ [s z y]]]]].

Observe that the last definite sentence contains the predicate variables r and s. Further, the complex term that appears as the argument of the predicate rel in this definite sentence contains an existential quantifier and a conjunction. The formula

∃r.[[rel r] ∧ [r john mary]]

is a goal formula in this context. It is a goal formula in which a predicate variable occurs “extensionally”, i.e. in a position where a substitution made for it can affect the top-level logical structure of the formula.

In the next section, we examine some of the properties of higher-order definite sentences and goal formulas. To preview the main results there, we introduce the following definition. 3.5. Definition. A substitution φ is a positive substitution if its range is contained in H^{+}. It is a closed positive substitution if its range is contained in HB.

Now let P be a finite collection of definite sentences, and let G be a goal formula whose free variables are contained in the listing x̄. We shall see, then, that ∃x̄.G is provable from P just in case there is a closed positive substitution φ for x̄ such that φ(G) is provable from P. This observation shall also facilitate the description of a simple proof procedure that may be used to extract substitutions such as φ. From these observations it will follow that our definite sentences and goal formulas provide the basis for a generalization to the programming paradigm of first-order logic.

4. Properties of Higher-Order Definite Sentences As observed in Section 3, one difference between the top-level logical structure of

first-order and higher-order goal formulas is that, in the higher-order context, predicate variables may appear as the heads of atomic goals. A consequence of this difference is that some of the proofs that can be constructed for goal formulas from definite sentences in the higher-order setting have quite a different character from any in the first-order case. An illustration of this fact is provided by the following derivation of the goal formula ∃y.[P y] from the definite sentence ∀x.[x ⊃ [P A]].

\begin{aligned}[P B] ⟶ [P B] \\ & Σ−IS \\ [P B] ⟶ ∃y.[P y] \end{aligned} ; ∼−IS ; ⟶ ∃y.[P y], ∼[P B] \begin{aligned}[P A] ⟶ [P A] \\ & Σ−IS \\ [P A] ⟶ ∃y.[P y] \end{aligned} ⊃−IA
∼[P B] ⊃ [P A] ⟶ ∃y.[P y], ∃y.[P y]

Contraction

∼[P B] ⊃ [P A] ⟶ ∃y.[P y] Π−IA

∀x.[x ⊃ [P A]] ⟶ ∃y.[P y]

It is easily observed that the top-level logical structure of a first-order formula remains invariant under any substitutions that are made for its free variables. It may then be seen that in a derivation whose endsequent contains only first-order definite formulas in the antecedent and only first-order goal formulas in the succedent, every other sequent must have only definite formulas and atoms in the antecedent and goal formulas in the succedent. This is, however, not the case in the higher-order context, as illustrated by the above derivation. Consider, for instance, the penultimate sequent in this derivation that is reproduced below:

∼[P B] ⊃ [P A] ⟶ ∃y.[P y].  (∗)

The formula ∼[P B] ⊃ [P A] that appears in the antecedent of this sequent is neither a definite formula nor an atom. Looking closely at this sequent also reveals why this might be a cause for concern from the perspective of our current endeavor. Although this sequent has a derivation, we observe that there is no term t such that

∼[P B] ⊃ [P A] ⟶ [P t]

has a derivation. Now, if all derivations of

∀x.[x ⊃ [P A]] ⟶ ∃y.[P y]

involve the derivation of (∗), or of sequents similar to (∗) in the sense just outlined, then there would be no proof of ∃y.[P y] from ∃x.[x ⊃ [P A]] from which an “answer” may be extracted. Thus, it would be the case that one of the properties critical to the computational interpretation of definite sentences is false.

We show in this section that problems of the sort alluded to in the previous paragraph do not arise, and that, in fact, higher-order definite sentences and goal formulas resemble the corresponding first-order formulas in several proof-theoretic senses. The method that we adopt in demonstrating this may be described as follows. Let us identify the following inference figure schemata

ρ(P C), Γ ⟶ Δ Π−IA^{+}

Π P, Γ ⟶ Δ

Γ ⟶ Δ, ρ(P C) Σ−IS^{+}

Γ ⟶ Δ, Σ P

where we expect only closed positive formulas, i.e. formulas from HB, to be substituted for C. These are evidently subcases of Π−IA and Σ−IS. We shall show that if there is any derivation at all of a sequent Γ ⟶ Δ where Γ consists only of definite sentences and Δ consists only of closed goal formulas, then there is one in which every inference figure obtained from Π−IA or Σ−IS is also an instance of Π−IA^{+} and Σ−IS^{+} respectively. These schemata are of interest because in any of their instances, if the lower sequent has only closed positive atoms and definite sentences in the antecedent and closed goal formulas in the succedent then so too does the upper sequent. Derivations of the sort mentioned, therefore, bear structural similarities to those in the first-order case, a fact that may be exploited to show that higher-order definite sentences and goal formulas retain many of the computational properties of their first-order counterparts.

The result that we prove below is actually of interest quite apart from the purposes of this paper. The so-called cut-elimination theorems have been of interest in the context of logic because they provide an insight into the nature of deduction and often are the basis for its mechanization. In the context of first-order logic, for instance, this theorem leads to the subformula property: if a sequent has a derivation, then it has one in which every formula in any intermediate sequent is a subformula of some formula in the endsequent. Several other useful structural properties of deduction in the first-order context flow from this observation, and the traditional proof procedures for first-order logic are based on it. As is evident from the example at the beginning of this section, the subformula property does not hold (under any acceptable interpretation) for higher-order logic even though the logic admits a cut-elimination theorem; predicate terms containing connectives and quantifiers may be generalized upon in the course of a derivation, and thus intermediate sequents may have formulas whose structure cannot be predicted from the formulas in the final one. For this reason, the usefulness of cut-elimination as a mechanism for analyzing and automating deduction in higher-order logic has been generally doubted. However, Theorem 4.1 below shows that there is useful structural information about proofs in higher-order logic to be obtained from the cut-elimination theorem for this logic, and is one of few results of this sort. This theorem permits us to observe that in the restricted setting of higher-order Horn clauses proofs for every derivable sequent can be constructed without ever having to generalize on predicate terms containing the logical constants ∼, ⊃, and Π. This observation in turn provides information about the structure of each sequent in a derivation and constitutes a restriction on substitution terms that is sufficient to enable the description of a complete theorem proving procedure for higher-order Horn clauses.

A Simplified Sequent Calculus. Part of the discussion above is given a precise form by the following theorem:

4.1. Theorem. Let Γ be a sequence of formulas that are either definite sentences or closed positive atoms of type o, and let Δ be a sequence of closed goal formulas. Then Γ ⟶ Δ has an LKH-derivation only if it has one in which

(i) the only inference figures that appear are Contraction, Interchange, Thinning, ∨−IS, ∧−IS, Σ−IS, ⊃−IA and Π−IA, and

(ii) each occurrence of the figure Π−IA or Σ−IS is also an occurrence of the figure Π−IA^{+} or Σ−IS^{+}.

The proof of this theorem is obtained by describing a transformation from an arbitrary LKH-derivation of Γ ⟶ Δ into a derivation of the requisite kind. This transformation is performed by replacing the formulas in each sequent by what we might call their “positive correlates” and by removing certain parts of the derivation that become unnecessary as a result. The following definition describes the manner in which the formulas in the succedent of each sequent are transformed.

4.2. Definition. Let x, y ∈ Var_{o} and, for each α, let z_{α} ∈ Var_{(α→o)}. The function pos on formulas is then defined as follows:

(i) If F is a constant or a variable

pos(F) = \{ \begin{matrix}λx.⊤, & if F is ∼; \\ λx.λy.⊤, & if F is ⊃; \\ λz_{α}.⊤, & if F is Π of type ((α → o) → o); \\ F, & otherwise. \end{matrix}

(ii) pos([F_{1} F_{2}]) = [pos(F_{1}) pos(F_{2})]. (iii) pos(λx.F) = λx.pos(F). Further, pc is the mapping on formulas defined as follows: If F is a formula, pc(F) = ρ(pos(F)).

From the definition above it follows easily that F(pc(F)) ⊆ F(pos(F)) = F(F). Thus if F is a closed formula, then pc(F) ∈ HB. The properties of pc stated in the following lemma are similarly easily argued for; these properties will be used in the proof of the main theorem. 4.3. Lemma. Let F be a λ-normal formula of type o.

(i) If F is an atom, then pc(F) is a positive atom. (ii) If F is ∼F_{1}, F_{1} ⊃ F_{2}, or Π P, then pc(F) = ⊤. (iii) If F is G ∗ H where ∗ is either ∨ or ∧, then pc(F) = pc(G) ∗ pc(H). (iv) If F is Σ P, then pc(F) = Σ pc(P)

In the lemma below, we argue that pc and ρ commute as operations on formulas. This observation is of interest because it yields the property of pc that is stated in Corollary 4.5 and is needed in the proof of the Theorem 4.1. 4.4. Lemma. For any formula F, pc(ρ(F)) = ρ(pc(F)). Proof. Given any formula B of the same type as x, an easy induction on the structure of a formula G verifies the following facts: If B is free for x in G, then pos(B) is free for x in pos(G) and pos(S_{B}^{x} G) = S_{pos(B)}^{x} pos(G). Now, let us say that a formula H results directly from a formula G by an application of a rule of λ-conversion if the subformula of G that is replaced by virtue of one of these rules is G itself. We claim that if H does indeed result from G in such a manner, then pos(H) also results from pos(G) in a similar manner. This claim is easily proved from the following observations:

(i) If G is λx.G_{1} and H is λy.S_{y}^{x} G_{1}, pos(G) is λx.pos(G_{1}) and pos(H) is λy.S_{y}^{x} pos(G_{1}). Further if y is free for x in G_{1} then y is free for x in pos(G_{1}).

(ii) If G is [λx.G_{1}] G_{2} and H is S_{G_{2}}^{x} G_{1} then pos(F) is [[λx.pos(G_{1})] pos(G_{2})] and pos(H) is S_{pos(G_{2})}^{x} pos(G_{1}). Further if G_{2} is free for x in G_{1} then pos(G_{2}) is free for x in pos(G_{1}).

(iii) If G is of type α → β then pos(G) is also of type α → β. If G is λy.[H y] then pos(G) is λy.[pos(H) y] and, further, y ∈ F(pos(H)) only if y ∈ F(H).

Now let F′ result from F by a rule of λ-conversion. By making use of the claim above and by inducing on the structure of F, it may be shown that pos(F′) results from pos(F) by a similar rule. From this it follows that pos(ρ(F)) results from pos(F) by the application of the rules of λ-conversion. Hence ρ(pos(ρ(F))) = ρ(pos(F)). Noting further that ρ(pos(F)) = ρ(ρ(pos(F))), the lemma is proved.

4.5. Corollary. If P and C are formulas of appropriate types, then

pc(ρ([P C])) = ρ([pc(P) pc(C)]).

Proof. The claim is evident from the following equalities:

pc(ρ([P C])) = ρ(pc([P C]))  by Lemma 4.4
= ρ([pos(P) pos(C)])  using definitions
= ρ([ρ(pos(P)) ρ(pos(C))]) by properties of λ-conversion
= ρ([pc(P) pc(C)])  using definitions.

While the mapping pc will adequately serve the purpose of transforming formulas in the succedent of each sequent in the proof of Theorem 4.1, it does not suffice as a means for transforming formulas in the antecedent. It may be observed that if F is a definite formula then pc(F) = ⊤. The transformation to be effected on formulas in the antecedent must be such that it preserves definite formulas. In order to describe such a mapping, we find it useful first to identify the following class of formulas that contains the class of definite formulas. 4.6. Definition. A formula of type o is an implicational formula just in case it has one of the following forms

(i) F ⊃ A, where F and A are λ-normal formulas and in addition A is a rigid atom, or (ii) ∀x.F, where F is itself an implicational formula.

We now define a function on implicational formulas whose purpose is to transform these formulas into definite formulas. 4.7. Definition. The function pos_{i} on implicational formulas is defined as follows

(i) If F is H ⊃ A then pos_{i}(F) = pos(H) ⊃ pos(A). (ii) If F is ∀x.F_{1} then pos_{i}(F) = ∀x.pos_{i}(F_{1}) If F is an implicational formula then pc_{i}(F) = ρ(pos_{i}(F)).

From the definition, it is evident that if F is a definite formula, pos_{i}(F) = F and, hence, pc_{i}(F) = ρ(F). While this is not true when F is an arbitrary implicational formula, it is clear that pc_{i}(F) is indeed a definite formula. The following lemma states an additional property of pc_{i} that will be useful in the proof of Theorem 4.1.

4.8. Lemma. If F is an implicational formula and x and C are, respectively, a variable and a formula of the same type, then

pc_{i}(ρ([λx.F] C)) = ρ([λx.pc_{i}(F)] pc(C)).

Proof. An easy induction on the structure of F shows that ρ([λx.F] C) is an implicational formula. Hence pos_{i} is defined on this formula and, consequently, the left-hand side of the equality is defined. We now claim that

pos_{i}(ρ([λx.F] C)) λ-conv [λx.pos_{i}(F)] pos(C).

Given this claim, it is clear that

ρ(pos_{i}(ρ([λx.F] C))) = ρ([λx.pos_{i}(F)] pos(C),

and the lemma follows by observing that ρ([λx.A] B) = ρ([λx.ρ(A)] ρ(B)).

Thus, it only remains to show the claim. Given any implicational formula F_{1}, we observe that if F_{1} ≡ F_{2} then pos_{i}(F_{1}) ≡ pos_{i}(F_{2}). In trying to show the claim, we may therefore assume that the bound variables of F are distinct from x and from the free variables of C. Making such an assumption, we now induce on the structure of F:

(a) F is of the form H ⊃ A. In this case ρ([λx.F] C) ≡ ρ(S_{C}^{x} H) ⊃ ρ(S_{C}^{x} A). Using the

definition of pos_{i} and arguments similar to those in Lemma 4.4, we see that

pos_{i}(ρ(S_{C}^{x} H) ⊃ ρ(S_{C}^{x} A)) λ-conv S_{pos(C)}^{x} pos(H) ⊃ S_{pos(C)}^{x} pos(A) The claim easily follows from these observations.

(b) F is of the form ∀y.F′. Since the bound variables of F are distinct from x and the free

variables of C, we see that

ρ([λx.F] C) ≡ ∀y.ρ([λx.F′] C).

Using the inductive hypothesis and the definitions of λ-conversion and of pos_{i} we see that

pos_{i}(ρ([λx.F] C)) λ-conv ∀y.[[λx.pos_{i}(F′)] pos(C)].

Observing that F(C) = F(pos(C)), it is clear that

∀y.[[λx.pos_{i}(F′)] pos(C)] λ-conv [λx.[∀y.pos_{i}(F′)]] pos(C).

The claim is now apparent from the definition of pos_{i}.

Using the two mappings pc and pc_{i}, the desired transformation on sequents may now be stated. This is the content of the following definition. 4.9. Definition. First, we extend pc_{i} to the class of all formulas of type o:

pc_{o}(F) = \{ \begin{matrix}pc_{i}(F), & if F is an implicational formula; \\ pc(F), & otherwise. \end{matrix}

The mapping pc_{s} on sequents is then defined as follows: pc_{s}(Γ ⟶ Δ) is the sequent that results by replacing each formula F in Γ by pc_{o}(F) and each formula G in Δ by pc(G).

We are now in a position to describe, in a precise manner, the transformation of LKH-derivations alluded to immediately after the statement of Theorem 4.1. We do this below, thereby proving the theorem.

Proof of Theorem 4.1 We assume initially that every formula in Γ and Δ is in principal normal form; we indicate how this requirement may be relaxed at the end. Now, a simple inductive argument on the heights of derivations convinces us of the following fact: If Θ′ and Λ′ are finite sequences of formulas that are obtained from Θ and Λ, respectively, by replacing each formula by one of its λ-normal forms, then Θ ⟶ Λ has a derivation only if Θ′ ⟶ Λ′ has a derivation in which the inference figure λ does not appear. Since every formula in Γ and Δ is in λ-normal form, we may assume that Γ ⟶ Δ has a derivation in which no use is made of the inference figure λ. Further, since every formula in Γ and Δ is closed, we may assume that each instance of the schemata Π−IA and Σ−IS in this derivation is obtained by substituting a closed formula for C; if a variable y does appear free in the formula substituted for C, then we replace each free occurrence of y in it and in the sequents in the derivation by a parameter of the same type as y that does not already appear in the derivation; it is easy to see that the result is still a derivation of the same kind, and that its endsequent is still Γ ⟶ Δ. Let T be such a derivation. We show below that T can be transformed into a derivation satisfying the requirements of the theorem.

To define the transformation, we need to distinguish between what we call the essential and the inessential sequents in T. A sequent (occurrence) is considered inessential if it appears above the lower sequent of a Π−IS, ⊃ −IS or ∼−IS inference figure along any path in the derivation. A sequent is essential if it is not inessential. We claim that every formula in the antecedent of an essential sequent is either a rigid atom or an implicational formula. Observe that from this claim it also follows that each essential sequent, except the endsequent, is the upper sequent of one of the figures Contraction, Interchange, Thinning, ∨−IS, ∧−IS, Σ−IS, ⊃−IA or Π−IA.

The claim is proved by inducing on the distance of an essential sequent from the endsequent. If this distance is 0, the claim is obviously true. Assuming then that the claim is true if the distance is d, we verify it for distance d + 1. Given the inductive hypothesis, we only need to consider the cases when the sequent in question is the upper sequent of an inference figure in which there is a formula in the antecedent of an upper sequent that is not in the antecedent of the lower sequent, i.e. one of the figures ∼−IS, ∨−IA, ∧−IA, ⊃−IA, ⊃−IS, Π−IA, and Σ−IA. The cases of ∼−IS and ⊃−IS are ruled out, given that we are considering essential sequents. Also, since the antecedent of the lower sequent contains only implicational formulas and rigid atoms, the figure in question cannot be one of ∨−IA, ∧−IA, or Σ−IA. The only cases that remain are ⊃ −IA and Π−IA. In the first case, i.e. when the inference figure in question is

Θ_{1} ⟶ Λ_{1}, F  G, Θ_{2} ⟶ Λ_{2}
F ⊃ G, Θ_{1}, Θ_{2} ⟶ Λ_{1}, Λ_{2}

the principal formula must be an implicational formula, and G must therefore be a rigid atom. From this it is clear that the claim holds in this case. If the inference figure is Π−IA, i.e. of the form

{ρ(P C), Θ ⟶ Λ \atop Π P, Θ ⟶ Λ}

the principal formula must again be an implicational formula, and so P must be of the form λx.F where F is an implicational formula. But then it is easily seen that ρ(P C) must be an implicational formula and the claim is verified.

Now let e(T) be the structure that results from removing all the inessential sequents from T; e(T) is a derivation of Γ ⟶ Δ but for the fact that some of its leaf sequents are not axioms: Such sequents are of the form Ξ ⟶ Φ, P, where P is ∼F, Π B or F ⊃ G. Let pe(T) be the result of replacing each Θ ⟶ Λ in e(T) by pc_{s}(Θ ⟶ Λ). We claim that each pair of upper sequent(s) and lower sequent in pe(T) is an instance of the same inference figure schema as the corresponding pair in e(T). To show this, we consider each of the possible cases in e(T) and check the corresponding pairs in pe(T). The claim is easily verified if the pair is an instance of Contraction, Interchange or Thinning. The cases for ∨−IS and ∧−IS are similarly clear, given Lemma 4.3. If the pair is an instance of ⊃ −IA, the principal formula is an implicational formula of the form F ⊃ A. Observing then that pc_{i}(F ⊃ A) = pc(F) ⊃ pc(A), the claim follows in this case as well. If the pair from e(T) is an instance of Σ−IS, i.e. of the form

{Θ ⟶ Λ, ρ(P C) \atop Θ ⟶ Λ, Σ P}

the claim follows from Lemma 4.3 and Corollary 4.5; pc(Σ P) = Σ pc(P) and

pc(ρ(P C)) = ρ(pc(P) pc(C)).

We note further that, since C is a closed formula, pc(C) ∈ HB and so the corresponding figure in pe(T) is actually an instance of Σ−IS^{+}. Finally, let the pair in e(T) be an instance of Π−IA, i.e. of the form

{ρ(P C), Θ ⟶ Λ \atop Π P, Θ ⟶ Λ}

By our earlier observations Π P is an implicational formula, and hence P is of the form λx.F, where F is an implicational formula. Using Lemma 4.8, we see that

pc_{i}(ρ((λx.F) C)) = ρ([λx.pc_{i}(F)] pc(C)).

Noting now that pc_{i}(Π [λx.F]) ≡ [Π [λx.pc_{i}(F)]] and that pc(C) ∈ HB, it is clear that the corresponding pair in pe(T) is also an instance of Π−IA, and in fact of Π−IA^{+}.

Given the forms of formulas in Γ and Δ, we observe that pc_{s}(Γ ⟶ Δ) = Γ ⟶ Δ. We also note that if A is an atomic formula and A ≡ A′, then pc_{o}(A) = pc(A′). Thus we may conclude, from the above considerations and Lemma 4.3, that pe(T) would be a derivation of Γ ⟶ Δ of the sort required by the theorem but for the fact that some of its leaf sequents are of the form Θ ⟶ Λ, ⊤. However, we may adjoin derivations of the form

⟶ ⊤

sequence of Thinnings and Interchanges

Θ ⟶ Λ, ⊤

above sequents of this sort to obtain a genuine LKH-derivation that satisfies the theorem.

The above argument is adequate in the case that each formula in Γ and Δ is in principal normal form. If this is not the case, then we proceed as follows. First we construct a derivation of the requisite sort for Γ′ ⟶ Δ′, where Γ′ and Δ′ are obtained from Γ and Δ respectively by placing each formula in principal normal form. A simple inductive argument then suffices to show that this derivation may be converted into one for Γ ⟶ Δ by replacing some of the formulas in the derivation by formulas that they convert to via the rule of α-conversion. 4.10. Example. An illustration of the transformation described in the proof of Theorem 4.1 may be provided by considering the derivation presented at the beginning of this section. This would be transformed into the following:

⟶ ⊤

Thinning

⟶ ⊤, ∃y.[P y]

Interchange

⟶ ∃y.[P y], ⊤

\begin{aligned}[P A] ⟶ [P A] \\ & Σ−IS \\ [P A] ⟶ ∃y.[P y] \end{aligned}

⊃−IA

⊤ ⊃ [P A] ⟶ ∃y.[P y], ∃y.[P y]

Contraction

⊤ ⊃ [P A] ⟶ ∃y.[P y] Π−IA

∀x.[x ⊃ [P A]] ⟶ ∃y.[P y]

The content of Theorem 4.1 may be expressed by the description of a simplified sequent calculus for definite sentences and goal formulas. Let LKHD be the subcalculus of LKH with exactly the same initial sequents but with inference figures restricted to being instances of the schemata Contraction, Interchange, Thinning, ∨−IS, ∧−IS, Σ−IS^{+}, ⊃−IA, and Π−IA^{+}. In the discussions below we shall be concerned with derivations for sequents of the form Γ ⟶ Δ, where Γ is any finite sequence of definite sentences and closed positive atoms and Δ is a finite sequence of closed goal formulas. By virtue of Theorem 4.1 we see that such a sequent has an LKH-derivation exactly when it has an LKHD-derivation. In considering questions about derivations for such a sequent we may, therefore, restrict our attention to the calculus LKHD, and we implicitly do so below.

Proofs from Higher-Order Definite Sentences. We now use the preceding results to demonstrate that higher-order definite sentences and goal formulas retain the prooftheoretic properties of the corresponding first-order formulas that were discussed in Section 1. In this endeavor, we use the characteristics of the higher-order formulas observed in the two lemmas below. The first lemma subsumes the statement that a finite set of higher-order definite sentences is consistent. 4.11. Lemma. If Γ is a finite sequence of definite sentences and closed positive atoms, then there can be no derivation for Γ ⟶ . Proof. Suppose the claim is false. Then there is a least h and a Γ of the requisite sort such that Γ ⟶ has a derivation of height h. Since Γ ⟶ is not an initial sequent, h is evidently not 1. Consider now by cases the inference figures of which Γ ⟶ could be the lower sequent, i.e. the figures Contraction, Thinning and Interchange in the antecedent, Π−IA^{+}, and ⊃ −IA. In each of these cases it is easily observed that there must be a finite sequence of definite sentences and closed positive atoms Γ′ such that Γ′ ⟶ has a derivation of height < h. This contradicts the leastness of h.

The lemma below relates the notions of classical and intuitionistic provability of a goal formula from a set of definite sentences. 4.12. Lemma. Let Γ be a finite sequence of definite sentences and closed positive atoms and let G be a closed goal formula. Then Γ ⟶ G has a derivation only if it has one in which there is at most one formula in the succedent of each sequent. Proof. We claim that a slightly stronger statement is true: A sequent of the form Γ ⟶ G_{1}, …, G_{n}, where Γ consists only of definite sentences and closed positive atoms and G_{1}, …, G_{n} are closed goal formulas, has a derivation only if there is an i such that 1 ≤ i ≤ n and Γ ⟶ G_{i} has a derivation in which at most one formula appears in the succedent of each sequent.

The claim is proved by an induction on the heights of derivations for sequents of the sort hypothesized in it. If the height is 1, then n = 1 and the claim is obviously true. Let us, therefore, assume the height is h + 1 and consider the possible cases for the inference figure that appears at the end of the derivation. If this figure is a Contraction, Thinning or Interchange in the succedent, the claim follows directly from the inductive hypothesis; in the case of Thinning, we only need to observe that, by Lemma 4.11, n > 1. The cases of Contraction, Thinning, and Interchange in the antecedent, ∨−IS, ∧−IS, Σ−IS^{+} and Π−IA^{+}, also follow from the hypothesis with a little further argument. Consider, for instance the case when the figure is an ∧−IS. The derivation at the end then has the following form:

\begin{matrix}Γ ⟶ G_{1}, …, G_{n−1}, G_{n}^{1} & Γ ⟶ G_{1}, …, G_{n−1}, G_{n}^{2} \\ Γ ⟶ G_{1}, …, G_{n−1}, G_{n}^{1} ∧ G_{n}^{2} \end{matrix}

By the hypothesis, there must be a derivation of the requisite sort either for Γ ⟶ G_{i} for some i, 1 ≤ i ≤ n − 1, or for both Γ ⟶ G_{n}^{1} and Γ ⟶ G_{n}^{2}. In the former case the claim follows directly, and in the latter case we use the two derivations together with an ∧−IS inference figure to construct a derivation of the requisite sort for Γ ⟶ G_{n}^{1} ∧ G_{n}^{2}.

The only remaining case is that of ⊃−IA, i.e. when the inference figure in question is of the form

\begin{matrix}Γ_{1} ⟶ G_{1}, …, G_{k}, G & A, Γ_{2} ⟶ G_{k+1}, …, G_{n} \\ G ⊃ A, Γ_{1}, Γ_{2} ⟶ G_{1}, …, G_{n} \end{matrix}

From Lemma 4.11 it follows that k < n. By the hypothesis, we see that there is a derivation of the requisite sort either for Γ_{1} ⟶ G_{i} for some i between 1 and k or for Γ_{1} ⟶ G. In the former case, by adjoining a sequence of Thinning and Interchange figures below the derivation for Γ_{1} ⟶ G_{i} we obtain the required derivation for G ⊃ A, Γ_{1}, Γ_{2} ⟶ G_{i}. In the latter case, using the induction hypothesis again we see that there is a derivation of the required sort for A, Γ_{2} ⟶ G_{j} for some j between k + 1 and n. This derivation may be combined with the one for Γ_{1} ⟶ G to obtain the required derivation for G ⊃ A, Γ_{1}, Γ_{2} ⟶ G_{j}.

Lemmas 4.11 and 4.12 permit us to further restrict our sequent calculus in the context of definite sentences. To make the picture precise, let us assume that Γ is a finite sequence of definite sentences and closed positive atoms, and that G is a goal formula such that Γ ⟶ G has a derivation. Then, using Lemma 4.12 we see that this sequent has a derivation in which there is no occurrence of Contraction or Interchange in the succedent. Using Lemma 4.11 it may be seen that such a derivation is also one in which the figure Thinning in the succedent does not appear. Thus, in considering questions about derivability for sequents of the sort described above, we may dispense with the structural inference figures pertaining to the succedent. This fact is made use of in the proof of Theorem 4.14 and in the discussions that follow it. We present this theorem after introducing a convenient notational convention.

4.13. Definition. Let D be the definite sentence ∀x̄.G ⊃ A. Then |D| denotes the set of all closed positive instances of G ⊃ A, i.e.

|D| = {φ(G ⊃ A) | φ is a closed positive substitution for x̄}.

This notation is extended to sets of definite sentences: If P is such a set,

|P| = ⋃{|D| | D ∈ P}.

From this definition it readily follows that |D| and |P| are both collections of definite sentences. 4.14. Theorem. Let Γ be a finite sequence of definite sentences and closed positive atoms, and let G be a closed goal formula. Then there is a derivation for Γ ⟶ G if and only if

(i) G is G_{1} ∧ G_{2} and there are derivations for Γ ⟶ G_{1} and Γ ⟶ G_{2}, or (ii) G is G_{1} ∨ G_{2} and there is a derivation for either Γ ⟶ G_{1} or Γ ⟶ G_{2}, or (iii) G is Σ P and there is a C ∈ HB such that Γ ⟶ ρ(P C) has a derivation, or (iv) G is an atom and either G is ⊤, or G ≡ A for some A in Γ, or, for some definite

sentence D in Γ, G′ ⊃ A ∈ |D|, G ≡ A, and there is a derivation for Γ ⟶ G′. Proof. (⊃) As we have noted, there is a derivation for a sequent of the sort described in the Theorem only if there is one in which there are no structural figures pertaining to the succedent. An induction on the heights of such derivations now proves the theorem in this direction.

If Γ ⟶ G has a derivation of height 1, then G is ⊤ or Γ is A and G ≡ A. In either case the theorem is true. For the case when the height is h+1, we consider each possibility for the last inference figure in the derivation. If it is one of ∧−IS, ∨−IS or Σ−IS^{+}, the theorem is evidently true. If it is a Contraction in the antecedent, i.e. of the form

{F, F, Γ ⟶ G \atop F, Γ ⟶ G}

we see that the upper sequent is of the kind described in the theorem and, in fact, has a derivation of height h. A recourse to the induction hypothesis now completes the proof. For instance, assume that G is of the form G_{1}∨G_{2}. By the hypothesis, there is a derivation for F, F, Γ ⟶ G_{i} for i = 1 or i = 2. By adjoining below this derivation a Contraction in the antecedent, we obtain a derivation for F, Γ ⟶ G_{i}. The analysis for the cases when G has a different structure follows an analogous pattern.

In the cases when the last inference figure is a Thinning or an Interchange in the antecedent, the argument is similar to that of Contraction. If the figure is Π−IA^{+}, i.e. of the form

{ρ(P C), Γ ⟶ G \atop Π P, Γ ⟶ G}

we see that ρ(P C) and Π P are both definite sentences and, further, that |ρ(P C)| ⊆ |Π P |. Applying the induction hypothesis to the upper sequent, the proof may now be completed by arguments similar to those outlined in the case of Contraction in the antecedent.

The only remaining case is that of ⊃ −IA. In this case, by Lemma 4.11 we observe that the derivation at the end has the following form

\begin{matrix}Γ_{1} ⟶ G′ & A, Γ_{2} ⟶ G \\ G′ ⊃ A, Γ_{1}, Γ_{2} ⟶ G \end{matrix}

The right upper sequent of this inference figure is evidently of the form required for the induction hypothesis. Once again using arguments similar to those in the case of Contraction in the antecedent, the proof may be completed in all cases except when G ≡ A. But if G ≡ A, we observe that the theorem is still true, since a derivation for G′ ⊃ A, Γ_{1}, Γ_{2} ⟶ G′ may be constructed by adjoining a sequence of Thinning and Interchange inference figures below the derivation for Γ_{1} ⟶ G′. (⊂) The only case that needs explicit consideration here is that when, for some definite sentence D in Γ, there is a G′ ⊃ A ∈ |D| such that G ≡ A and Γ ⟶ G′ has a derivation. In this case a derivation for Γ ⟶ G may be constructed as follows:

Γ ⟶ G′  A ⟶ G ⊃−IA
G′ ⊃ A, Γ ⟶ G

sequence of Π−IA^{+}

D, Γ ⟶ G sequence of Interchanges and a Contraction

Γ ⟶ G

In Section 1 we outlined the proof-theoretic properties of first-order definite sentences and goal formulas that play a pivotal role in their use as a basis for programming. Theorem 4.14 demonstrates that our higher-order generalizations of these formulas retain these properties. Thus, if G is a higher-order goal formula whose free variables are included in the listing x_{1}, …, x_{n} and P is a finite set of higher-order definite sentences, we see from clause (iii) of Theorem 4.14 that ∃x_{1}…. ∃x_{n}.G is provable from P just in case there is a closed positive substitution φ for x_{1}, …, x_{n} such that φ(G) is provable from P. Hence, sets of higher-order definite sentences and higher-order goal formulas may be construed, respectively, as programs and queries in a manner exactly analogous to the first-order case. Furthermore, clauses (i) – (iii) show that ∧, ∨ and the existential quantifier provide primitives for search specification in exactly the same way as in the first-order setting. Finally, by virtue of (iv), higher-order definite sentences provide the basis for defining nondeterministic procedures. Notice that in a definite sentence of form ∀x̄.(G ⊃ A), the head of A must be a parameter, and construing this formula as a procedure defining this head of A, therefore, makes good sense.

Theorem 4.14 also provides the skeleton for a procedure that may be used for determining whether a goal formula is provable from a set of definite sentences. In essence, clauses (i) – (iii) describe the means by which the search for a proof of a complex goal formula may be reduced to the search for proofs of a set of atoms. The search for a proof of an atomic goal may be progressed by “backchaining” on definite sentences in the manner indicated by clause (iv). A precise description of this proof procedure requires the explication of the notion of higher-order unification, and we undertake this task in the next section. We note, however, that the steps mentioned above must simplify the search in some manner if they are to be effective in finding a proof. That they do have this effect may be seen by associating a measure, indexed by a finite set of definite sentences, with each goal formula. For this purpose, we identify the notion of a reduced path in a derivation as a sequence of sequents that results by the removal of the lower sequents of structural inference figures from a path in the derivation; intuitively, the length of a reduced path is a count of the number of operational inference figures that appear along the corresponding path. Letting the true height of a derivation be the length of the longest reduced path in the derivation, the required measure may be defined as follows. 4.15. Definition. Let Γ be a finite sequence of definite sentences, and let G be a closed goal formula. Further, let k be the least among the true heights of derivations for Γ ⟶ G in which there appear no structural inference figures pertaining to the succedent; if no such derivation exists, k = ω. Then

μ_{Γ}(G) = \{ \begin{matrix}2^{k}, & if k < ω; \\ ω, & otherwise. \end{matrix}

The measure is extended to be relative to a finite set, P, of definite sentences by defining μ_{P}(G) = μ_{Γ}(G) where Γ is a listing of the members of P. This extension is clearly independent of the particular listing chosen.

The properties of this measure that are of interest from the perspective of describing a proof procedure are stated in the following Lemma. 4.16. Lemma. Let P be a finite set of definite sentences and let G be a closed goal formula that is provable from P. Then μ_{P}(G) > 0 and μ_{P}(G) < ω. Further,

(i) If G is an atom other than ⊤ then there is a G′ ⊃ G ∈ |P| such that μ_{P}(G′) < μ_{P}(G). (ii) If G is G_{1} ∨ G_{2} then μ_{P}(G_{i}) < μ_{P}(G) for i = 1 or i = 2. (iii) If G is G_{1} ∧ G_{2} then μ_{P}(G_{1}) + μ_{P}(G_{2}) < μ_{P}(G). (iv) If G is ΣP then for some C ∈ HB it is the case that μ_{P}(ρ(P C)) < μ_{P}(ΣP).

Proof. μ_{P}(G) is obviously greater that 0. Since G is provable from P, it is also obvious that μ_{P}(G) < ω. Now let Γ be a finite sequence of definite sentences such that Γ ⟶ G has a derivation of true height h. A reexamination of the proof of Lemma 4.14 reveals the following facts: If G is G_{1} ∨ G_{2}, then Γ ⟶ G_{i} has a derivation of true height < h for i = 1 or i = 2. If G is G_{1} ∧ G_{2}, then Γ ⟶ G_{i} has a derivation of true height < h for i = 1 and i = 2. If G is Σ P, then there is a C ∈ HB such that Γ ⟶ ρ(P C) has a derivation of true height < h. If G is an atom, then there is a G′ ⊃ G ∈ |P| such that Γ ⟶ G′ has a derivation of true height < h. From these observations, the rest of the lemma follows easily.

5. Searching for Proofs from Definite Sentences We now turn to the task of describing a procedure for determining whether there

is a proof for the existential closure of a goal formula from a set of definite sentences. As already noted, the description of such a procedure requires a consideration of the problem of unifying two higher-order formulas. This problem has been studied by several researchers, and in most extensive detail by [15]. In the first part of this section, we summarize this problem and detail those aspects of its solution in [15] that are pertinent to our current endeavor. We then introduce the notion of a P-derivation. P-derivations are a generalization to the higher-order context of the notion of SLD-derivations described in [2] and prevalent in most discussions of first-order definite sentences. At one level, they are intended to be syntactic objects for demonstrating the existence of a proof for a goal formula and our discussions show their correctness from this perspective. At another level, they are intended to provide a basis for an actual proof procedure — a symbol manipulating procedure that searches for P-derivations would constitute an interpreter for a programming paradigm that is based on higher-order definite sentences — and we explore some of their properties that are pertinent to the description of such a procedure.

The Higher-Order Unification Problem. Let us call a pair of formulas of the same type a disagreement pair. A disagreement set is then a finite set, {⟨F_{i}, H_{i}⟩ | 1 ≤ i ≤ n}, of disagreement pairs, and a unifier for the set is a substitution σ such that, for 1 ≤ i ≤ n, σ(F_{i}) = σ(H_{i}). The higher-order unification problem is then the following: Given a disagreement set, we desire to determine whether it has unifiers, and to explicitly provide a unifier if it does have one.

The problem described above is a generalization of the well-known unification problem for first-order terms. The higher-order unification problem has several properties that are, in a certain sense, divergent from those of the problem in the first-order case. For instance, the question of whether a unifier exists for an arbitrary disagreement set in the higherorder context is an undecidable question [10, 14, 17], whereas the corresponding question for first-order terms is decidable. As another example, it has been shown [12] that most general unifiers do not always exist for unifiable higher-order disagreement pairs. Despite these characteristics of the problem, a systematic search can be made for unifiers of a given disagreement set, and we discuss this aspect below.

Huet, in [15], describes a procedure for determining the existence of unifiers for a given disagreement set and shows that, whenever unifiers do exist, the procedure may be used to provide some of them. The basis for this procedure is in the fact that there are certain disagreement sets for which at least one unifier may easily be provided and, similarly, there are other disagreement sets for which it is easily manifest that no unifiers can exist. Given an arbitrary disagreement set, the procedure then attempts to reduce it to a disagreement set of one of these two kinds. This reduction proceeds by an iterative use of two kinds of simplifying functions, called SIMPL and MATCH, on disagreement sets. Since our notion of a P-derivation uses these functions in an intrinsic way, we devote some effort to describing them below.

In presenting the functions SIMPL and MATCH and in analyzing their properties, the normal form for formulas that is introduced by the following definition is useful. 5.1. Definition. A β-normal form F̃ = λx_{1}…. λx_{n}.[H A_{1} … A_{m}] is said to be a βη-long form if the type of H is of the form α_{1} → ⋯ → α_{m} → α_{0}, where α_{0} is an atomic type, and, for 1 ≤ i ≤ m, A_{i} is also a βη-long form. If F is a formula such that F λ-conv F̃, then F̃ is said to be a βη-long form of F. Given a βη-long form F = λx̄.[H A_{1} … A_{m}], a count of the number of occurrences of applications in F is provided by the following recursively defined measure on F:

ξ(F) = m + ∑_{i=1}^{m} ξ(A_{i}).

It is clear that every formula has a βη-long form; such a form may be obtained by first converting the formula to a β-normal form, and then performing a sequence of ηexpansions. We shall write F̃ below to denote a βη-long form of a formula F. The formula thus denoted is ambiguous only up to a renaming of bound variables. To see this, let F_{1} = λx_{1} … λx_{m}.[H A_{1} … A_{r}] and F_{2} = λy_{1}…. λy_{n}.[H′ B_{1} … B_{s}] be two βη-long forms such that F_{1} λ-conv F_{2}. Observing that F_{1} and F_{2} must have the same λ-normal forms, it is clear that λx_{1} … λx_{m}.H ≡ λy_{1}…. λy_{n}.H′, and hence m = n and r = s. Furthermore, for all i, 1 ≤ i ≤ r, it must be the case that λx_{1} … λx_{m}.A_{i} λ-conv λy_{1} … λy_{m}.B_{i}. A simple argument by induction on the measure in Definition 5.1 then shows that F_{1} ≡ F_{2}. This observation permits us to extend the measure ξ to arbitrary formulas. For any formula F, we may define ξ(F) = ξ(F̃). Given the uniqueness of βη-long forms up to α-conversions and the fact that ξ(F_{1}) = ξ(F_{2}) for any βη-long forms F_{1} and F_{2} such that F_{1} ≡ F_{2}, it follows that this extension of ξ is well-defined.

Given any formula F and any substitution σ, it is apparent that σ(F) = σ(F̃). The interest in the βη-long form of representation of formulas stems from the fact that the effects of substitutions on formulas in this form can be analyzed easily. As an instance of this, we observe the following lemma that is the basis of the first phase of simplification in the search for unifiers for a given disagreement set. In this lemma, and in the rest of this section, we use the notation U(D) to denote the set of unifiers for a disagreement set D. A proof of this lemma is contained in [15] and also in [25]. 5.2. Lemma. Let F_{1} = λx̄[H_{1} A_{1} … A_{r}] and F_{2} = λx̄[H_{2} B_{1} … B_{s}] be two rigid βη-long forms of the same type. Then σ ∈ U({⟨F_{1}, F_{2}⟩}) if and only if

(i) H_{1} = H_{2} (and, therefore, r = s), and (ii) σ ∈ U({⟨λx̄.A_{i}, λx̄.B_{i}⟩ | 1 ≤ i ≤ r}).

Let us say that F is rigid (flexible) just in case F̃ is rigid (flexible), and let us refer to the arguments of F̃ as the arguments of F. If F_{1} and F_{2} are two formulas of the same type, it is evident that βη-long forms of F_{1} and F_{2} must have binders of the same length. Furthermore, we may, by a sequence of α-conversions, arrange their binders to be identical. If F_{1} and F_{2} are both rigid, then Lemma 5.2 provides us a means for either determining that F_{1} and F_{2} have no unifiers or for reducing the problem of finding unifiers for F_{1} and F_{2} to that of finding unifiers for the arguments of these formulas. This, in fact, is the nature of the simplification effected on a given unification problem by the function SIMPL. 5.3. Definition. The function SIMPL on sets of disagreement pairs is defined as follows:

(1) If D = ∅ then SIMPL(D) = ∅.

(2) If D = {⟨F_{1}, F_{2}⟩}, and (a) if F_{1} is a flexible formula then SIMPL(D) = D; otherwise

(b) if F_{2} is a flexible formula then SIMPL(D) = {⟨F_{2}, F_{1}⟩};

(c) otherwise F_{1} and F_{2} are both rigid formulas. Let λx̄.[C_{1} A_{1} … A_{r}] and λx̄.[C_{2} B_{1} … B_{s}] be βη-long forms for F_{1} and F_{2}. If C_{1} ≠ C_{2} then SIMPL(D) = F; otherwise SIMPL(D) = SIMPL({⟨λx̄.A_{i}, λx̄.B_{i}⟩ | 1 ≤ i ≤ r}).

(3) Otherwise D has at least two members. Let D = {⟨F_{i}, G_{i}⟩ | 1 ≤ i ≤ n}. (a) If SIMPL({⟨F_{i}, G_{i}⟩}) = F for some i then SIMPL(D) = F;

(b) Otherwise SIMPL(D) = ⋃_{i=1}^{n} SIMPL({⟨F_{i}, G_{i}⟩}).

Clearly, SIMPL transforms a given disagreement set into either the marker F or a disagreement set consisting solely of “flexible-flexible” or “flexible-rigid” formulas. By an abuse of terminology, we shall regard F as a disagreement set that has no unifiers. The intention, then, is that SIMPL transforms the given set into a simplified set that has the same unifiers. The following lemma shows that SIMPL achieves this purpose in a finite number of steps. 5.4. Lemma. SIMPL is a total computable function on sets of disagreement pairs. Further, if D is a set of disagreement pairs then σ ∈ U(D) if and only if SIMPL(D) ≠ F and σ ∈ U(SIMPL(D)). Proof. We define a measure ψ on sets of disagreement pairs in the following fashion. If D = {⟨F_{i}, G_{i}⟩ | 1 ≤ i ≤ n}, then

ψ(D) = n + ∑_{i=1}^{n} ξ(F_{i}).

The lemma follows from Lemma 5.2 by an induction on this measure.

The first phase in the process of finding unifiers for a given disagreement set D thus consists of evaluating SIMPL(D). If the result of this is F, D has no unifiers. On the other hand, if the result is a set that is either empty or has only flexible-flexible pairs, at least one unifier can be provided easily for the set, as we shall see in the proof of Theorem 5.14; such a set is, therefore, referred to as a solved set. If the set has at least one flexiblerigid pair, then a substitution for the head of the flexible formula needs to be considered so as to make the heads of the two formulas in the pair identical. There are essentially two kinds of “elementary” substitutions that may be employed for this purpose. The first kind of substitution is the one that makes the head of the flexible formula “imitate” that of the rigid formula. In the context of first-order terms this is, in fact, the only kind of substitution that needs to be considered. If the head of the flexible formula is a higherorder variable, however, there is also another possibility. This is that of “projecting” one of the arguments of the flexible formula into the head position, in the hope that the head of the resulting formula becomes identical to the head of the rigid one or may be made so by a subsequent substitution. There are, thus, a set of substitutions, each of which may be investigated separately as a component of a complete unifier. The purpose of the function MATCH that is defined below is to produce these substitutions. 5.5. Definition. Let V be a set of variables, let F_{1} be a flexible formula, let F_{2} be a rigid formula of the same type as F_{1}, and let λx̄.[f A_{1} … A_{r}], and λx̄.[C B_{1} … B_{s}] be βη-long forms of F_{1} and F_{2}. Further, let the type of f be α_{1} → ⋯ → α_{r} → β, where β is primitive and, for 1 ≤ i ≤ r, let w_{i} be a variable of type α_{i}. The functions IMIT, PROJ, and MATCH are then defined as follows:

(i) If C is a variable (appearing also in x̄), then IMIT(F_{1}, F_{2}, V) = ∅; otherwise

IMIT(F_{1}, F_{2}, V) = {{⟨f, λw_{1} … λw_{r}.[C [h_{1} w_{1} … w_{r}] … [h_{s} w_{1} … w_{r}]]⟩}},

where h_{1}, …, h_{s} are variables of appropriate types not contained in V ∪ {w_{1}, …, w_{r}}. (ii) For 1 ≤ i ≤ r, if α_{i} is not of the form β_{1} → … → β_{t} → β then PROJ_{i}(F_{1}, F_{2}, V) = ∅;

otherwise,

PROJ_{i}(F_{1}, F_{2}, V) = {{⟨f, λw_{1} … λw_{r}.[w_{i} [h_{1} w_{1} … w_{r}] … [h_{t} w_{1} … w_{r}]]⟩}},

where h_{1}, …, h_{t} are variables of appropriate type not contained in V ∪ {w_{1}, …, w_{r}}.

(iii) MATCH(F_{1}, F_{2}, V) = IMIT(F_{1}, F_{2}, V) ∪ ( ⋃_{1≤i≤r} PROJ_{i}(F_{1}, F_{2}, V)).

The purpose of MATCH is to suggest a set of substitutions that may form “initial segments” of unifiers and, in this process, bring the search for a unifier closer to resolution. To describe the sense in which MATCH achieves this purpose precisely, we need the following measure on substitutions: 5.6. Definition. Let φ = {⟨f_{i}, T_{i}⟩ | 1 ≤ i ≤ n} be a substitution. We define a measure on φ as follows:

π(φ) = n + ∑_{i=1}^{n} ξ(T_{i}).

The correctness of MATCH is now stated in the lemma below. We omit a proof of this lemma, referring the interested reader to [15] or [25]. 5.7. Lemma. Let V be a set of variables, let F_{1} be a flexible formula and let F_{2} be a rigid formula of the same type as F_{1}. If there is a substitution σ ∈ U({⟨F_{1}, F_{2}⟩}) then there is a substitution φ ∈ MATCH(F_{1}, F_{2}, V) and a corresponding substitution σ′ such that

(i) σ =_{V} σ′ ∘ φ, and (ii) π(σ′) < π(σ).†

A unification procedure may now be described based on an iterative use of SIMPL and MATCH. A procedure that searches for a P-derivation, a notion that we describe next, actually embeds such a unification procedure within it.

P-Derivations. Let the symbols G, D, θ and V, perhaps with subscripts, denote sets of formulas of type o, disagreement sets, substitutions and sets of variables, respectively. The relation of being “P-derivable from” between tuples of the form ⟨G, D, θ, V⟩ is defined in the following manner.

† This lemma may actually be strengthened: If f ∈ V, then there is exactly one φ corresponding to each σ.

5.8. Definition. Let P be a set of definite sentences. We say a tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ is P-derivable from the tuple ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ if D_{1} ≠ F and, in addition, one of the following situations holds:

(1) (Goal reduction step) θ_{2} = ∅, D_{2} = D_{1}, and there is a goal formula G ∈ G_{1} such that (a) G is ⊤ and G_{2} = G_{1} − {G} and V_{2} = V_{1}, or

(b) G is G_{1} ∧ G_{2} and G_{2} = (G_{1} − {G}) ∪ {G_{1}, G_{2}} and V_{2} = V_{1}, or

(c) G is G_{1} ∨ G_{2} and, for i = 1 or i = 2, G_{2} = (G_{1} − {G}) ∪ {G_{i}} and V_{2} = V_{1}, or (d) G is Σ P and for some variable y ∉ V_{1} it is the case that V_{2} = V_{1} ∪ {y} and

G_{2} = (G_{1} − {G}) ∪ {λnorm(P y)}.

(2) (Backchaining step) Let G ∈ G_{1} be a rigid positive atom, and let D ∈ P be such that D ≡ ∀x_{1}…. ∀x_{n}.G′ ⊃ A for some sequence of variables x_{1}, …, x_{n} for which no x_{i} ∈ V_{1}. Then θ_{2} = ∅, V_{2} = V_{1} ∪ {x_{1}, …, x_{n}}, G_{2} = (G_{1} − {G}) ∪ {G′}, and D_{2} = SIMPL(D_{1} ∪ {⟨G, A⟩}).

(3) (Unification step) D_{1} is not a solved set and for some flexible-rigid pair ⟨F_{1}, F_{2}⟩ ∈ D_{1}, either MATCH(F_{1}, F_{2}, V_{1}) = ∅ and D_{2} = F, or there is a σ ∈ MATCH(F_{1}, F_{2}, V_{1}) and it is the case that θ_{2} = σ, G_{2} = σ(G_{1}), D_{2} = SIMPL(σ(D_{1})), and, if σ = {⟨x, T ⟩}, V_{2} = V_{1} ∪ F(T).

Let us call a finite set of goal formulas a goal set, and a disagreement set that is F or consists solely of pairs of positive formulas a positive disagreement set. If G_{1} is a goal set and D_{1} is a positive disagreement set then it is clear, from an inspection of the above definition, the definitions 5.3 and 5.5, and the fact that a positive formula remains a positive formula under a positive substitution, that G_{2} is a goal set and D_{2} a positive disagreement set for any tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩. 5.9. Definition. Let G be a goal set. Then we say that a sequence ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩_{1≤i≤n} is a P-derivation sequence for G just in case G_{1} = G, V_{1} = F(G_{1}), D_{1} = ∅, θ_{1} = ∅, and, for 1 ≤ i < n, ⟨G_{i+1}, D_{i+1}, θ_{i+1}, V_{i+1}⟩ is P-derivable from ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩.

From our earlier observations, and an easy induction on the length of the sequence, it is clear that in a P-derivation sequence for a goal set G each G_{i} is a goal set and each D_{i} is a positive disagreement set. We make implicit use of this observation in our discussions below. In particular, we intend unqualified uses of the symbols G and D to be read as syntactic variables for goal sets and positive disagreement sets, respectively.

A P-derivation sequence ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩_{1≤i≤n} terminates, i.e. is not contained in a longer sequence, if

(a) G_{n} is either empty or is a goal set consisting solely of flexible atoms and D_{n} is either empty or consists solely of flexible-flexible pairs, or (b) D_{n} = F. In the former case we say that it is a successfully terminated sequence. 5.10. Definition. A P-derivation sequence, ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩_{1≤i≤n}, for G that is a successfully terminated sequence is called a P-derivation of G and θ_{n} ∘ ⋯ ∘ θ_{1} is called its answer substitution. If G = {G} then we also say that the sequence is a P-derivation of G.

5.11. Example. Let P be the set of definite sentences in Example 3.3. Further, let f_{1} be a variable of type int → int and let G be the goal formula

[mapfun f_{1} [cons 1 [cons 2 nil]] [cons [g 1 1] [cons [g 1 2] nil]]].

Then the tuple ⟨G_{1}, D_{1}, ∅, V_{1}⟩ is P-derivable from ⟨{G}, ∅, ∅, {f_{1}}⟩ by a backchaining step, if

V_{1} = {f_{1}, f_{2}, l_{1}, l_{2}, x},
G_{1} = {[mapfun f_{2} l_{1} l_{2}]}, and
D_{1} = {⟨f_{1}, f_{2}⟩, ⟨x, 1⟩, ⟨[f_{1} x], [g 1 1]⟩, ⟨l_{1}, [cons 2 nil]⟩, ⟨l_{2}, [cons [g 1 2] nil]⟩},

where f_{2}, l_{1}, l_{2}, and x are variables. Similarly, if

V_{2} = V_{1} ∪ {h_{1}, h_{2}},
G_{2} = {[mapfun f_{2} l_{1} l_{2}]},
θ_{2} = {⟨f_{1}, λw.[g [h_{1} w][h_{2} w]]⟩}, and
D_{2} = {⟨l_{1}, [cons 2 nil]⟩, ⟨l_{2}, [cons [g 1 2] nil]⟩, ⟨x, 1⟩,
⟨[h_{1} x], 1⟩, ⟨[h_{2} x], 1⟩, ⟨f_{2}, λw.[g [h_{1} w] [h_{2} w]]⟩},

then the tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ is P-derivable from ⟨G_{1}, D_{1}, ∅, V_{1}⟩ by a unification step. It is, in fact, obtained by picking the flexible-rigid pair ⟨[f_{1} x], [g 1 1]⟩ from D_{1} and using the substitution provided by IMIT for this pair. If the substitution provided by PROJ_{1} was picked instead, we would obtain the tuple ⟨G_{2}, F, {⟨f_{1}, λw.w⟩}, V_{1}⟩.

There are several P-derivations of G, and all of them have the same answer substitution: {⟨f_{1}, λw.[g w 1]⟩}.

5.12. Example. Let P be a set of definite sentences that contains the definite sentence ∀x.[x ⊃ [P A]], where P and A are parameters of type int → o and int, respectively. Then, the following sequence of tuples constitutes a P-derivation of ∃y.[P y]:

⟨{∃y.[P y]}, ∅, ∅, ∅⟩, ⟨{[P y]}, ∅, ∅, {y}⟩, ⟨{x}, {⟨y, A⟩, ∅, {y, x}⟩, ⟨{x}, ∅, {⟨y, A⟩, {y, x}⟩.

Notice that this is a successfully terminated sequence, even though the final goal set contains a flexible atom. We shall see, in Theorem 5.14, that a goal set that contains only flexible atoms can be “solved” rather easily. In this particular case, for instance, the final goal set may be solved by applying the substitution {⟨x, ⊤⟩} to it.

As mentioned at the beginning of this section, a P-derivation of a goal formula G is intended to be an object that demonstrates the provability of G from the set of definite sentences P. Our next endeavor, culminating in the Theorems 5.14 and 5.18, is to show that this notion is true to our intention. In the process, we shall see that a P-derivation of G encodes enough information to make it possible to extract the result of a computation. We shall also observe some properties of P-derivations that are of interest from the perspective of constructing a procedure that searches for such a derivation of a goal formula. 5.13. Lemma. Let ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ be P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩, and let D_{2} ≠ F. Further let σ ∈ U(D_{2}) be a positive substitution such that every closed positive instance of the formulas in σ(G_{2}) is provable from P. Then

(i) σ ∘ θ_{2} ∈ U(D_{1}), and (ii) every closed positive instance of the formulas in σ ∘ θ_{2}(G_{1}) is provable from P. Proof. The lemma is proved by considering the cases in Definition 5.9. A goal reduction or a backchaining step. In these cases θ_{2} = ∅ and so σ ∘ θ_{2} = σ. Further, in a goal reduction step D_{2} = D_{1}, and in a backchaining step D_{1} ⊆ D_{2}. From these observations and the assumptions in the lemma, it follows that (i) is true. Similarly, it is clear that all the closed positive instances of σ ∘ θ_{2}(G) of each G ∈ G_{1} that is also an element of G_{2} are provable from P. To verify (ii), therefore, we only need to establish the truth of the previous statement for the case when the G ∈ G_{1} is not in G_{2}, and we do this below by considering the possibilities for such a G.

In the case that G is ⊤, the argument is obvious. If G is G_{1} ∨ G_{2}, then

σ ∘ θ_{2}(G) = σ ∘ θ_{2}(G_{1}) ∨ σ ∘ θ_{2}(G_{2}) = σ(G_{1}) ∨ σ(G_{2}).

Thus the closed positive instances of σ ∘ θ_{2}(G) are of the form G′ ∨ G′′ where G′ and G′′ are closed positive instances of σ(G_{1}) and σ(G_{2}) respectively. Noting that either σ(G_{1}) or σ(G_{2}) is an element of σ(G_{2}), the argument may be completed using the assumptions in the lemma and Theorem 4.14. A similar argument may be provided for the case when G is G_{1} ∧ G_{2}.

Before considering the remaining cases, we define a substitution that is parameterized by a substitution and a sequence of variables. Let c_{α} be an arbitrary parameter of type α. If ȳ is a sequence of variables and δ is a substitution, then

δȳ = {⟨x, c_{α}⟩ | x is a variable of type α such that x ∈ F(δ ∘ σ(y_{i})) for some y_{i} in ȳ}.

We note that if F is a positive formula all of whose free variables are included in the list ȳ and if δ is a positive substitution, then δȳ ∘ δ ∘ σ(F) is a closed positive formula.

Now let the G under consideration be Σ P. Any closed positive instance of σ ∘ θ_{2}(G) may be written in the form Σ (δ ∘ σ(P)) for a suitable δ; note that then δ ∘ σ(P) must itself be a closed positive formula. From Definition 5.9, we see that, for some y, λnorm(P y) ∈ G_{2} and hence σ(P y) ∈ σ(G_{2}). It is easily seen that δ_{y} ∘ δ ∘ σ(P y) is a closed positive instance of σ(P y) and is, therefore, provable from P. But now we observe that

δ_{y} ∘ δ ∘ σ(P y) = ρ([δ ∘ σ(P) δ_{y} ∘ σ ∘ δ(y)]).

Using Theorem 4.14 it then follows that Σ (δ ∘ σ(P)), is provable from P. The choice of δ having been arbitrary, we may thus conclude that any closed positive instance of σ ∘ θ_{2}(G) is provable from P.

The only other case to consider is when G is removed by a backchaining step. In this case, by Definition 5.9 and Lemma 5.4, there must be a D ∈ P such that

D ≡ ∀x̄.G′ ⊃ A, G′ ∈ G_{2}, and σ(G) = σ(A).

Once again, we observe that any closed positive instance of σ ∘ θ_{2}(G) may be written as δ ∘ σ(G) for a suitably chosen δ. Now δx̄ ∘ δ ∘ σ(G′ ⊃ A) is a closed positive instance of G′ ⊃ A, and hence is a member of |P|. Further,

δx̄ ∘ δ ∘ σ(G′ ⊃ A) = δx̄ ∘ δ ∘ σ(G′) ⊃ δx̄ ∘ δ ∘ σ(A) = δx̄ ∘ δ ∘ σ(G′) ⊃ δ ∘ σ(G).

Finally, δx̄∘δ∘σ(G′) is evidently a closed positive instance of σ(G′),and is therefore provable from P. Using these facts in conjunction with Theorem 4.14 we may now conclude that δ ∘ σ(G) is provable from P. A unification step. We note first that D_{2} ≠ F. Hence, in either of these cases, it follows from Lemma 5.4 that if σ ∈ U(D_{2}) then σ ∈ U(θ_{2}(D_{1})). But then, it is easy to see that σ ∘ θ_{2} ∈ U(D_{1}). Since G_{2} = θ_{2}(G_{1}) it is evident that every closed instance of a goal formula in σ ∘ θ_{2}(G_{1}) is also a closed instance of a goal formula in σ(G_{2}). From this the second part of the lemma is obvious.

5.14. Theorem. (Soundness of P-derivations) Let ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩_{1≤i≤n} be a P-derivation of G, and let θ be its answer substitution. Then there is a positive substitution σ such that

(i) σ ∈ U(D_{n}), and (ii) all the closed positive instances of the goal formulas in σ(G_{n}) are provable from P. Further, if σ is a positive substitution satisfying (i) and (ii), then every closed positive instance of σ ∘ θ(G) is provable from P.

Proof. The second part of the theorem follows easily from Lemma 5.13 and a backward induction on i, the index of each tuple in the given P-derivation sequence. For the first part we exhibit a substitution — that is a simple modification of the one in Lemma 3.5 in [15] — and then show that it satisfies the requirements.

Let h_{α} ∈ Var_{α} be a chosen variable for each atomic type α. Then for each type α we identify a formula Ê_{α} in the following fashion:

(a) If α is o, then Ê_{α} = ⊤.

(b) If α is an atomic type other than o, then Ê_{α} = h_{α}.

(c) If α is the function type β_{1} → ⋯ → β_{k} → β where β is an atomic type, then Ê_{α} = λx_{1}…. λx_{k}.Ê_{β}, where, for 1 ≤ i ≤ k, x_{i} is a variable of type β_{i} that is distinct from h_{β_{i}}.

Now let γ = {⟨y, Ê_{α}⟩ | y ∈ Var_{α}}. Finally, letting V = F(G_{n})∪F(D_{n}), we define σ = γ ↑ V.

We note that any goal formula in G_{n} is of the form [P C_{1} … C_{n}] where P is a variable whose type is of the form α_{1} → ⋯ → α_{n} → o. From this it is apparent that if G ∈ G_{n} then any ground instance of σ(G) is identical to ⊤. Thus, it is clear that σ satisfies (ii). If D_{n} is empty then σ ∈ U(D_{n}). Otherwise, let ⟨F_{1}, F_{2}⟩ ∈ D_{n}. Since F_{1} and F_{2} are two flexible formulas, it may be seen that σ(F_{1}) and σ(F_{2}) are of the form λy_{1}^{1}…. λy_{m_{1}}^{1}.Ê_{β_{1}}, and λy_{1}^{2}…. λy_{m_{2}}^{2}.Ê_{β_{2}} respectively, where β_{i} is a primitive type and Ê_{β_{i}} ∉ {y_{1}^{i}, …, y_{m_{i}}^{i}} for i = 1, 2. Since F_{1} and F_{2} have the same types and substitution is a type preserving mapping, it is clear that β_{1} = β_{2}, m_{1} = m_{2} and, for 1 ≤ i ≤ m_{1}, y_{i}^{1} and y_{i}^{2} are variables of the same type. But then evidently σ(F_{1}) = σ(F_{2}).

In order to show a converse of the above theorem, we need the observation contained in the following lemma that may be verified by a routine inspection of Definition 5.9. 5.15. Lemma. Let ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ be P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ and let D ≠ F. Then V_{1} ⊆ V_{2} and if F(G_{1}) ∪ F(D_{1}) ⊆ V_{1}, then F(G_{2}) ∪ F(D_{2}) ⊆ V_{2}.

We also need a measure of complexity corresponding to a goal set and a unifier. In defining such a measure, we use those introduced in Definitions 4.15 and 5.6. 5.16. Definition.

(i) Let G be a set of closed goal formulas. Then ν_{P}(G) = ∑_{G∈G} μ_{P}(G).

(ii) Let G be a set of goal formulas and let σ be a positive substitution such that each

formula in σ(G) is closed. Then κ_{P}(G, σ) = ⟨ν_{P}(σ(G)), π(σ)⟩. (iii) ≺ is the lexicographic ordering on the collection of pairs of natural numbers, i.e.

⟨m_{1}, n_{1}⟩ ≺ ⟨m_{2}, n_{2}⟩ if either m_{1} < m_{2} or m_{1} = m_{2} and n_{1} < n_{2}.

If G is a finite set of closed goal formulas such that each member of G is provable from P, then it is easily seen that ν_{P}(G) < ω. We make implicit use of this fact in the proof of the following lemma. 5.17. Lemma. Let ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ be a tuple that is not a terminated P-derivation sequence and for which F(G_{1}) ∪ F(D_{1}) ⊆ V_{1}. Further, let there be a positive substitution σ_{1} ∈ U(D_{1}) such that, for each G_{1} ∈ G_{1}, σ_{1}(G_{1}) is a closed goal formula that is provable from P. Then there is a tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ and a positive substitution σ_{2} such that

(i) σ_{2} ∈ U(D_{2}), (ii) σ_{1} =_{V_{1}} σ_{2} ∘ θ_{2}, (iii) for each G_{2} ∈ G_{2}, σ_{2}(G_{2}) is a closed goal formula that is provable from P, and (iv) κ_{P}(G_{2}, σ_{2}) ≺ κ_{P}(G_{1}, σ_{1}). In addition, when there are several tuples that are P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩, such a tuple and such a substitution exist for every choice of (1) the kind of step, (2) the goal formula in a goal reduction or backchaining step, and (3) the flexible-rigid pair in a unification step. Proof. Since ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ is not a terminated P-derivation sequence, it is clear that there must be a tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ that is P-derivable from it. We consider below the various ways in which such a tuple may result to show that there must exist a tuple, and a corresponding substitution, satisfying the requirements of the lemma. From this argument it will also be evident that this is the case no matter how the choices mentioned in the lemma are exercised. Goal reduction step. If there is tuple that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ by such a step, then there must be a goal formula in G_{1} of the form ⊤, G_{1} ∨ G_{2}, G_{1} ∧ G_{2}, or Σ P. Let us consider the first three cases first. In these cases, we let

D_{2} = D_{1}, θ_{2} = ∅, V_{2} = V_{1}, and σ_{2} = σ_{1}.

Since σ_{1} ∈ U(D_{1}), it is obvious that σ_{2} ∈ U(D_{2}). Further, σ_{1} =_{V_{1}} σ_{2} ∘ θ_{2}; in fact, σ_{1} = σ_{2} ∘ θ_{2}. Now we consider each of the cases in turn to provide a value for G_{2} that, together with the assignments provided above, meets the requirements of the lemma.

(a) If ⊤ ∈ G_{1}, then let G_{2} = G_{1}−{⊤}. ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ is obviously a tuple that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩. The observations above show that this tuple and σ_{2} satisfy conditions (i) and (ii) in the lemma. That (iii) is true follows from the facts that G_{2} ⊆ G_{1} and σ_{2} = σ_{1}. Observing additionally that μ_{P}(⊤) > 0, (iv) follows.

(b) Let G_{1} ∨ G_{2} ∈ G_{1}. We note here that

σ_{1}(G_{1} ∨ G_{2}) = σ_{1}(G_{1}) ∨ σ_{1}(G_{2}) = σ_{2}(G_{1}) ∨ σ_{2}(G_{2}),

and, further, that σ_{2}(G_{1}) and σ_{2}(G_{2}) are closed goal formulas. Using Theorem 4.14 and the assumption that σ_{1}(G_{1} ∨G_{2}) is provable from P, we see that σ_{2}(G_{i}) is provable from P for i = 1 or i = 2. Further, by Lemma 4.16, it is the case that for the same i

μ_{P}(σ_{1}(G_{i})) < μ_{P}(σ_{1}(G_{1} ∨ G_{2})).

Setting

G_{2} = (G_{1} − {G_{1} ∨ G_{2}}) ∪ {G_{i}},

we obtain a tuple that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ and that together with σ_{2} satisfies the requirements in the lemma.

(c) If G_{1} ∧ G_{2} ∈ G_{1}, let G_{2} = (G_{1} − {G_{1} ∧ G_{2}}) ∪ {G_{1}, G_{2}}. By arguments similar to those in (b), it follows that ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩ and σ_{2} meet the requirements in the lemma. The only case remaining is when Σ P ∈ G_{1}. Here we choose a variable y such that

y ∉ V_{1}, and let

G_{2} = (G_{1} − {Σ P }) ∪ {λnorm(P y)}, D_{2} = D_{1}, θ_{2} = ∅, and V_{2} = V_{1} ∪ {y}.

Evidently ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ is a tuple that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩. Now if we let P′ = σ_{1}(P), we see that Σ P′ ∈ σ_{1}(G_{1}). Thus, by assumption, P′ is a closed positive formula and Σ P′ is provable from P. From Theorem 4.14 and Lemma 4.16 it follows that there is a closed positive formula C such that ρ(P′ C) is provable from P and, in fact, μ_{P}(ρ(P′ C)) < μ_{P}(Σ P′). Setting

σ_{2} = σ_{1} ∘ {⟨y, C⟩},

we see that ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ and σ_{2} meet the requirements in the lemma: Since y ∉ V_{1} and F(D_{1}) ⊆ V_{1}, σ_{2} ∈ U(D_{2}) and σ_{1} =_{V_{1}} σ_{2}. Since F(G_{1}) ⊆ V_{1}, (iii) is satisfied for each G ∈ G_{2} that is also in G_{1}. For the only other G ∈ G_{2}, i.e. λnorm(P y), it is apparent that σ_{2}(G) = ρ(P′ C) and so (iii) is satisfied in this case too. From these observations and the fact that μ_{P}(ρ(P′ C)) < μ_{P}(σ_{1}(Σ P)), (iv) also follows. Backchaining step. For this step to be applicable, there must be a rigid positive atom G ∈ G_{1}. Let G_{a} = σ_{1}(G). By assumption, G_{a} is a closed positive atom that is provable from P. Therefore, by Theorem 4.14, there must be a formula G′′ ⊃ G_{a} ∈ |P| such that G′′ is provable from P; in fact, by Lemma 4.16, μ_{P}(G′′) < μ_{P}(G_{a}). Since G′′ ⊃ G_{a} ∈ |P|, there must be a D ∈ P such that

D ≡ ∀x_{1}…. ∀x_{n}.G′ ⊃ A,

where x_{1}, …, x_{n} are not members of V_{1}, and a positive substitution φ for {x_{1}, …, x_{n}} such that G_{a} = φ(A) and G′′ = φ(G′). Now, setting

G_{2} = (G_{1} − {G}) ∪ {G′},  θ_{2} = ∅,

D_{2} = SIMPL(D_{1} ∪ ({⟨G, A⟩}),  V_{2} = V_{1} ∪ {x_{1}, …, x_{n}},

we obtain the tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩. Letting σ_{2} = σ_{1} ∘ φ, we see that this tuple and σ_{2} also meet the requirements in the lemma: Since x_{i} ∉ V_{1} for 1 ≤ i ≤ n,

σ_{1} =_{V_{1}} σ_{2} =_{V_{1}} σ_{2} ∘ θ_{2}.

Thus (ii) is satisfied. Also, since F(D_{1}) ⊆ V_{1}, σ_{2} ∈ U(D_{1}). Noting that φ(A) is a closed formula and that F(G) ⊆ V_{1},

σ_{2}(G) = σ_{1}(G) = φ(A) = σ_{2}(A).

From these observations and Lemma 5.4, it is clear that σ_{2} ∈ U(D_{2}), i.e. (i) is satisfied. Now, since F(G_{1}) ⊆ V_{1}, σ_{2}(G_{1}) = σ_{1}(G_{1}) for each G_{1} ∈ G_{2} that is also in G_{1}. Thus (iii) is true by assumption for such a G_{1}. For the only other formula in G_{2}, i.e. G′, this follows by observing that

σ_{2}(G′) = φ(G′) = G′′;

G′′ is by assumption provable from P. Finally, (iv) follows by observing that

μ_{P}(σ_{2}(G′)) = μ_{P}(G′′) < μ_{P}(G_{a}) = μ_{P}(σ_{1}(G)).

Unification step. For this case to be applicable, there must be a flexible-rigid pair in D_{1}. Let ⟨F_{1}, F_{2}⟩ be an arbitrary such pair. By Lemma 5.7, there is a (positive) substitution φ ∈ MATCH(F_{1}, F_{2}, V_{1}) and a (positive) substitution δ such that σ_{1} =_{V_{1}} δ ∘ φ and π(δ) < π(σ_{1}). Setting

G_{2} = φ(G_{1}), D_{2} = SIMPL(φ(D_{1})), θ_{2} = φ,

and choosing V_{2} appropriately, we see that there is a tuple ⟨G_{2}, D_{2}, θ_{2}, V_{2}⟩ that is P-derivable from ⟨G_{1}, D_{1}, θ_{1}, V_{1}⟩. Letting σ_{2} = δ we see easily that the other requirements of the lemma are also satisfied: Since F(D_{1}) ⊆ V_{1}, it is clear that

σ_{1}(D_{1}) = σ_{2} ∘ θ_{2}(D_{1}) = σ_{2}(θ_{2}(D_{1})).

Noting that σ_{1} ∈ U(D_{1}), (i) follows from Lemma 5.4. (ii) is evidently true. Since F(G_{1}) ⊆ V_{1}, we see that

σ_{1}(G_{1}) = σ_{2} ∘ θ_{2}(G_{1}) = σ_{2}(θ_{2}(G_{1})) = σ_{2}(G_{2}).

That every G_{2} ∈ σ_{2}(G_{2}) is a closed goal formula that is provable from P now follows trivially from the assumptions. Finally

κ_{P}(G_{2}, σ_{2}) ≺ κ_{P}(G_{1}, σ_{1})

since ν_{P}(σ_{2}(G_{2})) = ν_{P}(σ_{1}(G_{1})) and π(σ_{2}) < π(σ_{1}).

5.18. Theorem. (Completeness of P-derivations) Let φ be a closed positive substitution for the free variables of G such that φ(G) is provable from P. Then there is a P-derivation of G with an answer substitution θ such that φ ⪯_{F(G)} θ. Proof. From Lemmas 5.17 and 5.15 and the assumption of the theorem, it is evident that there is a P-derivation sequence ⟨G_{i}, D_{i}, θ_{i}, V_{i}⟩_{1≤i} for {G} and a sequence of substitutions σ_{i} such that

(i) σ_{1} = φ, (ii) σ_{i+1} satisfies the equation σ_{i} =_{V_{i}} σ_{i+1} ∘ θ_{i+1}, (iii) σ_{i} ∈ U(D_{i}), and (iv) κ_{P}(G_{i+1}, σ_{i+1}) ≺ κ_{P}(G_{i}, σ_{i}). From (iv) and the definition of ≺ it is clear that the sequence must terminate. From (iii) and Lemmas 5.4 and 5.7 it is evident, then, that it must be a successfully terminated sequence, i.e. a P-derivation of G. Using (i), (ii) and Lemma 5.15, an induction on the length n of the sequence then reveals that φ ⪯_{V_{1}} θ_{n}∘⋯∘θ_{1}. But F(G) = V_{1} and θ_{n}∘⋯∘θ_{1} is the answer substitution for the sequence.

P-derivations, thus, provide the basis for describing the proof procedure that we desired at the outset. Given a goal formula G, such a procedure starts with the tuple ⟨{G}, ∅, ∅, F(G)⟩ and constructs a P-derivation sequence. If the procedure performs an exhaustive search, and if there is a proof of G from P, it will always succeed in constructing a P-derivation of G from which a result may be extracted. A breadth-first search may be inappropriate if the procedure is intended as an interpreter for a programming language based on our definite sentences. By virtue of Lemma 5.17, we see that there are certain cases in which the procedure may limit its choices without adverse effects. The following choices are, however, critical:

(i) Choice of disjunct in a goal reduction step involving a disjunctive goal, (ii) Choice of definite sentence in a backchaining step, and (iii) Choice of substitution in a unification step. When it encounters such choices, the procedure may, with an accompanying loss of completeness, perform a depth-first search with backtracking. The particular manner in which to exercise these choices is very much an empirical question, a question to be settled only by experimentation.

6. Conclusion

In this paper we have concerned ourselves with the provision of higher-order features within logic programming. An approach that has been espoused elsewhere in this regard is to leave the basis of first-order logic programming languages unchanged and to provide some of the functionality of higher-order features through special mechanisms built into the interpreter. This approach is exemplified by the presence of “extra-logical” predicates such as univ and functor in most current implementations of Prolog [32]. While this approach has the advantage that usable “higher-order” extensions may be provided rapidly, it has the drawbacks that the logical basis of the resulting language is no longer clear and, further, that the true nature and utility of higher-order features within logic programming is obscured.

We have explored an alternative approach based on strengthening the underlying logic. In a precise sense, we have abstracted out those properties of first-order Horn clauses that appear to be essential to their computational interpretation, and have described a class of higher-order formulas that retain these properties. Towards realizing a higher-order logic programming language based on these formulas, we have also discussed the structure of a theorem-proving procedure for them. These results have been used elsewhere [21, 25] in the description of a language called λProlog. Although space does not permit a detailed discussion of this language, it needs to be mentioned that an experimental implementation for it exists, and has in fact been widely distributed. This implementation has, among other things, provided us with insights into the practical aspects of the trade-offs to be made in designing an actual theorem-proving procedure based on the discussions in Section 5 [25]. Its existence has also stimulated research into applications of the truly novel feature of the extension discussed in this paper: the use of λ-terms as data structures in a logic programming language.

This work has suggested several questions of both a theoretical and a practical nature, some of which are currently being examined. One theoretical question that has been addressed is that of providing for a stronger use of logical connectives within logic programming. Our approach in this regard has been to understand the desired “search” semantics for each logical connective and to then identify classes of formulas within appropriately chosen proofs systems that permit a match between the declarative and search-related meanings for the connectives. One extension along these lines to the classical theory of Horn clauses is provided by the intuitionistic theory of hereditary Harrop formulas. The first-order version of these formulas is presented in [18, 19] and the higher-order version is discussed in detail in [23]. These formulas result from allowing certain occurrences of universal quantifiers and implications into goals and program clauses and provide the means for realizing new notions of abstractions within logic programming. The higherorder version of hereditary Harrop formulas has been incorporated into the current version of λProlog [27] and has provided significant enrichments to it as a programming language.

A second theoretical issue is the provision of a richer term language within λProlog. The use of simply typed λ-terms has turned out to be a limiting factor in the programming context, and we have therefore incorporated a form of polymorphism inspired by ML [11, 24]. A complete theoretical analysis for this extension is, however, yet to be provided. Further, there is reason to believe that a term language that permits an explicit quantification over types, e.g. the one discussed in [8], may be a better choice in this context. In a similar vein, a richer term language like the one provided in [30], may also be considered as the basis for the data structures of λProlog.

Among the practical questions, an important one that is being addressed is the description of an efficient implementation for a λProlog-like language [26]. The key pursuit in this respect is to devise data structures for λ-terms that will support reasonable implementations of the reduction mechanism of functional programming on the one hand, and of the unification and backchaining mechanisms of logic programming on the other. Another issue of interest is the harnessing of the richness added to the logic programming paradigm by the use of λ-terms as data structures. As already indicated, ongoing research has been focused on exploiting such a language in areas that include theorem proving, type inference, program transformation, and computational linguisitics.

Acknowledgements. This paper is based on Nadathur’s doctoral dissertation. The authors gratefully acknowledge helpful comments provided on this work by Jean Gallier, Andre Scedrov and Richard Statman.

References

[1] Andrews, P. B. Resolution in type theory. Journal of Symbolic Logic 36 (1971) 414 – 432.

[2] Apt, K. R., and van Emden, M. H. Contributions to the theory of logic programming. J. ACM 29, 3 (1982) 841 – 862.

[3] Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, North Holland Publishing Co., 1981.

[4] Bowen, K. A. Programming with full first-order logic. Machine Intelligence 10, Hayes, J. E., Michie, D. and Pao, Y-H, eds., Halsted Press, 1982, 421 – 440.

[5] Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5 (1940) 56 – 68.

[6] Constable, R. L. et. al. Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986.

[7] Felty, A., and Miller, D. Specifying theorem provers in a higher-order logic programming language. Proceedings of the 9th International Conference on Automated Deduction, 1988, Springer-Verlag, 61 – 80.

[8] Fortune, S., Leivant, D., and O’Donnell, M. The expressiveness of simple and secondorder type structures. J. ACM 30, 1 (1983) 151 – 185.

[9] Gentzen, G. Investigations into logical deduction. The Collected Papers of Gerhard Gentzen, Szabo, M. E., ed., North-Holland Publishing Co., 1969, 68 – 131.

[10] Goldfarb, W. D. The undecidability of the second-order unification problem. Theoretical Computer Science 13 (1981) 225 – 230.

[11] Gordon, M., Milner, A., and Wadsworth, C. Edinburgh LCF: A Mechanized Logic of Computation, LNCS 78, Springer-Verlag, 1972.

[12] Gould, W. E. A matching procedure for ω-order logic. Scientific Report No. 4, A F C R L (1976) 66 – 781.

[13] Hannan, J. and Miller, D. Uses of higher-order unification for implementing program transformers. Proceedings of the Fifth International Conference and Symposium on Logic Programming, 1988, MIT Press, 942 – 959.

[14] Huet, G. P. The undecidability of unification in third order logic. Information and Control 22, 3 (1973) 257 – 267.

[15] Huet, G. P. A unification algorithm for typed λ-calculus. Theoretical Computer Science 1 (1975) 27 – 57.

[16] Huet, G. and Lang, B. Proving and Applying Program Transformations Expressed with Second-Order Logic. Acta Informatica 11 (1978) 31–55.

[17] Lucchesi, C. L. The undecidability of the unification problem for third order languages. Report C S R R 2059, Dept. of Applied Analysis and Computer Science, University of Waterloo, 1972.

[18] Miller, D. Hereditary Harrop formulas and logic programming. Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow, August 1987.

[19] Miller, D. A logical analysis of modules in logic programming. Journal of Logic Programming 6 (1989) 79 – 108.

[20] Miller, D., and Nadathur, G. Some uses of higher-order logic in computational linguistics. Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, 1986, 247 – 255.

[21] Miller, D. and Nadathur, G. Higher-order logic programming. Proceedings of the Third International Logic Programming Conference, London, 1986, LNCS 225, Springer Verlag, 448 – 462.

[22] Miller, D., and Nadathur, G. A logic programming approach to manipulating formulas and programs. IEEE Symposium on Logic Programming, 1987, 379 – 388.

[23] Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A. Uniform proofs as a foundation for logic programming. To appear in the Annals of Pure and Applied Logic.

[24] Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17 (1978) 348 – 375.

[25] Nadathur, G. A higher-order logic as the basis for logic programming. Ph.D. Dissertation, University of Pennsylvania, May 1987.

[26] Nadathur, G. and Jayaraman, B. Towards a WAM model for λProlog. To appear in the Proceedings of the North American Conference on Logic Programming, MIT Press, 1989.

[27] Nadathur, G. and Miller, D. An overview of λProlog. Proceedings of the Fifth International Conference on Logic Programming, 1988, MIT Press, 810 – 827.

[28] Paulson, L. C. Natural deduction as higher-order resolution. The Journal of Logic Programming 3, 3 (1986) 237 – 258.

[29] Pfenning, F. Partial polymorphic type inference and higher-order unification. Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, 1988, 153 – 163.

[30] Pfenning, F. and Elliot, C. Higher-order abstract syntax. Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, 1988, 199 – 208.

[31] Scherlis, W. and Scott, D. First steps towards inferential programming. Information Processing 83, North-Holland, Amsterdam, 1983.

[32] Sterling, L., and Shapiro, E. The Art of Prolog: Advanced Programming Techniques. MIT Press, Cambridge MA, 1986.

[33] van Emden, M. H., and Kowalski, R. A. The semantics of predicate logic as a programming language. J. ACM 23, 4 (1976) 733 – 742.

[34] Warren, D. H. D. Higher-order extensions to Prolog: Are they needed? Machine Intelligence 10, Hayes, J. E., Michie, D. and Pao, Y-H, eds., Halsted Press, 1982, 441 – 454.