HiLog: A Foundation for Higher-Order Logic Programming^{∗}

Weidong Chen^{†} Michael Kifer^{‡} David S. Warren Department of Computer Science State University of New York at Stony Brook Stony Brook, NY 11794

Abstract

We describe a novel logic, called HiLog, and show that it provides a more suitable basis for logic programming than does traditional predicate logic. HiLog has a higher-order syntax and allows arbitrary terms to appear in places where predicates, functions and atomic formulas occur in predicate calculus. But its semantics is first-order and admits a sound and complete proof procedure. Applications of HiLog are discussed, including DCG grammars, higher-order and modular logic programming, and deductive databases.

Keywords: logic programming, higher-order logic, contextual predicate calculus, first-order semantics, resolution theorem proving, database languages, object-oriented databases, modular programming, DCG grammars.

1 Preface

Manipulating predicates, functions, and even atomic formulas is a commonplace in logic programming. For example, Prolog combines predicate calculus, higher-order and meta-level programming in one working system, allowing programmers routine use of generic predicate definitions (e.g., transitive closure, sorting) where predicates can be passed as parameters and returned as values [7]. Another well-known useful feature is the “call” meta-predicate of Prolog. Applications of higher-order constructs in the database context have been pointed out in many works, including [23, 28, 40].

Although predicate calculus provides the basis for Prolog, it does not have the wherewithal to support any of these features, which consequently have an ad hoc status in logic programming. In this paper, we investigate the fundamental principles underlying higher-order logic programming and, in particular, shed new light on why and how these Prolog features appear to work in practice. We propose a novel logic, called HiLog, which provides a clean declarative semantics to much of this higher-order logic programming.

From the outset, even the terminology of “higher-orderness” seems ill-defined. A number of works have proposed various higher-order constructs in the logic framework [1, 5, 12, 7, 22, 23, 29, 30, 41, 44] but with such a diversity of syntax and semantics, it is not always clear what kind of higher-orderness is being claimed. In our opinion, there are at least two different facets to the issue: a higher-order syntax and a higher-order semantics. Logicians seem to have been long aware of this distinction and, for example, Enderton [15, page 282] describes a translation of the syntactically second-order predicate calculus into a first-order multi-sorted logic that admits a first-order semantics.

∗This paper is an expanded version of the work previously reported in [9, 10].

†Present address: Computer Science and Engineering, Southern Methodist University, Dallas, TX 75275.

‡Work of M. Kifer was partially supported by the NSF grant IRI-8903507.

Informally, by higher-order syntax, logicians mean a language in which variables are allowed to appear in places where normally predicate and/or function symbols do. In contrast, higher-order semantics is manifested by semantic structures in which variables may range over domains of relations and functions constructed out of the domains of individuals. In a first-order semantics, variables can only range over domains of individuals or over the names of predicates and functions.

The third component in this picture is the equality theory that is built into the semantics of the logic. As explained below, an equality theory may partially bridge the gap between first-order and higher-order semantics. In the extreme case, this theory may imply a 1-1 correspondence between the domain of individuals and the domains of higher-order constructs. In this case, higher-order and first-order semantics become virtually indistinguishable.

We note that the classification based upon semantics has no implication whatsoever regarding the “intrinsic higher-orderness,” that is, whether there exists a sound and complete proof theory for a higher-order semantics. It is quite possible to replace a higher-order semantics for some languages by an entailment-equivalent first-order semantics. On the other hand, it is well known that some semantics (e.g., the standard semantics of second-order predicate calculus) are inherently higher-order and no equivalent first-order substitute exists for the corresponding languages.

Predicate calculus is the primary example of a logic where syntax and semantics are both firstorder. There are logics that have a higher-order syntax but a first-order semantics. F-logic [23, 24] is one example; HiLog, to be discussed in this paper, also falls into this category. Examples of logics with higher-order syntax and semantics include COL [1] and Church’s simple theory of types [12, 22]. On the other hand, LDL [5, 45] is a language with a first-order syntax and a higher-order semantics.

Let us examine the equational theories underlying various logics more closely. Under a higher-order semantics, and equation between predicates (or function) symbols, e.g. p = q, is true if and only if these symbols are interpreted via the same relation (resp., function). Another way of saying this is that logics with a higher-order semantics have a built-in extensional equality theory of predicates and functions. In contrast, in HiLog and F-logic predicates and other higher-order syntactic objects are not equal unless they (i.e., their names) are equated explicitly. Thus, it is possible for two predicate symbols, say p and q, to be interpreted by the same relation and yet the equality p = q be false.

The above examples represent the two extreme cases, in a sense. There are higher-order languages with a first-order semantics that embody a non-trivial equality theory. An example is a subset of λProlog [41, 44] that has no type variables and whose syntax is essentially the same as Church’s simple theory of types [12]. Equality in λProlog corresponds to λ-equivalence and is not extensional: there may exist predicates that are not λ-equivalent but still extensionally equal.

To better see the role of equational theories on the classification of logical theories, note that there are two different aspects associated with an expression that denotes a predicate or a function. For instance, in λ-Prolog, one aspect is the meaning of the expression as a λ-term (or, more precisely, as an equivalence class of λ-terms), which we call the intension; the other aspect is the relation or a function associated with the expression, which we call the extension. These two aspects become indistinguishable if extensionality axioms are built into the logic. For instance, in Henkin’s semantics of Church’s type theory [22], it makes no difference whether predicate variables are considered to range over predicate names (intensions) or over relations (extensions), since each extension now becomes associated with exactly one intension, and vice versa.

The distinction between intensions and extensions is important. It is known that extensions can be notoriously difficult to handle in an efficient manner. Separating intensions from extensions makes it possible to have an equational theory over predicate and function names that is separate from the extensional equality of relations and functions. A logic that avoids an overly strong equational theory of intensions, can have a simple first-order semantics, a decidable unification problem and, at the same time, a higher-order syntax.

In a type-free logic, the same term may appear in different contexts as predicates or functions of different arities and even as atomic formulas. Thus the same intension can be associated with different extensions in different contexts. For instance, in the Lambda Calculus [39], a λ-term is considered a function or an object depending on its syntactic position. In HiLog, the same symbol may denote a predicate, a function, or an atomic formula. Semantics of a type-free logic has to maintain the distinctions between various extensions associated with the same intension. Since the same variable may appear in different contexts and have different extensions, it makes better sense for variables to range over intensions rather than extensions because only intensions remain the same across different contexts.

In this paper, we present a simple logical framework in which predicates, functions, and atomic formulas can be manipulated as first-class entities. It is quite clear that in order to support such manipulation naturally enough, the syntax has to be higher-order. As explained earlier, this leaves open two possibilities for the semantics. Under higher-order semantics, predicates and functions are identified by their extensions, that is, two predicates represent the same thing if and only if their extensions coincide in every appropriate semantic structure. Unfortunately, extensional equality of predicates and functions is not even semi-decidable, in general, which is likely to carry over to the unification problem.

In contrast, under first-order semantics, predicates and functions have intensions that can be manipulated directly. Furthermore, depending on the context, the same intension may assume different roles, acting as a relation, a function, or even a proposition. Unless the built-in equational theory is too strong, logical consequence relation under a first-order semantics is more tractable than under a higher-order semantics, and this observation motivates our choice for HiLog.^{1} The basic idea is to construct a logic that distinguishes between intensional and extensional aspects of the semantics and embodies only a trivial equality theory of intensions. Intensions can be thought of as names of abstract or concrete entities, while extensions correspond to various roles these entities play in the real world. It has also been argued by Maida and Shapiro [35, 36] that knowledge representation is part of the conceptual structure of cognitive agents, and therefore should not (and even cannot) contain extensions. The reason is that cognitive agents do not have direct access to the world, but only to one of its representations. Our approach is in the same spirit and, consequently, extensions of predicates and functions are not available for direct manipulation. On the other hand, intensions of higher-order entities such as predicates, functions, and even atomic formulas can be freely manipulated. Their extensions come into play only when the respective expressions need be evaluated. Thus, HiLog combines advantages of higher-order syntax with the simplicity of first-order semantics, benefiting from both.

The rest of the paper is organized as follows. After a brief motivational discussion, we formally present the syntax and semantics of HiLog. Then we give several examples of applying HiLog to higherorder logic programming, DCG grammars, and modular logic programming. After that, we discuss the relationship of HiLog to predicate calculus; its relationship to some of the recently proposed database languages is discussed in Section 5. A resolution-based proof theory of HiLog is described in Section 6.

1This rule of thumb has exceptions though. For instance, type theory under Henkin’s semantics has a proof theory despite the fact that Henkin’s semantics is higher-order. In contrast, for certain strains of first-order annotated logics [25, 26] complete proof procedures may not exist, in general.

2 Syntax and Semantics of HiLog

2.1 Motivation

Prolog syntax is quite flexible; it allows symbols to assume different roles depending upon their context (e.g., to have different arities, or to be viewed as a constant, a function, or a predicate). For instance, in the clause

r(X) ← p(X, f(a)), q(p(X, f(a)), f(p, b)).

the symbol f occurs both as a unary and as a binary function, and p appears as a binary predicate as well as a binary function symbol. Furthermore, the same syntactic object, p(X, f(a)), is an atomic formula in the first literal of the clause-body and an individual term in the second.

The support for multiple roles for non-logical parameters (constants, functions, and predicates) is a handy feature of Prolog but, unfortunately, this support is provided in a rather ad hoc way. For instance, while in the above example different occurrences of the same symbol can be semantically disambiguated simply by renaming the occurrences of f and p, this cannot be done in the following rule:

p(X, Y) ← q(Y), X.

Here, the individual variable X occurs as a first-order term and as an atomic formula, and renaming its different occurrences will, intuitively, yield a semantically different statement.

HiLog supports multiple roles for parameter symbols in a much more general and elegant manner. Parameters are arityless and the distinction between predicate, function, and constant symbols is eliminated. In particular, a HiLog term can be constructed from any logical symbol followed by any finite number of arguments. Different occurrences of the same parameter are related to the same object characterized by the same intension. Associated with such an intension are several different extensions that capture the different roles the symbol may assume in different contexts.

The same view is extended to arbitrary terms. HiLog allows complex terms (not just parameter symbols) to be viewed as functions, predicates and atomic formulas. For example, a generic transitive closure predicate can be defined as follows:

closure(R)(X, Y) ← R(X, Y).

closure(R)(X, Y) ← R(X, Z), closure(R)(Z, Y).

Here, closure is (syntactically) a second-order function which, given any relation R, returns its transitive closure closure(R). Generic definitions can be used in various ways. For instance,

parent(john, bill). parent(bill, bob). manager(john, mary). manager(mary, kathy). relation(parent). relation(manager). reports to(Person)(Superior) ← relation(Relname), closure(Relname)(Person,Superior).

will return { bill, mary, bob, kathy } in response to the query ?- reports to(john)(X), which is the set of john’s ancestors and bosses.

Often various applications of Prolog require term traversal. In HiLog, binary terms can be traversed as follows:

traverse(X(Y,Z)) ← traverse(Y), traverse(Z).

Notice that X is a variable that ranges over functors of the language, and therefore this program is independent of the alphabet of that language. In contrast, in Prolog one would have to either specify such a rule for every functor in the alphabet of the program, e.g.,

traverse(f(Y,Z)) ← traverse(Y), traverse(Z). traverse(g(Y,Z)) ← traverse(Y), traverse(Z). ... ... ...

or use a built-in predicate arg/3, as in

traverse(Tree) ← arg(1, Tree, Left), arg(2, Tree, Right), traverse(Left), traverse(Right).

In the latter, the structure of Tree is less visible and even is not enforced (unless we add another subgoal for checking the total number of arguments).

In databases, schema browsing is common [40]. In HiLog, browsing can be performed through the same query language as the one used for data retrieval. For instance,

relations(Y)(X) ← X(Y,Z). relations(Z)(X) ← X(Y,Z). ?- relations(john)(X).

will return the names of all binary predicates whose tuples mention the token john. HiLog shares this browsing capability with another recently proposed language, called F-logic [23, 24].

The ability to use sets is very important in logic programming. Prolog supports the use of sets by means of the setof construct, which has only an operational semantics. Although newer logic languages, such as LDL [5, 45] or COL [1], do provide semantics for sets, they have to severely restrict their use to avoid logical paradoxes and/or computational intractability. In HiLog, sets can be represented naturally by parameterized predicates mentioned earlier. For instance, the following HiLog rule defines groups of satisfied employees working for each manager. An employee is satisfied with the job if and only if he earns more than his boss:

sat empl(Boss)(Empl) ← supervises(Boss, Empl), salary(Boss,B sal), salary(Empl, E sal), E sal > B sal.

The set-term, sat empl(Boss) is akin to the setof and the grouping constructs of Prolog and LDL, respectively, although HiLog sets are not constructed or used the same way. Having defined sets intensionally, via terms, we can go on and use these sets in other relationships, as in the following fragment that associates packages of benefits with groups of satisfied employees:

package1(health ins). package1(life ins). package2(free car). package2(long vacations). benefits( package1, sat empl(john) ). benefits( package2, sat empl(bob) ).

The following is a query regarding benefit packages that bob enjoys as an employee in the above enterprise:

?- benefits(X,Y), Y(bob).

Note that the above information about sets can be also encoded in Prolog, but less naturally. A more detailed discussion of these issues appears in Sections 4, 5, and 8.

As seen from the earlier examples, HiLog terms are also atomic formulas. In this capacity, their semantics is indirectly captured by the truth value assigned to each ground term. For instance, instead of saying that a pair < a, b > is in the relation for a predicate p, we say that the term p(a, b) denotes a true proposition. Formal details are provided in the next two subsections.

2.2 Language

In addition to parentheses, connectives, and quantifiers, the alphabet of a language L of HiLog contains a countably infinite set V of variables and a countable set S of parameter symbols. We assume that V and S are disjoint.

The set T of HiLog terms of L is a minimal set of strings over the alphabet satisfying the following conditions:

• V ∪ S ⊆ T ;

• If t, t_{1},…, t_{n} are in T , then t(t_{1},…, t_{n}) ∈ T , where n ≥ 1.

Notice that according to this definition, a term can be applied to any finite number of terms and parameter symbols are arityless.

An atomic formula is a term. More complex formulas are built from atomic formulas in the usual way, by means of connectives ∨, ∧ (also written as &), ¬, and quantifiers ∃ and ∀.

In addition, we use ← and ⊂ to denote the implication, where (ϕ ← ψ) ≡ (ϕ ⊂ ψ) ≡ (ϕ ∨ ¬ψ). Likewise, ϕ → ψ and ϕ ⊃ ψ will stand for ¬ϕ ∨ ψ. The bi-directional implication, “ ↔ ”, also has the standard meaning.

A literal is either an atomic formula, a positive literal, or the negation ¬A of an atomic formula A, a negative literal. A clause is of the form ∀X_{1}...∀X_{k}(L_{1} ∨ ... ∨ L_{n}), where L_{1}, ..., L_{n} are literals and X_{1}, ..., X_{k} are all the variables occurring in L_{1}, ..., L_{n}. It is usually written simply as L_{1} ∨ ... ∨ L_{n}. When n = 0, a clause is called the empty clause. A Horn clause is a clause that contains at most one positive literal. A definite clause is a Horn clause of the form A ∨ ¬B_{1} ∨ ... ∨ ¬B_{n}, where A, B_{1}, ..., B_{n} are atomic formulas; definite clauses are usually written as A ← B_{1}, ..., B_{n}, where A is the head and the conjunction B_{1}, ..., B_{n} is the body of the clause.^{2} A negative clause is a clause containing no positive literals. A goal is a conjunction of literals, and a query is the negation of a goal, which can be written as a negative clause. For practical applications, we consider definite logic programs that consist of a finite number of definite clauses. Section 4.1 briefly deals with logic programs with negation.

2.3 Semantic Structures

Since—at the first glance—the semantics of HiLog may seem a bit unusual, we precede the formal description by an informal discussion that shows how the semantics of the first-order predicate calculus has evolved to support higher-orderness of HiLog. First, we define the Herbrand semantics because it is especially close to the Herbrand semantics of predicate calculus.

2As usual in logic programming literature, we use “,” to denote conjunction of literals in the clause body.

The Herbrand universe for a HiLog language, L, is the set of all ground (i.e., variable-free) HiLog terms in T . Since, terms in HiLog are also atomic formulas, it follows that the Herbrand universe and the Herbrand base (cf. [34]) coincide. This is not a coincidence: if we want to manipulate atomic formulas as terms, the former must be elements of the universe. Now, a Herbrand interpretation is simply a subset of the Herbrand base (≡ universe), the definition of Herbrand interpretation commonly used in logic programming [34]. The definition of formula satisfaction in such interpretations simply repeats the corresponding definition in [34].

Although Herbrand interpretations suffice for many of the needs of logic programming, there are at least two important reasons to be interested in a more general notion of semantic structure [15]: programs with equality and the semantics of negation by failure.

Recall that, in first-order predicate calculus, a semantic structure M for a language L is a pair < U, I >, where U is called the domain of M and I is a function that interprets parameters of L (i.e., constants, function symbols, and predicate symbols). I consists of two different mappings, F and P. The former, F, interprets each k-ary (k ≥ 0) function symbol of L by a function U^{k} ⟼ U; the mapping P maps each n-ary predicate symbol to an n-ary relation over U. We consider constants as 0-ary function symbols, so F takes care of constants as well. In what follows, whenever f is a function symbol, I(f) will stand for F(f); when p is a predicate name, I(p) will stand for P(p). Note that the set of function symbols and the set of predicate symbols are disjoint.

In HiLog, one of our original goals was to eliminate the syntactic distinction among constants, function symbols, and predicates, so one cannot tell a constant from a predicate or a function symbol. Therefore, F and P must map each parameter symbol to all of the following: an element of U, a function over U, and a relation on U. Another of our goals was to make symbols arityless. So, each symbol must be mapped into an infinite tuple of functions and relations, one for each arity.

There is a subtlety, however. How should we interpret a formula like X(a), where X is a variable? In predicate calculus, such formulas are interpreted with respect to a variable assignment, which is a mapping ν : V ⟼ U. However, ν(X) is an element of the semantic domain U, and in order to interpret X(a) with respect to ν we must associate relations with elements of U rather then parameters of L. Thus, the interpreting mappings F and P must associate functions and relations with every element in U, including I(s) for each s ∈ S, not with the symbols in S.

Following the usual development in predicate calculus, we can extend a variable assignment ν recursively to the set T of all terms as follows:

• ν(s) = I(s) for every parameter symbol in S;

• ν(t(t_{1}, ..., t_{n})) = F(ν(t))(ν(t_{1}), ..., ν(t_{n})).

However, the truth of an atomic formula t(t_{1}, ..., t_{n}) can be determined either with respect to the n-ary relation that P associates with ν(t), that is, P(ν(t))(ν(t_{1}), ..., ν(t_{n})), or with respect to the 0-ary relation (i.e., true or false) which it associates with ν(t(t_{1}, ..., t_{n})), that is, P(ν(t(t_{1}, ..., t_{n}))). Both alternatives seem reasonable, but the second one results in a more uniform treatment of HiLog terms. Furthermore, it turns out that under certain natural assumptions, these two choices lead to the same semantics.

It is easy to see now that adopting the second alternative obviates the need for P. Indeed, all we need is to classify elements of the domain U into the intensions of true and false propositions. A simple way to do this is by introducing a subset U_{true} ⊆ U that designates propositions that are true in M.

Coming back to Herbrand interpretations discussed at the beginning of this section, we see that—in the Herbrand case—U_{true} is precisely that subset of the Herbrand base that determines the interpretation.

After this informal introduction, we are ready for the formal development. A semantic structure for HiLog, M, is a quadruple < U, U_{true}, I, F >, where

• U is a nonempty set of intensions for the domain of M;

• U_{true} is a subset of U that specifies which of the elements in U are intensions of true propositions;

• I : S ⟼ U is a function that associates an intension with each logical symbol;

• F : U ⟼ ∏_{k=1}^{∞}[U^{k} ⟼ U] is a function, such that for every u ∈ U and k ≥ 1, the k-th projection

of F(u), also denoted by u_{F}^{(k)}, is a function in [U^{k} ⟼ U]. Here ∏ denotes the Cartesian product of sets and [U^{k} ⟼ U] is the set of all functions that map U^{k} to U.

Given a semantic structure M, and a variable assignment ν : V ⟼ U, we extend it recursively to the set T of terms as follows:

• ν(s) = I(s) for every s ∈ S;

• ν(t(t_{1},…, t_{n})) = (ν(t))_{F}^{(n)}(ν(t_{1}),…, ν(t_{n})).

Let ϕ be an atomic formula. It is satisfied by M under ν, denoted M ⊧_{ν} ϕ, if and only if ν(ϕ) ∈ U_{true}.

We thus see that a HiLog term may represent an individual, a function, a predicate, or an atomic formula in different contexts. The intension of a term is its associated element in the universe U. Extensional aspects of terms are captured as follows. The extensional aspect of a term viewed as a proposition is its truth value defined by its membership in U_{true}, while the extensional meaning of a term in its capacity as a function is captured by F. For example, if a term t appears as a k-ary function, e.g., in t(t_{1},…, t_{k}), its extensional meaning under a variable assignment ν is the k-th projection of the vector of functions associated with the intension of t, that is, (ν(t))_{F}^{(k)}. On the other hand, the role of the above term as a proposition is indirectly captured through F and U_{true} so that t(t_{1},…, t_{k}) is true if and only if ν(t(t_{1}, ..., t_{k})) ∈ U_{true}.

Finally, the meaning of complex formulas is defined in the standard way:

• M ⊧_{ν} (ϕ ∧ ψ) if and only if M ⊧_{ν} ϕ and M ⊧_{ν} ψ;

• M ⊧_{ν} (ϕ ∨ ψ) if and only if M ⊧_{ν} ϕ or M ⊧_{ν} ψ;

• M ⊧_{ν} (¬ϕ) if and only if M |̸=_{ν} ϕ;

• M ⊧_{ν} (∀X)ϕ if and only if for every variable assignment, μ, that may differ from ν only on X, M ⊧_{μ} ϕ;

• M ⊧_{ν} (∃X)ϕ if and only if for some variable assignment, μ, that may differ from ν only on X, M ⊧_{μ} ϕ;

For closed formulas (i.e., formulas all of whose variables are quantified), M ⊧_{ν} ϕ does not depend on ν and we can write simply M ⊧ ϕ.

Interpreted symbols, such as “=”, “true”, and “false”, can be incorporated into HiLog by requiring interpretations to satisfy the following restrictions:

• I(true) ∈ U_{true};

• I(false) ∉ U_{true};

• I(=)_{F}^{(k)}(u_{1},…, u_{k}) ∈ U_{true} if and only if u_{1} = u_{2} = ⋯ = u_{k} (i.e., if all the u_{i}’s denote the same element of U).

It should be noted that, at least in the case of “true” and “false”, functional extensions of arities greater than 1 could be defined differently. Although our definition of true and false seems natural, we do not impose it in any essential way, and our theory does not depend on the above specific choice.

Compared with other higher-order logics, such as Church’s theory of types [12] and λProlog [41, 44], HiLog treats only atomic formulas as first-class objects. Formulas that contain connectives, such as “and”, “or”, or “not”, could be built into HiLog by interpreting these connectives as follows:

• I(and)_{F}^{(2)}(d_{1}, d_{2}) ∈ U_{true} if and only if both d_{1} and d_{2} are in U_{true}, for every d_{1}, d_{2} ∈ U;

• I(or)_{F}^{(2)}(d_{1}, d_{2}) ∈ U_{true} if and only if d_{1} or d_{2} are in U_{true}, for every d_{1}, d_{2} ∈ U;

• I(not)_{F}^{(1)}(d) ∈ U_{true} if and only if d is not in U_{true}, for every d ∈ U.

Alternatively, the above connectives can be defined using HiLog clauses, e.g., and(X,Y) :- X,Y. Encoding formulas with quantified variables would require introduction of λ-abstraction into HiLog, which can be also done, but is beyond the scope of this paper.

3 Relationship to Prolog and Predicate Calculus

In this section, we show from various perspectives that HiLog is, in a well-defined sense, a faithful extension of predicate calculus. In the sequel, we will use “PC” as an abbreviation for “predicate calculus.” First, we compare HiLog to what we call contextual predicate calculus. This is an extension of ordinary, “pure” predicate calculus and is inspired by the way Prolog permits the use of the same symbol in different contexts (e.g., as a predicate symbol or as a function symbol of different arities). Syntactically, formulas in contextual PC are also well-formed in HiLog and therefore there is a question of whether the validity problems for such formulas under the semantics of HiLog and contextual PC coincide. We show that this is not always the case, but under certain conditions the two validity problems do coincide. In the second subsection, we consider formulas in pure predicate calculus. Such formulas are also well-formed in contextual PC and therefore also in HiLog. We then establish that the validity problem in pure PC coincides with the same problem in HiLog for an even larger class of formulas than in the case of contextual PC. The third subsection shows that every HiLog formula can be encoded as a formula in pure PC.

3.1 Validity in Contextual Predicate Calculus and HiLog

In Prolog, the same symbol may appear in different contexts as a predicate, a constant, or a function symbol; the same symbol can even occur with different arities in different parts of the program. The exact role played by an occurrence of a symbol depends on the context in which this symbol occurs. Such Prolog programs are normally understood as formulas in predicate calculus in which different occurrences of the same symbol are replaced by different function or predicate symbols (whichever is appropriate) of suitable arities. This ad hoc use of parameter symbols in multiple roles motivates a simple extension of PC, which we call contextual predicate calculus.

A language L of contextual PC contains a set of parameter symbols, S, and a set of variables, V. A term is either a variable, a parameter symbol, or an expression of the form s(t_{1}, ..., t_{n}), where s ∈ S, n > 0, and t_{1}, ... , t_{n} are terms. An atomic formula is any term other than a variable, and the rest of the definitions are as usual.

Clearly, contextual PC is an extension of PC in the direction of HiLog, but is not as radical. It stops short of introducing a higher-order syntax (because s above is an element of S, not a variable). Every formula in contextual PC is also a formula in HiLog. On the other hand, X and X(a)(b) are well-formed formulas in HiLog but not in contextual PC. Similarly, every PC formula is also a formula in contextual PC, but not vice versa, e.g., s(s, s) is a formula in contextual PC but not in PC.

Semantics of contextual PC is also a middle ground between HiLog and pure PC. A semantic structure for a contextual PC language is a tuple M =< U, I_{F}, I_{P} >. For each symbol s ∈ S, the function I_{F} associates an infinite tuple < f_{0}, f_{1}, f_{2}, ⋯ >, where f_{0} is an element of U and for i > 0, f_{i} is a function U^{i} ⟼ U. Likewise, I_{P}(s) is a tuple < p_{0}, p_{1}, p_{2}, ⋯ >, where p_{0} is a 0-ary relation, p_{1} is a unary relation, etc. We will denote the k-th components of the above infinite tuples by I_{F}^{(k)}(s) and I_{P}^{(k)}(s), respectively. (Recall that a 0-ary relation is a set of 0-ary tuples and that there is only one such tuple—the empty tuple <>. Therefore, there are only two 0-ary relations: the empty one and the relation {<>}. The former is used to interpret false propositions while the latter interprets true propositions.)

Given a variable assignment ν : V ⟼ U, we define ν(s) = s, whenever s ∈ S, and ν(s(t_{1}, ..., t_{n})) = I_{F}^{(n)}(s)(ν(t_{1}), ..., ν(t_{n})). If s(t_{1}, ..., t_{n}) is an atomic formula, M ⊧_{ν} s(t_{1}, ..., t_{n}) if and only if < ν(t_{1}),..., ν(t_{n}) >∈ I_{P}^{(n)}(s). The rest of the definition of ⊧ is the same as for PC and HiLog.

Although there are contextual PC formulas that are not well-formed in PC, any such formula, ϕ, can be transformed into a formula ϕ′ in PC by replacing occurrences of each parameter symbol as follows. All occurrences of s as a k-ary function are replaced by a new k-ary function symbol s_{F}^{k}; all occurrences of s in the position of a k-ary predicate are replaced by a new predicate symbol s_{P}^{k}. For instance, under this transformation s(s, t(t)) becomes s_{P}^{2}(s_{F}^{0}, t_{F}^{1}(t_{F}^{0})). This transformation is explicit in Prolog where parameter symbols can assume multiple roles. A justification for using this transformation stems from the following easy fact:

Lemma 3.1

1. A formula in contextual PC is valid if and only if its transformation into pure PC is valid.

2. A formula in PC is valid if and only if it is also valid when considered under the semantics of contextual PC.

Proof: Let L be a language of contextual PC and L′ be the corresponding language of pure PC in which the transformed formulas are expressed. That is, if S is a set of parameters of L then the set of function symbols of L′ is {s_{F}^{k}|k ≥ 0, s ∈ L}, where the superscript indicates the arity; {s_{P}^{k}|k ≥ 0, s ∈ L} is the set of predicate symbols of L′.

The proof of (1) is then carried out by constructing an isomorphism M between the sets of semantic structures for L and L′ such that if M =< U, I_{F}, I_{P} > is a semantic structure for L, ϕ is a formula in L and ϕ′ is its translation to L′ then M ⊧ ϕ if and only if M(M) ⊧ ϕ′. M(M) =< U, I > is constructed in an obvious way: I(s_{P}^{k}) = I_{P}^{(k)}(s) and I(s_{F}^{k}) = I_{F}^{(k)}(s).

To prove (2), consider L′, a language of PC. Let L′′ be a language of contextual PC with the same sets of parameters and variables. Let M′ =< U, I > be a semantic structure of L′. The corresponding semantic structure M′′ =< U, I_{F}, I_{P} > is constructed thus: If p is a k-ary predicate symbol in L′ then I_{P}^{(k)}(p) = I(p); if f is a k-ary function symbol in L′ then I_{F}^{(k)}(f) = I(f). The rest of I_{P} and I_{F} can be arbitrary. It is easy to see that a PC formula ϕ in L′ is true in M′ if and only if it is true in M′′. Thus, if such a formula is valid when considered as a formula in L′′ then it is valid as a formula in L′.

By reversing the above construction, for every semantic structure M′′ of the language L′′ of contextual PC, one can construct a PC structure M′ for L′ such that a PC formula ϕ in L′ is true in M′′ if and only if it is true in M′. Thus, if ϕ is valid as a PC formula in L′, it is valid as a formula in the contextual PC language L′′. □

The above lemma essentially says that contextual PC is only a minor extension of PC. However, because of the greater similarity between the syntax of contextual PC and HiLog, it is instructive to investigate the relationship between the validity problems in these two logics. Suppose S and V is a set of parameters and variables, respectively. Let L_{H} be a language of HiLog and L_{P} be the sublanguage of contextual PC. In view of Lemma 3.1, it is tempting to think that every formula in L_{P} is valid under the semantics of contextual PC if and only if it is valid under the semantics of HiLog. It turns out that the difference between these semantics is more fundamental than in the case of the two flavors of PC. Consider the following formula that is valid in HiLog:

(s(a) = r(b, c)) ⊃ (s(a) ↔ r(b, c))  (1)

It is easy to see that this formula is not valid in contextual PC, for the latter can assign relations to the parameters s and r that are not related in any way to the meaning assigned to the terms s(a) and r(b,c). This stands in sharp contrast with HiLog where truth value is assigned to intensions of atoms and according to the premise of (1) the terms s(a) and r(b, c) do have the same intension; hence, as atomic formulas, they also must have the same truth value.

Nevertheless, there is a correspondence between valid formulas of L_{P} in HiLog and contextual PC in the important cases described in Theorem 3.1 below.

Definition 3.1 Given a language L of contextual PC, a semantic structure M =< U, I_{F}, I_{P} > is free if and only if for every pair of parameter symbols f and g and any pair of arities n ≥ 0 and m ≥ 0, the following holds:

• for all x_{1},…, x_{n} and y_{1},…, y_{m} in U, I_{F}^{(n)}(f)(x_{1},…, x_{n}) = I_{F}^{(m)}(g)(y_{1},…, y_{m}) if and only if f and g are identical symbols, n = m, and x_{i}, y_{i} are identical elements in U, for all i (1 ≤ i ≤ n).

Definition 3.2 A sentence ϕ in contextual PC is freely-interpretable if it has the following property:

• if ϕ is satisfied by every free semantic structure then it is satisfied by all semantic structures.

Theorem 3.1 Let, as before, L_{H} be a language of HiLog and L_{P} be the sublanguage of contextual PC (i.e., they share the same set S of parameters and the set V of variables). Let ϕ be a formula in L_{P}. Then

1. If ⊧^{cpc} ϕ then ⊧^{hilog} ϕ.

2. If ϕ is freely-interpretable then ⊧^{hilog} ϕ if and only if ⊧^{cpc} ϕ.

Here, ⊧^{cpc} and ⊧^{hilog} denote logical implication with respect to the semantics of contextual PC and HiLog, respectively.

Proof: The proof of (1) is similar but simpler than the proof of (2); it is left to the reader. To prove (2), suppose that ⊧^{hilog} ϕ_{H} holds. We show that ⊧^{cpc} ϕ holds as well. Given a free semantic structure M_{P} =< U, I_{F}, I_{P} > for L_{P}, we construct a semantic structure M_{H} =< U, U_{true}, I, F > of L_{H} as follows:

• The domain U is the same as in M_{P};

• I(s) = I_{F}^{(0)}(s) for every symbol s of S;

• for every u ∈ U and every k ≥ 1, if u = I_{F}^{(0)}(s) for some s ∈ S, then u_{F}^{(k)} = I_{F}^{(k)}(s); otherwise define u_{F}^{(k)}(u_{1}, ⋯, u_{k}) = d for some fixed d ∈ U;

• u ∈ U_{true} if and only if one of the following conditions holds:

– u = I_{F}^{(0)}(s) for some s ∈ S such that I_{P}^{(0)}(s) is a nonempty 0-ary relation^{3} (equivalently, if M_{P} ⊧ s); or

– u = I_{F}^{(k)}(s)(u_{1}, ⋯, u_{k}) for some s ∈ S and u_{i} ∈ U (1 ≤ i ≤ k), such that < u_{1}, ⋯, u_{k} >∈ I_{P}^{(k)}(s).

The semantic structure M_{H} is well-defined since M_{P} is free. It can be shown by induction that for any formula ϕ of L_{P} and any variable assignment ν, M_{P} ⊧_{ν} ϕ if and only if M_{H} ⊧_{ν} ϕ. Therefore, if ⊧^{hilog} ϕ, then ϕ is satisfied in every free semantic structure for L_{P}. Since ϕ is freely-interpretable, it is satisfied in every semantic structure for L_{P}, that is, ⊧^{cpc} ϕ holds.

To prove the other direction of (2), let us assume that ⊧^{cpc} ϕ holds. We need to show that ⊧^{hilog} ϕ holds as well. Given a semantic structure M_{H} =< U, U_{true}, I_{H}, F > for L_{H}, we construct a semantic structure M_{P} =< U, I_{F}, I_{P} > for L_{P} as follows:

• The domain U is the same as in M_{H};

• for every symbol s of L_{H},

– I_{F}^{(0)}(s) = I_{H}(s);

– I_{F}^{(k)}(s) = (I_{H}(s))_{F}^{(k)}, for every k ≥ 1;

– I_{P}^{(0)}(s) is a non-empty 0-ary relation (equivalently, M_{P} ⊧ s) if and only if I_{H}(s) ∈ U_{true};

– < u_{1}, ⋯, u_{k} >∈ I_{P}^{(k)}(s), k ≥ 1, if and only if (I_{H}(s))_{F}^{(k)}(u_{1}, ⋯, u_{k}) ∈ U_{true}.

Again it can be shown by induction that for any formula ϕ of L_{P} and any variable assignment ν, M_{P} ⊧_{ν} ϕ if and only if M_{H} ⊧_{ν} ϕ. Therefore if there exists some M_{H} such that M_{H} |̸=_{ν} ϕ, a semantic structure M_{P} of L_{P} can be constructed such that M_{P} |̸= ϕ, contrary to the assumption. Thus ⊧^{hilog} ϕ holds. □

Although the condition in Theorem 3.1 is not syntactic, it encompasses important classes of formulas. The following lemma shows that all equality-free formulas of predicate calculus are freely-interpretable. The other interesting class that is particularly important for logic programming consists of sets of definite clauses with equality, but such that the equality is restricted to clause bodies. If G is a query and is a negative clause and P is a definite logic program (possibly with equality in clause bodies) then evaluating the query amounts to showing that the set S = G ∪ P is unsatisfiable. Since Theorem 3.1 concerns validity (which is a contrapositive of unsatisfiability), the class of formulas to consider in this theorem is {¬S | S is a conjunction of Horn clauses free of equality in the head}.

3Recall that the nonempty 0-ary relation interprets true propositions, while the empty relation interprets false propositions.

Lemma 3.2 The following classes of contextual PC formulas are freely-interpretable:

1. Sets of equality-free sentences.

2. Formulas of the form ¬S, where S is a conjunction of Horn clauses free of “=” in clause-heads.

Proof: Consider a language L of contextual PC with a set of parameters S. Let ϕ be a formula in L that has one of the forms (1) or (2) above. Assume that for some semantic structure M =< U, I_{F}, I_{P} > for L, M |̸= ϕ. We show that there exists a free semantic structure M′ =< U′, I′_{F}, I′_{P} > such that M′ |̸= ϕ.

The domain U′ of M′ is a free algebra built out of the elements of U and parameter symbols of L. In other words, it is a minimal set satisfying the following conditions:

• U ∪ S ⊆ U′;

• if d_{1}, ⋯, d_{k} are in U′ and s ∈ S then the abstract symbol s(d_{1}, ⋯, d_{k}) is in U′ for every k ≥ 0.

For every s ∈ S define I_{F}^{′(0)}(s) = s and for each k ≥ 1 define I_{F}^{′(0)}(s)(d_{1}, ⋯, d_{k}) = s(d_{1}, ⋯, d_{k}) for all d_{1}, ⋯, d_{k} in U′.

There is a natural mapping ∗ : U′ ⟼ U defined thus: For every element u in U′, the corresponding element u^{∗} in U is such that:

• u^{∗} = u, if u ∈ U;

• s^{∗} = I_{F}^{(0)}(s), if s ∈ S; and

• (s(u_{1}, ⋯, u_{k}))^{∗} = I_{F}^{(k)}(s)(u_{1}^{∗}, ⋯, u_{k}^{∗});

Next, define I_{P}^{′(k)}(s) as follows: < u_{1}, ⋯, u_{k} >∈ I_{P}^{′(k)}(s) if and only if < u_{1}^{∗}, ⋯, u_{k}^{∗} >∈ I_{P}^{(k)}(p).

By the definition, M′ is a free semantic structure, and the mapping ∗ : U′ ⟼ U is a homomorphism of M′ onto M [15]. By the Homomorphism Theorem [15], the following properties hold:

(i) If ν : V ⟼ U′ is a variable assignment with respect to M′ then there is a variable assignment ν^{∗} : V ⟼ U with respect to M, defined as follows: for each variable X of L, ν^{∗}(X) = (ν(X))^{∗};

(ii) For any term t of L, ν^{∗}(t) = (ν(t))^{∗}, where ν^{∗}(t) is evaluated with respect to M while ν(t) is evaluated with respect to M′;

(iii) The mapping ν ⟼ ν^{∗} is an epimorphism of variable assignments, i.e., for every variable assignment μ for M there is an assignment ν for M′ such that ν^{∗} = μ;

(iv) For every equality-free formula ϕ, M′ ⊧_{ν} ϕ if and only if M ⊧_{ν^{∗}} ϕ.

Obviously, (1) follows from (iii) and (iv).

To show (2), let S be a conjunction of Horn clauses free of equality in clause heads. To show that ¬S is freely interpretable, we prove that M |̸=_{ν^{∗}} ¬S implies M′ |̸=_{ν} ¬S. The latter is the same as saying that M ⊧_{ν^{∗}} S implies M′ ⊧_{ν} S, and since S is a conjunction of clauses, we only need to establish this fact for the case of a single clause, r, that is, to show that M ⊧_{ν^{∗}} r implies M′ ⊧_{ν} r.

Let r be a clause of the form L_{1} ∨ ... ∨ L_{n}. Assume that M ⊧_{ν^{∗}} r. Then there exists some literal L_{i} such that M ⊧_{ν^{∗}} L_{i}. If L_{i} is not an equality literal, then M′ ⊧_{ν} L_{i} by (iii), and thus M′ ⊧_{ν} r. If L_{i} is an equality literal, then L_{i} must be of the form ¬(t_{1} = t_{2}), by the assumption. It follows from the definition of the mapping “∗” that if ν(t_{1}) = ν(t_{2}) then also ν^{∗}(t_{1}) = ν^{∗}(t_{2}) (but the opposite may not be true). Hence M ⊧_{ν^{∗}} L_{i} implies M′ ⊧_{ν} L_{i} and also M′ ⊧_{ν} r. □

It is interesting to note that although formulas of the form ¬S in the above lemma are freelyinterpretable, S itself may not be freely interpretable. A simple example is the formula c ← a=b that is true in every free interpretation, but is not a valid formula in general.

3.2 Validity in Pure Predicate Calculus and HiLog

Since formulas in pure PC are also formulas in contextual PC, the results of the previous subsection hold for PC formulas as well. However, since the language of PC is a subset of the language of contextual PC, we will be able to establish a result stronger than Theorem 3.1.

Definition 3.3 Let P be a set of formulas in a PC or a contextual PC language L. Let γ denote the cardinality of the set of parameters of L. We say that P is cardinal with respect to L if the following property holds:

• If P is true in every semantic structure M such that the cardinality of the domain of M is at least γ, then P is true in every semantic structure of L.

Lemma 3.3 Every freely-interpretable formula in contextual PC is cardinal. In particular, the formulas of the form described in Lemma 3.2 are cardinal.

Proof: For simplicity, we will prove the lemma for languages with finite sets of parameters. It suffices to show that every free semantic structure for a language L of contextual PC has an infinite domain. Then if ϕ is freely-interpretable, suppose that it is true in every semantic structure of cardinality at least γ. Then it holds in every infinite and, in particular, every free semantic structure. Hence, since ϕ is freely interpretable, it holds in every semantic structure.

Let M =< U, I_{F}, P > be a semantic structure for L and let s be a parameter symbol in L. Let u_{0} = I_{F}^{(0)}(s), u_{1} = I_{F}^{(1)}(s)(u_{0}), u_{2} = I_{F}^{(1)}(s)(u_{1}), and so on. Then, by the definition of free structures, u_{0}, u_{1}, u_{2}, and so on, are all distinct elements of U. □

Theorem 3.2 Let ϕ be a set of formulas in PC (and hence in HiLog). Then

• If ϕ is valid in PC then it is valid in HiLog.

• If ϕ is cardinal and is valid in HiLog then it is also valid in PC.

Before presenting the proof, we show that the second part of the theorem does not hold, in general. Consider the following formula:

(q(a) ↔ r(a)) ← ∀X∀Y(X = Y).

Clearly, this is a well-formed formula both in predicate calculus and in HiLog. It is also a valid HiLog formula because whenever the right side of the formula is true in a semantic structure M = < U, U_{true}, I, F >, the domain of this structure must be a singleton element. So, in M, q and r are mapped to the same element of U. Therefore, I(q(a)) = I(r(a)) and the left hand of the formula holds true. However, this formula is not valid in predicate calculus, since it is falsified by every semantic structure that has a one-element domain and interprets q by an empty relation while r by a nonempty one. One reason for this discrepancy between HiLog and predicate calculus is that the domains of quantification are different: in HiLog this domain contains r and q while in predicate calculus it does not. Therefore, predicate calculus has, in a sense, more interpretations than HiLog. Another reason is that truth of atomic formulas is defined via intensions of these formulas in the domain of interpretation rather than via relations associated with predicate symbols.

The second part of Theorem 3.2 hinges in an essential way on the assumption that ϕ is a well-formed formula in predicate calculus. It is not true, for example, for formulas in contextual predicate calculus. Consider

(s(a) ↔ r(b)) ← (s(a) = r(b)).  (2)

This formula is not well-formed in PC (s and r play multiple roles here) but is well-formed in contextual PC. It is also a cardinal formula. It is easy to see that (2) is valid in HiLog but not in contextual PC (the latter is because semantic structures in contextual PC can assign different truth values to the atoms s(a) and r(b), even if the terms s(a) and r(b) have the same intension). Another observation is that (2) is cardinal but not freely-interpretable (it holds in every free structure because the premise is always false; however, as noted above, this formula is not valid in contextual PC). This means that Theorem 3.2 strengthens the result of Theorem 3.1.

Proof of Theorem 3.2: Let L_{P} be a language of PC with a set of parameters S and a set of variables V. Let L_{H} be a language of HiLog with the same sets of parameters and variables.^{4}

We define a pair of mappings:

• HtoP : L_{H}-Structures ⟼ L_{P} -Structures

• P toH : L_{P} -Structures ⟼ L_{H}-Structures

such that for any predicate calculus formula over L_{P} the following holds, where ⊧^{pc} and ⊧^{hilog} denote logical entailment in predicate calculus and HiLog, respectively:

Prop-1: If M_{H} is a semantic structure for L_{H} and HtoP (M_{H}) ⊧^{pc} ϕ, then M_{H} ⊧^{hilog} ϕ.

Prop-2: If M_{P} is a semantic structure for L_{P} such that the cardinality of the domain of M is at least that of S and P toH(M_{P}) ⊧^{hilog} ϕ, then M_{P} ⊧^{pc} ϕ.

The theorem immediately follows from the existence of the mappings with these two properties.

To construct HtoP, let M_{H} =< U, U_{true}, I_{H}, F > be a semantic structure for L_{H}. Define the corresponding structure for L_{P} as follows: HtoP (M_{H}) =< U, I_{P} > has the same domain U as M_{H} and I_{P} is defined below:

• I_{P} (c) = I_{H}(c), if c is a constant of L_{P};

• I_{P} (f) = (I_{H}(f))_{F}^{(k)}, if f is a k-ary function symbol of L_{P}; and

4It is important for the following construction that the HiLog interpreted parameters, such as “=”, “true”, and “false”, are never used as function symbols in the PC language L_{P}.

• I_{P} (p) = {(u_{1}, ..., u_{m})| (I_{H}(p))_{F}^{(m)}(u_{1}, ..., u_{m}) ∈ U_{true}}.

Now, Property 1 of HtoP follows straightforwardly, by induction on the structure of ϕ. Note that here we did not impose any restrictions on semantic structures.

To define P toH, let M_{P} =< U, I_{P} > be a semantic structure for L_{P}, where the cardinality of U is at least as high as that of S. Because of the cardinality assumption, there is a mapping I_{H} from S to U such that

• I_{H}(c) = I_{P} (c) for every symbol c in S that corresponds to a constant symbol c of L_{P}; and

• I_{H}(f) ≠ I_{H}(g) for every pair of distinct symbols f and g in S that correspond to function symbols (of arity > 0) or predicate symbols of L_{P}.

We can now define P toH(M_{P}) = M_{H} =< U, U_{true}, I_{H}, F >, where

• the universe U of M_{H} is the same as that of M_{P};

• the mapping I_{H} from the parameters S of L_{H} to U is the one defined in the previous paragraph; and

• F is defined thus:

– If f ∈ S corresponds to a k-ary function symbol of L_{P}, where k ≥ 1, then (I_{H}(f))_{F}^{(k)}(u_{1}, ..., u_{k}) = I_{P} (f)(u_{1}, ..., u_{k}); for other arities r (r ≠ k), (I_{H}(f))_{F}^{(r)} is defined arbitrarily.

– If p ∈ S is an m-ary predicate symbol, where m ≥ 0, then (I_{H}(p))_{F}^{(m)}(u_{1}, ..., u_{m}) is in U_{true} if and only if (u_{1}, ..., u_{m}) ∈ I_{P} (p); there are no other requirements to the definition of (I_{H}(p))_{F}^{(m)}. Neither are there any requirements to (I_{H}(p))_{F}^{(s)} for other arities s, where s ≠ m.

– On other elements of U, F is defined in an arbitrary way.

Since I_{H} maps distinct function and predicate symbols of S into different elements of U, the mappings (I_{H}(f))_{F}^{(k)} and (I_{H}(p))_{F}^{(m)} are well-defined.

Let ν be a variable assignment. Since L_{H} and L_{P} share the same set of variables and P toH(M_{P}) shares the domain U with M_{P}, ν is a variable assignment for both P toH(M_{P}) and M_{P}. Let ν_{H} and ν_{P} denote the extensions of ν to the set of all terms in L_{H} and L_{P}, respectively. The following properties can be proved by induction:

• for any term t of L_{P} in PC (which is also a term in L_{H}), ν_{H}(t) = ν_{P} (t);

• for any formula ϕ of L_{P} in PC (which is also a formula in L_{H}), P toH(M_{P}) ⊧_{ν}^{hilog} ϕ if and only if M_{P} ⊧_{ν}^{pc} ϕ.

Therefore, if ϕ is valid in HiLog, ϕ is valid in all semantic structures M_{P} such that the cardinality of the domain of M_{P} is at least that of S. If ϕ is also cardinal, this implies that ϕ is true in all semantic structures of predicate calculus. □

3.3 Encoding HiLog in Predicate Calculus

Since HiLog syntax is richer than that of predicate calculus, it may seem that HiLog is a more expressive logic. It turns out, however, that every HiLog formula can be encoded in predicate calculus, and therefore these two logics are equally expressive. It should be borne in mind though that our objective is not to devise a more expressive logic, but a logic whose syntax is more suitable for logic programming. In this respect, one can compare programming in HiLog vs. Prolog to programming in Prolog vs. Horn logic. It is well-known that Horn logic has the computational power of a Turing machine and, therefore, is sufficient for all computational needs. However, programmer’s convenience and the need to simplify problem specification calls for a richer syntax (negation, etc.) and this is why Prolog has the additional constructs it is notorious for. More discussion of this issue appears in Section 8.

The following encoding of HiLog in predicate calculus was suggested by James Wu [57]. Given a HiLog language L_{H} with a set of variables V and parameters S, we define L_{P}^{encode} to be a language of predicate calculus with the set of variables V, constant symbols S, a unique predicate symbol “call”, and for each n ≥ 1, an (n + 1)-ary function symbol apply_{n+1}. Given a HiLog formula ϕ, its encoding in predicate calculus, ϕ^{∗}, is determined by the following recursive transformation rules. In these rules, encodea is a transformation that encodes HiLog terms that appear in contexts where they are interpreted as atomic formulas, and encodet encodes these terms in all other contexts.

• encode_{t}(X) = X, for each variable X ∈ V;

• encode_{t}(s) = s, for each logic symbol s ∈ S;

• encode_{t}( t(t_{1}, ..., t_{n}) ) = apply_{n+1}( encode_{t}(t), encode_{t}(t_{1}), ..., encode_{t}(t_{n}) );

• encode_{a}(t_{1} = t_{2}) = (encode_{t}(t_{1}) = encode_{t}(t_{2}));

• encode_{a}(A) = call( encode_{t}(A) ), where A is a HiLog atomic formula other than equality;

• encode_{a}( A ∨ B) = encode_{a}(A) ∨ encode_{a}(B);

• encode_{a}( A ∧ B) = encode_{a}(A) ∧ encode_{a}(B);

• encode_{a}( ¬A) = ¬encode_{a}(A);

• encode_{a}( (QX)A) = (QX)encode_{a}(A), where Q is either ∃ or ∀.

Given a HiLog semantic structure M =< U, U_{true}, I_{H}, F >, the corresponding predicate calculus structure, encode(M) =< U, I_{P} >, is defined as follows:

• I_{P} (c) = I_{H}(c), for each c ∈ S;

• I_{P} (apply_{n+1})(u, u_{1}, ..., u_{n}) = (u)_{F}^{(n)}(u_{1}, ..., u_{n});

• I_{P} (call) = U_{true};

• The equality predicate, “=”, has the standard interpretation in encode(M)

(i.e., I_{P} (=) =^{def} {< u, u >| u ∈ U}).

The following result and its proof is due to James Wu [57]. The reason for the special treatment of “=” in the above definitions will become apparent in Section 6.4.

Theorem 3.3 (Encoding Theorem) Let ϕ be a HiLog formula and M a semantic structure. Let ν be a variable assignment for the free variables in ϕ. Then

M ⊧_{ν} ϕ if and only if encode(M) ⊧_{ν} encode_{a}(ϕ).

Proof: By structural induction, ν(t) = ν(encodet(t)), for every HiLog term t. Consider now a HiLog atomic formula A, other than an equation. By the definition, encodea(A) = call(encodet(A)). Therefore, M ⊧_{ν} A

if and only if ν(A) ∈ U_{true};

if and only if ν(encodet(A)) ∈ I_{pred}(call); if and only if encode(M) ⊧_{ν} call(encodet(A)); if and only if encode(M) ⊧_{ν} encodea(A).

For the equality, we have encodea(t1 = t2) = (encodet(t1) = encodet(t2)). Thus, M ⊧_{ν} (t1 = t2)

if and only if ν(t1) = ν(t2);

if and only if ν(encodet(t1)) = ν(encodet(t2));

if and only if encode(M) ⊧_{ν} (encodet(t1)) = encodet(t2)); if and only if encode(M) ⊧_{ν} encodea(t1 = t2).

We have thus proved the claim for atomic formulas. The rest of the proof is an easy induction of the structure of HiLog formulas. □

Corollary 3.1 Let ϕ be a HiLog formula. Then ϕ is valid if and only if encode_{a}(ϕ) is valid in predicate calculus.

Proof: Let L_{H} be a HiLog language. It is easy to see that the function encode is a 1-1 and onto mapping from HiLog interpretations of L_{H} to predicate calculus interpretations of L_{P}^{encode} (the language L_{P}^{encode} was defined earlier, before the definition of the encoding of HiLog in PC). Indeed, we could use equations for encode “in reverse” to define a function decode such that decode(encode(M)) = M. The claim now follows from Theorem 3.3. □

We conclude this section with a few remarks to shed some light on the relationship between HiLog and the second-order predicate calculus under the standard semantics [15]. Clearly, one should expect certain similarities because, for example, quantification over predicates and function symbols is allowed in both logics. On the other hand, the first-order nature of HiLog semantics suggests that there must be very significant differences.

For a similarity, it is easy to see that the language of HiLog is rich enough to express so called extensionality axioms. For instance, for arity 2 we can write

∀P∀Q(eq2(P, Q) ↔ ∀X∀Y(P(X, Y) ↔ Q(X, Y)))  (3)

According to (3), eq2(P, Q) is true if and only if P and Q are the same when viewed as binary predicates. This formula is identical to the extensionality axiom for binary predicates in second-order logic with the standard higher-order semantics. Thus, HiLog syntax appears to be rich enough to capture both the intensional and extensional aspects of functions and predicates.

However, a critical difference between the semantics of HiLog and the standard semantics for secondorder logic is the domain of variables. In HiLog, variables range over a nonempty set of intensions. So in (3), P and Q range only over the intensions of binary relations, but there also may be relations without the corresponding intensions (the latter do not affect the meaning of (3) in HiLog). In contrast, in the standard second-order semantics, the domain of predicate variables P and Q is the set of all binary relations over the individual domain. Therefore the extensionality axiom of standard second-order logic talks about all possible relations. Although this distinction does not appear to have impact on the validity of (3), it does make a difference for the so called relation comprehension formulas [15]:

∃P∀X1 ⋯ ∀Xn(P(X1 ⋯, Xn) ↔ ϕ)  (4)

where ϕ is some formula in which P does not occur free and the only free variables are X_{1}, ..., X_{n}. It is well-known that these formulas are valid in the standard second-order predicate calculus. It turns out however, that they are not valid in HiLog. For instance, the formula:

∃P∀X∀Y(P(X, Y) ↔ ¬p(X, Y))  (5)

is not valid in HiLog. One HiLog semantic structure which falsifies it is < {d}, {d}, I, F >, where I(p) = d, and d_{F}^{(k)}(d, ⋯, d) = d for all k(k ≥ 1). Intuitively, this happens because domains of HiLog interpretations do not necessarily have intensions for complements of relations associated with predicate names. Whether this effect is desirable or not depends on the intended meaning of quantification. In HiLog, the quantification is over intensions, and since there is no name for ¬p in T , (5) is not valid.

4 Applications of HiLog

As explained earlier, although the semantics of HiLog is first-order, a term can be viewed as an individual, a function, or a predicate, depending on the context in which it appears. When functions or predicates are treated as objects, they are manipulated as terms through their intensions; when applied to arguments they are evaluated as functions or relations through their extensions. By distinguishing between intensional and extensional aspects of functions and predicates, HiLog preserves the advantages of higher-order logic and avoids the difficulties with extensions introduced by higher-order semantics. In this section we review a subset of HiLog that is suitable for logic programming and then show its uses in higher-order logic programming, definite clause grammars in natural language processing, and other areas.

4.1 Logic Programming in HiLog

For practical applications, we consider logic programming instead of general theorem proving with HiLog. By a logic program we mean a finite set of formulas of the form

∀X_{1}...∀X_{n}(A ← L_{1} ∧ ... ∧ L_{m})

where m ≥ 0, A is an atomic formula, L_{1}, ..., L_{m} are literals, and X_{1}, ..., X_{n} are all the variables occurring in A, L_{1}, ..., L_{m} [34]. Each universal formula in a program can be written as a general clause. However, in logic programming, such clauses are often written as:

A ← L_{1}, ..., L_{m}.

If L_{1}, ..., L_{m} are atomic formulas, such clauses are called definite Horn clauses, and a logic program consisting of only definite clauses is called a definite logic program.

For definite logic programs, standard logic programming techniques [52, 4, 34] can be used to define the declarative and procedural semantics. The only difference is the form of atomic formulas and unification (unification is discussed in Section 6.3). For instance, for definite HiLog programs, the model intersection property holds and, therefore, each such program has a unique minimal (with respect to set inclusion) Herbrand model. The T_{P} operator is also defined as usual: If H is a Herbrand interpretation and P is a definite program, T_{P}(H) is the set of all literals that are heads of ground clauses of P whose body is satisfied in H. The standard results about fixpoint also hold. These facts are easy to verify directly or with the use of Theorem 3.3.

For logic programs with negation, semantics is defined by choosing one or several of the minimal Herbrand models. For instance, the definitions of well founded semantics [48, 50, 53, 54] and stable model semantics [19] are independent of the notions of atomic formulas and Herbrand bases and thus the same definitions can be applied to HiLog. Some results on negation in HiLog can be found in [51].

4.2 Higher-Order and Modular Logic Programming

Higher-order constructs have been found very useful in programming practice. An example is the maplist of Lisp. It can be defined in HiLog either as a higher-order predicate

maplist(F, [], []).

maplist(F, [X|R], [Y|Z]) ← F(X, Y), maplist(F, R, Z).

or as a generic predicate

maplist(F)([], []).

maplist(F)([X|R], [Y|Z]) ← F(X, Y), maplist(F)(R, Z).

The latter is possible since HiLog allows complex terms such as maplist(F) to appear as predicates.

The example in Section 2.1 shows the usefulness of generic view definitions, such as closure, in databases. Generic transitive closure can also be defined in Prolog:

closure(R, X, Y) ← C =.. [R, X, Y], call(C).

closure(R, X, Y) ← C =.. [R, X, Z], call(C), closure(R, Z, Y).

However, this is obviously inelegant compared to HiLog (see Section 2.1), since this involves both constructing a term out of a list and reflecting this term into an atomic formula using “call”. The point of this example is that the lack of theoretical foundations for higher-order constructs in Prolog resulted in an obscure syntax, which partially explains why Prolog programs involving those constructs are notoriously hard to understand.

It turns out that since variables may be instantiated to HiLog terms which in turn have propositional meaning, there is no need for the infamous “call” predicate that is built into Prolog. The latter is naturally defined in HiLog as

call(X) ← X.

which has the intended semantics.

Higher-order constructs have been also used in database languages, such as COL [1] and LDL [5, 45], for modeling complex objects containing sets. The original semantics of these languages, as described in [1, 5, 45], is higher-order, which leads to certain semantic and computational difficulties. In Section 5 we propose an alternative semantics for COL and LDL using HiLog, and argue that the latter is computationally more tractable and practically more convenient.

Modular logic programming is another application where higher-order logic has been employed. In [7, 8], a theory of modules is developed based upon standard second-order logic. The semantics of a module is a second-order relation over first-order predicates interpreted as first-order relations. The relational view of modules is a natural extension of logic programming. However, standard second-order logic is not recursively axiomatizable, and practical usage of modules does not need the full power of second-order predicate calculus.

HiLog can be used to provide a simple alternative semantics for modular logic programming which, unlike [7, 8], has a sound and complete proof theory. Consider the following program fragment (which is well-formed both in predicate calculus and in HiLog):

sort([], []).

sort([X|T], R) ← part(X, T, U1, U2), sort(U1, V1), sort(U2, V2), append(V1, [X|V2], R).

part(M, [], [], []).

part(M, [E|L], [E|U1], U2) ← order(E, M), part(M, L, U1, U2). part(M, [E|L], U1, [E|U2]) ← not order(E, M), part(M, L, U1, U2).

To turn it into a module definition, we need to determine its interface with other modules. This program fragment contains two defined predicates: sort and part. Suppose that predicate sort is exported, while part is an internal predicate. There are also two undefined predicates order and append. Let us assume that predicate order is a parameter which can be instantiated to any binary predicate of the user’s choice; predicate append will be considered as a global predicate defined outside the module. To obtain a module definition, we replace each non-global predicate symbol by a predicate variable of the same arity, where different predicate names are replaced by distinct variables. This is done to ensure the local scope of those symbols, since only variables have local scopes in logic. For sorting, the module definition will then look like this:

mod sort (Sort, Order) =^{def} { Sort([], []). Sort([X|T], R) ← Part(X, T, U1, U2),

Sort(U1, V1), Sort(U2, V2), append(V1, [X|V2], R).

Part(M, [], [], []).

Part(M, [E|L], [E|U1], U2) ← Order(E, M), Part(M, L, U1, U2).

Part(M, [E|L], U1, [E|U2]) ← not Order(E, M), Part(M, L, U1, U2). }.

Here mod sort is the module name. In HiLog, mod sort is a first-order parameter symbol, just like append. In contrast, under the second-order semantics of [7, 8], mod sort is viewed as a second-order predicate symbol.

Notice that the head of the module definition defines the module interface: it contains all exported predicates (Sort) and input predicate parameters (Order); the body of the definition defines the “implementation” of the module. Individual variables are still universally quantified with respect to each clause in the body (unless they are module parameters, which is discussed in [7, 8]). Non-interface predicate variables in the body, such as Part, represent private predicates that are not to be seen outside the module. The quantification of predicate variables is such that all input predicate parameters are universally quantified and all other predicates (private and exported ones) are existentially quantified inside the scope of the universal quantification of the input predicate variables. It is the existential quantification of private predicate variables that ensures the invisibility of data local to the module. The above module definition defines not only first-order predicates in the body, but also the second-order predicate (i.e., the module name) in the head. Let Body(Sort, Part, Order) be any proof theoretic characterization of the body of the definition for mod sort (e.g., circumscription [33]). Then the meaning of the module definition can be expressed via the following formula:

∀ Order ∃ Sort ∃ Part (mod sort(Sort, Order) ∧ Body(Sort, Part, Order))

Instead of viewing this formula as one in the standard second-order logic, we can consider it as a formula in HiLog and have a more tractable semantics for module definitions.

The HiLog semantics for modules yields the same result as [7] in most cases, but disagrees with [7] in marginal situations when the inherent difference between the intensional treatment of predicates in HiLog and the extensional treatment in [7, 8] becomes essential. For instance, when two different predicates p and q that are extensionally equivalent are to be unified, they are unifiable in the standard second-order semantics, but not in HiLog.

Another distinction is that, HiLog modules have features that are not found in [7]. For instance, modules in [7], being second-order predicates, cannot be imported into other modules, since second order predicates cannot be arguments to other second-order predicates. Therefore manipulating modules requires more than just a second-order PC. In contrast, there are no such difficulties in HiLog, and module names, being merely first-order terms in HiLog, can be passed to other modules as parameters.

4.3 Definite Clause Grammars in HiLog

Definite clause grammars (DCGs), developed for processing natural language [46], extend the contextfree grammars by adding arguments for checking the agreement among linguistic structures, and by allowing arbitrary computation in the body of a rule. They can be translated into Prolog by adding an additional pair of arguments for representing the string of words being parsed. As an example, consider the following DCG rules:

s(sent(Subj, Verb)) ⟶ np(Subj, Num), vp(Verb, Num). np(Word, Num) ⟶ [Word], {isproper name(Word, Num)}. vp(Word, Num) ⟶ [Word], {isverb(Word, Num)}.

The standard transformation yields the following Prolog program:

s(sent(Subj, Verb), L0, L) ← np(Subj, Num, L0, L1), vp(Verb, Num, L1, L). np(Word, Num, L0, L) ← connect(Word, L0, L), isproper name(Word, Num). vp(Word, Num, L0, L) ← connect(Word, L0, L), isverb(Word, Num). connect(Word, [Word|L], L).

Suppose we have the following facts:

isproper name(john, singular).

isverb(walks, singular).

Then, parsing a natural language sentence such as

::= john walks. will be reduced to evaluating a logical query

?- s(X, [john, walks], []).

Although Prolog is adequate for many languages defined by DCG grammars, there are cases in which generic grammatical rules become necessary. Optionality of a nonterminal symbol and the occurrence of an arbitrary symbol zero or more times are some of the examples [2]. Such rules can be specified as follows (adapted from [2]):

option(X) ⟶ X. option(X) ⟶ [].

seq(X) ⟶ X, seq(X).

seq(X) ⟶ [].

nonempty seq(X) ⟶ X, seq(X).

Unfortunately, the above translation into Prolog no longer works, since Prolog does not allow variable predicates. Indeed, blindly following this recipe, we would get

nonempty seq(X)(L0, L) ← X(L0, L1), seq(X)(L1, L).

which is a HiLog but not a Prolog rule. To overcome this problem, we could try to turn X(L0, L) into something like NewX =.. [X, L0, L], call(NewX). However, even this patch does not work all the time. Because of the syntactic limitations of Prolog, special mechanisms for translating such grammars into Prolog are needed, and papers have been written on that subject (e.g., [2]). In contrast, as we have just seen, translation of generic grammars into HiLog is immediate, and does not require any special machinery: we simply go on (as suggested by the standard algorithm) and replace each nonterminal, N, by a HiLog atom N(L1, L2). Regardless of whether N is a predicate symbol, a function symbol, a variable, or a term, HiLog accommodates them all, due to the richness of its syntax.

As a matter of fact, even the original DCG-to-Prolog translation could be made more natural in HiLog. DCG nonterminals with parameters are readily transformed into parameterized predicates in HiLog. For example, the first DCG rule above:

s(sent(Subj, Verb, L0, L)) ⟶ np(Subj, Num, L0, L1), vp(Verb, Num, L1, L).

would become

s(sent(Subj, Verb))(L0, L) ← np(Subj, Num)(L0, L1), vp(Verb, Num)(L1, L).

4.4 Query Evaluator

Consider relational expressions composed from, say, binary relations connected by the relational operators minus, union, and the like. Suppose that the parser has already produced a parse tree (parsing is easy using Horn clauses) of the expression in the form of a term, say, minus(union(p, q), inter(q, r)), or similar. As the next step, we would like to write an evaluator for such expressions, which in HiLog looks as follows:

minus(P,Q)(X,Y) ← P(X,Y), ¬Q(X,Y).

union(P,Q)(X,Y) ← P(X,Y). union(P,Q)(X,Y) ← Q(X,Y).

. . . . . . . . .

For comparison, we present an analogue of the above program in Prolog. The simplest approach to this problem seems to be to define a translation predicate, tr, that converts parse trees into Prolog goals, and then use call. The rules for tr are as follows:

tr( minus(P,Q), X, Y, ( G1 , not (G2)) ) ← tr(P, X, Y, G1), tr(Q, X, Y, G2).

tr( union(P,Q), X, Y, ( G1 ; G2) ) ← tr(P, X, Y, G1), tr(Q, X, Y, G2).

. . . . . . . . .

tr( P, X, Y, Atom) ← Atom =.. [P, X, Y].

The first observation about this Prolog program is that it is clumsy compared to its HiLog counterpart (notice that the arguments X, Y in tr are essential for the program to run correctly). Second, the last rule is intended to capture the situation where P is instantiated to a predicate symbol. However, this restriction is only implicit in the built-in predicate “=..”, which will give an error if P is not a predicate symbol. One way to get around this is to list all the facts such as tr( p, X, Y, p(X,Y) ) (for each predicate symbol) in advance. However, this is particularly inconvenient in the database environment when the user may create or delete new relations, since the above program would have to be updated each time.

The ease of writing the above program in HiLog stems from the ability to represent intermediate results of query evaluation in a natural way. For instance, minus(p, q) can be viewed as the name of an intermediate relation for the result of subtracting Q from P. However, it should be clear that in order to take full advantage of HiLog, arities of all relations must be known at compile time, since we must know how many variables should appear in various places in rules. Therefore, rules for the relational operators that do not change the arities of relations (like the ones above) look particularly attractive in HiLog. On the other hand, operators such as join or Cartesian product require a heavier machinery, such as functor and arg. Still, this program would be much more elegant in HiLog than in Prolog.

4.5 Type Checking

Recently, Thom Fruehwirth has pointed out to us that the monomorphic type checking system of [16] can be naturally extended to a polymorphic type checking system for HiLog [17], while expressing general polymorphism in predicate calculus is usually quite cumbersome.

5 HiLog as a Database Programming Language

In this section, we show that HiLog provides an alternative (first-order) semantics to some of the wellknown database languages with higher-order semantics, thereby eliminating some of their problems. Specifically, we will focus on COL [1] and LDL [5, 45]. After that we will discuss various applications of HiLog to object-oriented databases.

COL [1] is a logic-based language for complex objects. One notable feature of COL is that, in addition to finite set construction, it also provides so called “data functions”. These functions may take sets and individuals as arguments, and return sets as results. Data functions can be defined by either facts or rules. For example, some of the operations over sets can be defined as data functions as follows [1]:

X ∈ intersection(S1, S2) ← X ∈ S1, X ∈ S2.

X ∈ union(S1, S2) ← X ∈ S1. X ∈ union(S1, S2) ← X ∈ S2. X ∈ difference(S1, S2) ← X ∈ S1, not (X ∈ S2).

Notice that variables S1, S2 range over a domain of sets, and thus, according to our classification, the semantics of COL is higher-order. This higher-orderness presents certain semantic problems for logic programs in COL. Consider the following example adapted from [1]:

person(peter, {bridge}). person(thom, {chess,tennis}). person(thom, hobby(peter)). Y ∈ hobby(X) ← person(X,Z), Y ∈ Z.

This program is unstratified in COL, since hobby and person mutually depend on each other and, therefore, the following perfectly legal queries that request all Tom’s hobbies and inquire whether Tom plays bridge, will be rejected:

?- X ∈ hobby(thom). ?- person(thom, { chess, tennis }).

To cope with this problem, [1] proposes to use an analogue of the notion of local stratification adapted from logic programming [47].

For simplicity, we restrict our attention to COL programs without tuple constructs and such that their finite set-constructs have no variables. Thus, the forms such as { a, b } are allowed, but { a, b, X } are not. Later we will show how to extend our results to the general case. Now, the restricted COL programs can be transformed into HiLog programs as follows:

1. Replace every finite set construction, {a_{1}, ..., a_{n}}, that appears in the COL program by a new HiLog logical symbol, sym, and add the following facts to the program: sym(a_{1}), ..., sym(a_{n}). Identical finite set constructions must be consistently replaced by the same symbol. For instance, person(thom, {chess, tennis}) will be replaced by person(thom, hobby thom), and the following pair of facts:

hobby thom(chess). hobby thom (tennis) .

2. Replace COL-formulas of the form X ∈ f(...) by HiLog formulas f(...)(X).

Then the above program is transformed into the following well-formed HiLog program:

person(peter, hobby peter). person(thom, hobby thom). person(thom, hobby(peter)). hobby peter(bridge). hobby thom(chess). hobby thom(tennis). hobby(X)(Y) ← person(X,Z), Z(Y).

and the corresponding queries become

?- hobby thom(X). ?- person(thom, hobby thom).

These queries yield the same results as their counterparts in COL (provided that the above unstratified COL program is given the intended semantics). For another example, consider the COL query

?- person(thom, {chess}).

to the above database (with the last rule deleted, to ensure stratification). This query fails because {chess} and {chess, tennis} are two different sets. The corresponding HiLog query is

?- person(thom, another hobby thom), another hobby thom(chess).

(and the database must contain another hobby thom(chess)). This query also fails since, similarly to COL, another hobby thom represents a different set of hobbies than hobby thom. However, the query

?- person(thom, hobby thom), hobby thom(chess).

succeeds, since it is asking whether Thom plays chess, while the previous query inquired whether { chess } is one of Thom’s hobby sets. Notice that the semantics of COL treats Thom as if he had different sets of hobbies in different “frames of mind,” and we have been able to capture this aspect of COL pretty adequately. In contrast, in COL there is no easy way (without introducing additional rules) to ask whether Thom plays chess, which demonstrates greater flexibility of HiLog compared to COL.

There is, however, a significant difference between the semantics of COL and that of HiLog. For instance, suppose that instead of the previous clause for hobby, the hobby-function is defined as follows:

chess ∈ hobby(peter). bridge ∈ hobby(peter).

Then the query

?- person(thom, {bridge, chess}).

returns the answer “true” in COL, while the corresponding query

?- person(thom, yet another hobby thom).

in HiLog returns “false”.

This difference stems from the fact that in COL, the domain of set variables consists of sets (extensions), while the domain of variables in HiLog is a set of objects (intensions). Thus, in COL, person(thom, hobby(peter)) is evaluated to person(thom, {bridge, chess }), which allows the above COL query to succeed. Our contention is, however, that the separation of intensional and extensional aspects in HiLog makes it more flexible: The extensional semantics of COL can be captured in HiLog rather easily, by defining extensional equality of intensions. For instance, the following formula

∀P∀Q ( eq1(P, Q) ↔ ∀ X ( P(X) ↔ Q(X) ))

says that P and Q always represent the same unary relations extensionally; P and Q may be intensionally different though, and nothing is said about, say, binary relations represented by P and Q. However, the above axiom does not quite capture our intentions. What we really need is the extensional equality of predicates with respect to the intended semantics of logic programs. For the purposes of this section, we adopt the perfect model semantics of locally stratified programs, which can be defined for HiLog along the same lines of [47]. The intended extensional equality can now be captured via the following rules with negation: eq1(P, Q) ← subset(P, Q), subset(Q, P). subset(P, Q) ← not not subset(P, Q). not subset(P, Q) ← P(X), not Q(X).

Now, if desirable, HiLog can simulate the extensional semantics of COL for the above query as follows:

?- person(thom, X), eq1(X, yet another hobby thom).

Recall that according to the first transformation rule, the database would contain the facts

yet another hobby thom(bridge). yet another hobby thom(chess).

Since person(thom, hobby(peter)) is one of the original facts in the database, the above HiLog query succeeds with X = hobby(peter).

So, to simulate the semantics of COL more closely (but still not exactly), we must add one more transformation rule, which must be applied after the first two:

3. Replace every literal p(..., t, ...) in the body of a rule (including the queries), where t is either a term involving a data function or a constant that replaces a finite set construction (introduced by the first transformation rule), by the following conjunction: p(..., X, ...), eq1(X, t). For instance, in the above, the query

?- person(thom, yet another hobby thom). was replaced by

?- person(thom, X), eq1(X, yet another hobby thom).

We complete our discussion of COL by showing how to extend the translation described above to the general case. Capturing the tuple construct is easy. We just reserve a parameter symbol, say tuple, for the specific purpose of representing COL tuples; e.g., [a,b] and [c,d,e] become tuple(a,b) and tuple(c,d,e), respectively. For the set construct, we reserve a special symbol, setc. Now, every finite set construct, e.g., { a, b, X, d }, should be replaced by a HiLog term, setc(a,b,X,d), and the appropriate facts must be added to the database. In our example these would be

setc(a,b,X,d)(a). setc(a,b,X,d)(b). setc(a,b,X,d)(X). setc(a,b,X,d)(d).

The transformation rule 2 requires no change; in rule 3 we only need to replace the phrase “constant replacing a finite set construct” by the phrase “set term replacing finite set construct.”

LDL [5, 45] is another influential logic database language with a higher-order semantics. In addition to finite set construction, it provides the, so called, grouping construct, which is even more general than data functions of COL. Again, LDL programs can be translated into HiLog with an alternative, first-order, semantics. Similarly to COL, certain programs that are not well-formed in LDL can be given satisfactory semantics by such a translation.

Finite set constructs of LDL are translated into HiLog the same way as in the case of COL. For the grouping construct (which in LDL can occur only in rule heads), we can do the following:

Replace every LDL rule of the form p(X⃗, < Y⃗ >) ← body, where X⃗, Y⃗ are vectors of variables, by the pair of HiLog rules:

p(X⃗, sym(X⃗)) ← body. sym(X⃗)(Y⃗) ← body.

where sym is a new HiLog symbol.

Consider, the following LDL program:

p(X).

p(<X>) ← p(X).

Intuitively, this says that p is true of all elements of the domain and also of some other element of the domain that, in some sense, is the set of all domain elements. However, in LDL, sets are members of the domain on a par with individuals. As a result, the above program becomes tantamount to the famous set theoretic paradox, since p has to contain the set of all sets as an element. The corresponding HiLog program is

p(X).

p(a) ← p(X). a(X) ← p(X).

It defines a predicate which is true of every element in the domain. It also defines a as a symbol that represents the entire domain, whenever this symbol appears as a constant within an atomic formula. This corresponds to the aforementioned intuitive meaning of the above LDL program, which favors the HiLog semantics over LDL. This also shows that, in general, the translation of LDL into HiLog does not capture all the power of the grouping construct^{5}. However, in most “normal” cases of grouping in LDL, the corresponding HiLog program gives the same result. For instance, consider the set-intersection example from [5]:

intersect(S,T,<X>) ← member(X, S), member(X, T).

The corresponding HiLog program is:

intersect(S,T,inter(S,T)) ← member(X, S), member(X, T).

inter(S,T)(X) ← member(X, S), member(X, T).

which gives the same result. Note, however, that in HiLog set intersection has a more concise and elegant representation:

inter(S,T)(X) ← S(X), T(X).

We thus see that HiLog provides an alternative (we believe, computationally more attractive) semantics to LDL. Unlike COL, where it seems that HiLog can closely mimic the semantics, there is a more dramatic difference between HiLog and LDL because the latter is so expressive that even logical paradoxes can be represented without much difficulty. Such paradoxes are not representable in HiLog since the latter has a first-order semantics, and the translation of paradoxical LDL rules yields rather benign HiLog programs.

5In our opinion, the above discussion suggests that capturing the semantics of grouping construct exactly is not necessary and even harmful.

To conclude this comparison, we mention that the alternative semantics for sets in LDL and COL described above is in the same spirit as the semantics described in C-logic [11] and O-logic [27], although the latter are first-order (object-oriented) languages. It appears thus, that higher-orderness of the syntax of HiLog is inessential in order to simulate sets. However, it is essential for other applications described earlier. It seems like an interesting observation, therefore, that changing the philosophy behind logical languages can—in some cases—eliminate the need in higher-orderness either in semantics, or in syntax, or in both.

Another promising application of HiLog in the database field is its use as an implementation vehicle for object-oriented languages recently proposed in [11, 27, 23, 24]. C-logic [11] is the simplest of the three; it supports complex objects, object ids, sets, and classes. For instance, the “hobby” example discussed earlier can be represented in C-logic as follows:

person: peter[hobby → {bridge}].

person: thom[hobby → {chess, tennis}].

thom[hobby → {X}] ← peter[hobby → {X}].

yielding the same results as those produced by the corresponding HiLog representation.

C-logic admits a natural translation into predicate calculus by viewing each class symbol (e.g., person) as a unary predicate, and each set-valued attribute (e.g., hobby) as a binary predicate [11]. Ologic [27] extends C-logic by allowing single-valued attributes and by introducing a lattice structure over object ids, which helps to localize the effect of data inconsistency. Translation of O-logic into predicate calculus is just a shade more complex; it additionally requires axiomatization of functional attributes and data inconsistency. F-logic [23, 24] takes object-oriented logica to a new dimension by introducing higher-orderness with a first-order semantics, in the same spirit as HiLog. Although it can be encoded in predicate calculus, this encoding is neither natural nor suggestive of an efficient implementation. However, an extension of the algorithm from [11] would translate F-logic into HiLog quite naturally.

This opens up a possibility of using HiLog for fast prototyping of object-oriented logic languages. Compared to the direct implementation of object-oriented databases, the advantage of HiLog as an implementation platform is that it can be relatively easily implemented using one of the already available technologies developed for Prolog [56, 42] or LDL.

6 Proof Theory of HiLog

Because of the encoding in Section 3, one can use a proof theory for predicate calculus in order to prove theorems for HiLog. However, a proof theory stated in terms of this encoding is neither intuitive, nor suggestive of a possible efficient implementation. Furthermore extensions of HiLog will be developed in order to support more features such as lambda abstractions and dynamic updates, and these extensions may not have a direct translation into predicate calculus. A direct proof theory of HiLog is therefore important in its own right and may provide additional insights for further investigations of HiLog extensions.

In this section, we present a resolution-based proof theory given directly in terms of HiLog. The following issues are examined: Skolem and Herbrand theorem, unification, and resolution. The discussion follows the development of resolution-based proof theory for predicate calculus [6].

6.1 Skolemization

Given a sentence ϕ in HiLog, it can be transformed into an equivalent formula ϕ′ in prenex normal form Q_{1}X_{1} … Q_{n}X_{n}ψ, where Q_{i} (1 ≤ i ≤ n) is either ∀ or ∃, ψ is a quantifier-free formula in conjunctive normal form, and X_{i}(1 ≤ i ≤ n) are all variables occurring in ψ. The rules for this transformation are identical to those for the ordinary predicate calculus, since the usual De Morgan’s laws apply due to the fact that the definition of logical entailment relation ⊧_{ν} in Section 2.3 is identical to that in predicate calculus (except for the notion of atomic formulas).

Because of the similarities between HiLog and predicate calculus, one might think that by eliminating all existential quantifiers in ϕ′ using the usual Skolemization process in predicate calculus, we will obtain a Skolem standard form ϕ∗ of ϕ, which is unsatisfiable if and only if so is ϕ. However, unsatisfiability of ϕ∗ does not entail unsatisfiability of ϕ.^{6} To see this, consider

ϕ ≡ ∀X∃Yp(X, Y) ∧ ∀F∃Z¬p(Z, F(Z)).

Converting ψ into prenex normal form and then Skolemizing X and Y in the ordinary manner (using the new function symbols g and h), yields

ϕ∗ ≡ ∀X∀F( p(X, g(X)) ∧ ¬p(h(F), F(h(F))) ).

It is easy to see that ϕ is satisfiable in HiLog (but not in the second-order predicate calculus!), which can be verified directly by constructing a semantic structure M =< U, U_{true}, I, F > in which for every u ∈ U the function u_{F}^{(1)} is different from all the functions λ : U ⟼ U defined by the expression ∀X∃Yp(X, Y). In contrast, ϕ∗ is unsatisfiable, since

p(h(g), g(h(g))) ∧ ¬p(h(g), g(h(g)))

is an instance of ϕ∗.

Intuitively, the reason why the usual Skolemization process misbehaves is that in HiLog it is not enough to choose a new symbol to represent a Skolem function: such a symbol also needs to be assigned a new intension. Indeed, we have to assign an appropriate Skolem function as an extension of the symbol introduced by Skolemization. In predicate calculus, extensions are assigned directly to function symbols and, therefore, by choosing a new function symbol we can construct a semantic structure for any desired Skolem function. In contrast, HiLog assigns extensions to intensions of function symbols and simply choosing a new symbol is no longer enough: we should be able to assign a new intension to such a symbol, which—as the above example shows—is not always possible. In fact, as we shall see, choosing a new symbol is not that crucial for Skolemization in HiLog.

One way to overcome this problem is to modify Skolemization so as to avoid the need to assign new intensions to Skolem functions. Instead of introducing a new Skolem symbol, we will use an unused arity of one of the old symbols, patching the extra argument positions. For the formula ϕ above, we could use, say, symbol p with the arity 3 for Y and with the arity 4 for Z, obtaining the following Skolemized form:

∀X p(X, p(X, p, p)) ∧ ∀F¬p(p(F, p, p, p), F(p(F, p, p, p))).

Notice how the symbol p was used to fill in the argument positions of the terms p(X, p, p) and p(F, p, p, p).

Let L be a language of HiLog that contains at least one parameter symbol. Given a formula ϕ_{0} of L in prenex normal form Q_{1}X_{1} … Q_{n}X_{n}ψ, where Q_{i} (1 ≤ i ≤ n) is either ∀ or ∃, ψ is a quantifier-free formula in conjunctive normal form and X_{i}(1 ≤ i ≤ n) are all variables occurring in ψ. Suppose that Q_{i} is the leftmost existential quantifier in ϕ. Let k be the maximum arity that has been used in ϕ, which exists since ϕ is finite. We obtain a new formula ϕ_{1} by eliminating the leftmost existential quantifier Q_{i} in ϕ and replacing every occurrence of X_{i} in ψ with p(X_{1}, ⋯, X_{i−1}, p, ..., p) which has max(k + 1, i − 1) arguments. Assume that there are m existential quantifiers in ϕ_{0}. We repeat this process for every ϕ_{j}(j < m) and finally derive a formula ϕ_{m} without any existential quantifiers. The formula ϕ_{m} is called the Skolem standard form of ϕ_{0}.

6We are grateful to one of the referees for suggesting this example and pointing out to a mistake in an earlier draft of this paper.

Lemma 6.1 A sentence ϕ is unsatisfiable if and only if its Skolem standard form ϕ^{∗} is unsatisfiable.

Proof: Without loss of generality, we assume that ϕ is already in prenex normal form. Let ϕ_{0} be ϕ and m be the number of existential quantifiers in ϕ. Then ϕ^{∗} is ϕ_{m}, where each ϕ_{j}(1 ≤ j ≤ m) is obtained from ϕ_{j−1} by the above Skolemization process. We show that ϕ_{j} is unsatisfiable if and only if ϕ_{j−1} is unsatisfiable.

Let ϕ_{j−1} be in a prenex normal form ∀X_{1}...∀X_{i−1}∃X_{i}Q_{i+1}X_{i+1}...Q_{n}X_{n}ψ[X_{1}, ..., X_{n}], where X_{i} is the leftmost existential variable, ψ[X_{1}, ..., X_{n}] is a formula in conjunctive form and X_{1}, ..., X_{n} are all the variables occurring in it. Suppose that k is the maximum arity that has been used in ϕ_{j−1}, and f is the parameter symbol used in the Skolemization of X_{i}. Then ϕ_{j} is of the form

∀X_{1}...∀X_{i−1}Q_{i+1}X_{i+1}...Q_{n}X_{n}ψ[X_{1}, ..., X_{i−1}, f(X_{1}, ..., X_{i−1}, f, ..., f), X_{i+1}, ..., X_{n}],

where f(X_{1}, ..., X_{i−1}, f, ..., f) has max(k + 1, i − 1) arguments.

Suppose that ϕ_{j−1} is true in a semantic structure M =< U, U_{true}, I, F > but ϕ_{j} is unsatisfiable. Then for every x_{1}, ..., x_{i−1} ∈ U, there exists x_{i} ∈ U such that

M ⊧_{ν} Q_{i+1}X_{i+1}...Q_{n}X_{n}ψ[X_{1}, ..., X_{n}],  (6)

for every variable assignment ν that maps X_{1}, ... , X_{i} to x_{1}, ... , x_{i}, respectively. We construct a new semantic structure M′ =< U, U_{true}, I, F′ >, where F′ is exactly the same as F except that for every x_{1}, ..., x_{i−1} ∈ U, I(f)_{F′}^{k+1}(x_{1}, ..., x_{i−1}, I(f), ..., I(f)) = x_{i}, where x_{i} is chosen as explained in (6) above. Since the arity k + 1 is not used in ϕ_{j−1}, I(f)_{F}^{k+1} is not used to determine whether (6) holds. Therefore, M′ ⊧_{ν} ϕ_{j}. Since ν was chosen arbitrarily for X_{1}, ..., X_{i−1} and X_{i} does not occur in ϕ_{j}, it follows that M′ ⊧ ϕ_{j}, contrary to the assumption that ϕ_{j} is unsatisfiable. Therefore ϕ_{j−1} must be unsatisfiable.

In the other direction, assume that ϕ_{j} is true in a semantic structure M. From the definition, it would follow that ϕ_{j−1} is true in M—a contradiction. Thus ϕ_{j} must be unsatisfiable. □

Note that Skolemization in HiLog, as presented above, works for finite sets of formulas only. For infinite sets, one can use the compactness theorem for HiLog (which holds because of the encoding theorem, Theorem 3.3) to guarantee that there always are “spare” arities to use in Skolemization. Another approach would be to introduce sorted symbols into HiLog and then use classical Skolemization, which does not rely on the existence of unused arities. The latter, however, requires an extension to the syntax and semantics of HiLog and will not be discussed here.

6.2 Herbrand’s Theorem

Once Skolemized, we can restrict our attention to universal formulas, i.e., to formulas in prenex normal form whose prefix contains universal quantification only. Furthermore, transforming such formulas into conjunctive normal form, yields HiLog formulas in the clausal form. As usual, we can then drop quantification altogether with the understanding that clauses are implicitly universally quantified. Variable-free formulas are called ground. The rest of the formulas are nonground.

Herbrand interpretations for HiLog were defined in Section 2.3. Recall that given a HiLog language L, its Herbrand universe, HU(L), coincides with its Herbrand base and is defined as the set of all ground (i.e. variable-free) HiLog terms. However, when the equality predicate is taken into account, the definition of Herbrand interpretations needs adjustment.

Definition 6.1 Let L be a HiLog language and H be a subset of its Herbrand base. Then H is called a Herbrand interpretation if it is closed under the congruence:

• (α = α) ∈ H;

• if (α = β) ∈ H, then (β = α) ∈ H;

• if (α = β), (β = γ) ∈ H, then (α = γ) ∈ H;

• if L, (α = β) ∈ H and L′ is the result of replacing of an occurrence of α in L by β, then L′ ∈ H.

Given a Herbrand interpretation H, we can define satisfaction of formulas in H similarly to the classic case:

• If a is a ground HiLog atomic formula, then H ⊧ a if and only if a ∈ H.

• If ϕ and ψ are ground HiLog formulas then

– H ⊧ (ϕ ∨ ψ) if and only if H ⊧ ϕ or H ⊧ ψ.

– H ⊧ (ϕ ∧ ψ) if and only if H ⊧ ϕ and H ⊧ ψ.

– H ⊧ ¬ϕ if and only if it is not the case that H ⊧ ϕ.

• If ϕ is a universal formula then H ⊧ ϕ if and only if H ⊧ ϕ′ for every ground instance ϕ′ of ϕ.

To avoid possible misunderstanding, recall that in the presence of equality we only consider those semantic structures that assign the intended meaning to the equality predicate (see Section 2.3). To emphasize this fact, we will call such semantic structures E-structures. We can then talk about Eunsatisfiable and E-valid formulas, i.e. formulas that are false (resp. true) in all E-structures.

Lemma 6.2 Let L be a HiLog language. For every E-structure M there is a Herbrand interpretation H_{M} such that for every universal formula ϕ, M ⊧ ϕ if and only if H_{M} ⊧ ϕ. Likewise, for every Herbrand interpretation H, there is an E-structure M_{H} such that H ⊧ ϕ if and only if M_{H} ⊧ ϕ, for every universal formula ϕ.

Proof: If M is an E-structure then the corresponding Herbrand interpretation H_{M} is simply the set of all ground atomic formulas of L satisfied by M.

Conversely, let H be a Herbrand interpretation. The corresponding E-structure M_{H} =< U, U_{true}, I, F > is defined thus:

1. U =^{def} HU(L)/ =, the factor-space of the Herbrand universe, HU(L), with respect to the equivalence relation induced by the equality atoms in H. If s ∈ HU(L), its corresponding element in U will be denoted by [s].

2. U_{true} =^{def} HU(L)/ =, the factor-space of H with respect to the aforesaid equivalence relation.

3. I : S ⟼ U is obtained from the identity embedding Id : S ⟼ HU(L) by composing Id with the natural epimorphism HU(L) ⟼ U, i.e., for each s ∈ S, I(s) = [s].

4. F is defined thus: For every [s] ∈ U and k ≥ 0, [s]_{F}^{(k)}([t_{1}], ..., [t_{k}]) = [s(t_{1}, ..., t_{k})].

It is left to the reader to verify that M and H_{M} (resp., H and M_{H}) stand in the desired relationship to each other. The proof is carried out by structural induction on HiLog formulas, similarly to the classic case. □

As a consequence of the above lemma, a universal formula is E-unsatisfiable if and only if it has no Herbrand model:

Corollary 6.1 A set S of HiLog clauses is E-unsatisfiable if and only if S is false under all Herbrand interpretations of S.

Theorem 6.1 (cf. Herbrand’s Theorem) A set S of HiLog clauses is E-unsatisfiable if and only if there is a finite E-unsatisfiable set S′ of ground instances of clauses of S.

Proof: It is easy to verify that for any set of HiLog clauses S, the encoding of Section 2.3 establishes a 1-1 correspondence between Herbrand interpretations of S and those of encode_{a}(S). The only subtlety here is that, in HiLog, the Herbrand universe and the Herbrand base coincide, while in predicate calculus they are distinct. For this reason, the Herbrand universe of encode_{a}(S) is obtained by applying encode_{t} to the Herbrand universe of S, while the Herbrand base of encode_{a}(S) is obtained from that of S via encode_{a}.

Herbrand’s theorem for HiLog now directly follows from Theorem 3.3 and the analogous result in predicate calculus [6]. □

6.3 Unification

Although HiLog allows arbitrary terms to appear in places where only predicates and functions are usually allowed in predicate calculus, unification in HiLog is a very simple extension of unification in predicate calculus and is decidable. This is mainly because HiLog separates intensions from extensions and does not have any non-trivial built-in equality theory over intensions.

Except for the different notion of terms in HiLog, the definitions of substitutions, applications of substitutions to terms, and substitution composition in HiLog are the same as those in predicate calculus [6].

Definition 6.2 A substitution is a finite set of the form {t_{1}/X_{1}, ..., t_{n}/X_{n}}, where X_{1}, ..., X_{n} are distinct variables, and every term t_{i} is different from X_{i}, where 1 ≤ i ≤ n.

Definition 6.3 A unifier for a set of HiLog terms {e_{1},…, e_{k}} is a substitution θ such that e_{1}θ = … = e_{k}θ. A set {e_{1},…, e_{k}} is unifiable if it has a unifier.

Definition 6.4 A unifier σ for a set {e_{1},…, e_{k}} of expressions is most general if and only if for each unifier θ for this set there is a substitution λ such that θ = σλ.

Following [38], we can derive an efficient unification algorithm by solving equations. An equation is of the form t_{1} = t_{2}, where t_{1}, t_{2} are terms. An equation set (possibly empty) is solved if it has the form {X_{1} = t_{1},…, X_{n} = t_{n}} and the X_{i}’s are distinct variables which do not occur in any t_{j} (1 ≤ j ≤ n). Notice that a finite equation set in solved form can be naturally viewed as a substitution.

A solution of the equation set {t_{1} = s_{1},…, t_{n} = s_{n}} is a substitution θ such that t_{i}θ ≡ s_{i}θ (1 ≤ i ≤ n). An equation set is solvable if it has a solution. A solution σ for an equation set E is most general if and only if for each solution θ of E there is a substitution λ such that θ = σλ.

Given a finite equation set, the unification algorithm non-deterministically chooses an equation from the equation set to which it applies one of the following transformations according to the form of the selected equation:

1. For t(t_{1},…, t_{n}) = s(s_{1},…, s_{m}), where n ≠ m, halt with failure.

2. For t(t_{1},…, t_{n}) = s(s_{1},…, s_{n}) replace the equation by t = s, t_{1} = s_{1}, ..., t_{n} = s_{n}.

3. For f = g, delete the equation if f and g are identical parameter symbols in S; otherwise halt with failure.

4. For X = X, where X is a variable, delete the equation.

5. For t = X, where t is not a variable and X is a variable, replace the equation by X = t.

6. For X = t, where X is a variable and t is a term different from X, if X appears in t then halt with failure; otherwise replace X by t wherever it occurs in the equations.

The algorithm terminates when no step can be applied or when failure is reported.

Theorem 6.2 (Unification Theorem) The unification algorithm applied to a finite set of equations E returns a finite set E^{∗} of equations in solved form if and only if E is solvable. It returns failure otherwise. The returned equation set E^{∗} viewed as a substitution is a most general solution of E if E is solvable.

Proof: It is easy to see that for any pair of HiLog terms, s and r, they are unifiable if and only if so are encodet(s) and encodet(r), if and only if encodea(s) and encodea(r) are unifiable. It is also easy to see that the encoding of HiLog in PC transforms the above unification algorithm for HiLog into the corresponding algorithm for PC, described in [38]. The theorem now follows from these two facts. A direct proof can be also obtained as a simple adaptation of the proof in [38]. □

According to the above theorem, HiLog unification is decidable. The reader may wonder about the result reported in [20] where it is shown that unification becomes undecidable once variables are allowed in places where normally only function symbols are permitted to appear. There is no contradiction, however, with our result, for the following reasons. Informally, for a sufficiently rich logic with a higherorder syntax to have a decidable unification problem, two conditions are sufficient. First, the semantics of the logic should be first-order. That is, predicate and function variables should not range over relations or functions. Instead, they must range over intensions or names of predicates and functions, for, as is well known, extensional equality of predicates and functions is undecidable. Second, the logic should not have an undecidable built-in equality theory over names of predicates and functions. HiLog satisfies both conditions by separating intensions from extensions (thereby avoiding extensional unification) and by embodying only a trivial equality theory of intensions. In contrast, Goldfarb [20] essentially works with second-order λ-terms that embody an undecidable equality theory, and this is what makes unification undecidable in this case.

6.4 Refutation

Definition 6.5 If two or more literals of the same polarity (i.e., both positive or both negative) in a clause C have a most general unifier σ, then Cσ is called a factor of C.

Definition 6.6 Let C_{1} ≡ L[t]∨C′_{1}, and C_{2} ≡ (r = s)∨C′_{2} be two clauses with no variables in common, where L[t] is a literal with an occurrence of the term t (including the case when L[t] ≡ t). If t and r have a most general unifier σ, then

Lσ[sσ] ∨ C′_{1}σ ∨ C′_{2}σ

is a binary paramodulant of C_{1} and C_{2}. In this paramodulant, Lσ[sσ] denotes the result of replacing one single occurrence of tσ in Lσ by sσ.

It is important to realize that since L[t] in the above definition may be the same as t, in HiLog one needs to paramodulate not only on the terms occurring strictly inside atomic formulas, as is the case in predicate calculus, but also on atomic formulas themselves. This is an interesting distinction with respect to PC which stems from the fact that HiLog is a higher-order language in which atomic formulas are not distinguished from terms. An example when atomic formulas must be paramodulated upon is presented below.

Definition 6.7 Let C_{1} = L_{1}∨C′_{1} and C_{2} = ¬L_{2}∨C′_{2} be a pair of clauses with no variables in common. If L_{1} and L_{2} have a most general unifier σ, then the clause

C′_{1}σ ∨ C′_{2}σ

is called a binary resolvent of C_{1} and C_{2}.

A deduction of a clause C from a set of clauses S is a finite sequence of clauses D_{1}, ..., D_{n} such that D_{n} = C and for 1 ≤ k ≤ n each D_{k} is either a member of S, a factor of D_{i} (i < k), a paramodulant of some D_{i} and D_{j} (i, j < k), or a binary resolvent of D_{i} and D_{j} (i, j < k). A deduction ending with the empty clause is called a refutation. If C is deducible from S, we write S ⊢ C.

One way to prove the completeness theorem is to adapt the corresponding proof for PC [6]. A shorter proof, however, results from the use of Theorem 3.3:

Theorem 6.3 (Soundness and Completeness of Resolution) A set S of clauses is E-unsatisfiable if and only if there exists a refutation of S ∪ {X = X}.

Proof: Under the encoding of Section 3, given a set of HiLog clauses S, any application of the factorization, paramodulation, or the resolution rules to clauses in S corresponds to an application of the respective rule to encode(S), and vice versa.^{7} Thus, it follows from the analogous result in predicate calculus [6] that the combination of resolution, factorization, and paramodulation is a complete set of inference rules for refuting E-unsatisfiable sets of HiLog clauses.

We also note that if S contains no equality atoms then “E-unsatisfiability” can be replaced by “unsatisfiability” and the axiom X = X would not be needed. □

Consider an example. Recall from Section 3 that the formula

(s(a) = r(b, c)) ⊃ (s(a) ↔ r(b, c))

is valid in HiLog. Therefore its negation should be E-unsatisfiable. The negation of the above formula can be transformed into the following three clauses:

7It is noted that the special treatment of “=” in the definition of encode in Section 3.3 was essential to ensure the above correspondence in case of the paramodulation rule.

(1) s(a) = r(b, c).
(2) s(a) ∨ r(b, c).
(3) ¬s(a) ∨ ¬r(b, c).

By paramodulation, we can derive from (2) and (1)

(4) r(b, c).

and from (3) and (1)

(5) ¬r(b, c).

Then by resolution we can derive the empty clause from (4) and (5), which completes the refutation.

7 HiLog Implementation Issues

A straightforward implementation of a Horn clause logic programming language based on HiLog is possible using the encoding of HiLog into PC, described in Section 3. Since this encoding preserves Horn clauses, we could simply use a standard Prolog compiler to execute the result of such encoding. While this is theoretically sound and may even be practical for prototype programs, for large programs there are some efficiency issues that deserve further consideration. These have to do with fast access to the appropriate clauses at predicate invocation, and efficient representation of data structures. Also, built-in nonlogical predicates, dynamic changes to the database, and control constructs, such as the “cut”, lead to new issues in the HiLog framework.

Consider a simple HiLog Horn clause:

p(X,Y) ← q(X,Z), p(Z,Y).

This clause also happens to be a predicate logic Horn clause. Its encoding in predicate logic is:

call(apply(p,X,Y)) ← call(apply(q,X,Z)), call(apply(p,Z,Y)).

With every clause encoded in this way, each HiLog program, no matter how large, defines exactly one Prolog predicate, call/1. For Prolog-like efficiency, each predicate invocation must locate quickly the clauses whose heads might possibly unify. In Prolog systems, this is achieved first by branching directly to clauses with the same predicate, and then using indexing, normally on the main functor symbol of the first argument, to further refine the search. Notice that for the encoding of a HiLog program, these two ways of refining the search are not very effective; Prolog sees only one predicate, call/1, and the main functors of all those heads are apply/n. Thus the only filtering would come from the arity of “apply”. One approach would be to use partial evaluation techniques to optimize the direct translation [21]. A problem with this approach is how to treat nonlogical constructs, such as “assert”. Another way to improve clause access would be to improve the indexing strategy used by the underlying Prolog system, perhaps as proposed in [49]. An alternative is to constrain the HiLog programs in such a way as to allow simple compile-time optimizations. One way we are exploring is to restrict the clauses to those whose heads have a nonvariable symbol in the leftmost position, that is, clauses whose heads are rigid terms. In this case, all rigid calls in the bodies of clauses can be compiled to branch directly to the appropriate clauses.

Another issue is the representation of HiLog terms. In Prolog, complex terms are normally represented as linked record structures. An n-ary term is represented using n + 1 consecutive words, the first word indicates the functor symbol and the arity, n, and the following n words represent the n arguments. To represent a HiLog term, another arity is required. The most natural way uses n + 2 words: one for the arity, one for (a pointer to) the functor term, and n for the argument terms. While this might seem somewhat wasteful of space, using an entire word for a relatively small arity, we suspect that this will turn out to be the most efficient representation. It is actually a regularization of Prolog’s representation and will make for slightly simpler traversal algorithms.

A realistic logic programming system must support built-ins, which have nonlogical behavior. A decision must be made as to whether these built-ins can be accessed by a most general call. For example, should the query ← X(Y) be able to call the read/1 predicate? The most reasonable choice seems to be to exclude this possibility. A desired separation of built-in predicates from the rest can be achieved by introducing sorts into HiLog, that is, by splitting S and V into disjoint subsets and then proceeding to define HiLog terms of different sorts. Then, “normal” variables will not be instantiatable to symbols that represent built-in predicates. If the user wishes to manipulate such symbols, he would have to use variables of an appropriate sort explicitly.

The issue of the “cut” is also complicated. In Prolog a cut eliminates the alternative clauses remaining for the current predicate. Since in HiLog different calls can access various subsets of clauses, the notion of “predicate” is not so well-defined. These and other issues are explored in more detail in [18].

8 Conclusion: Do We Need Yet Another Logic?

Whenever a new logic is proposed, the question is (and should be) raised as to whether yet another logic is needed. Why not just stay with the logics we know and understand? This is an especially cogent point when the new logic has a simple and reasonably direct translation into the grand-daddy of all logics, first-order predicate calculus, as in our case HiLog does. We believe, however, that in the case of HiLog there are at least three reasons why we should seriously entertain the idea of this new logic as a basis for logic programming.

Firstly, programming in HiLog makes more logic programs logical. We all admonish Prolog programmers to make their programs as pure as possible and to eschew the evils of Prolog’s nonlogical constructs. In Prolog the intermixing of predicate and function symbols, in particular in the predicate, call/1, is nonlogical, whereas in HiLog it is completely logical and is a first-class citizen. So in HiLog programmers need not avoid using call/1, and so have more flexibility in their task of writing pure logic programs.

Secondly, even though one might say that HiLog is simply a syntactic variant of Prolog, syntax is important when one is doing meta-programming. Since in meta-programming the syntax determines the data structures to be manipulated, a simpler syntax means that meta-programs can be much simpler. We saw this in the example of translating DCGs to HiLog, to the extent that a meta-program already written (the DCG translator) would automatically work in a more complicated situation, and so did not need to be changed at all.

Thirdly, and perhaps most importantly, a different logic encourages in the programmer a different way of thinking. Certainly the translation of any HiLog program could be programmed directly in Prolog, but would it be? The DCG example, we believe, shows not. Not only is there an issue of efficiency in that the translation might not execute as efficiently as the programmer desires, but also that the programmer would not even think of that Prolog program. HiLog encourages the programmer to think about and use parameterized predicates; Prolog does not. HiLog programmers would be more likely than Prolog programmers to modularize their programs along the lines suggested in Section 4.2 above. The language influences the way programmers think, and the programs they write.

Finally, we would like to point out that HiLog is not the only logic which can be encoded in predicate calculus. The classic first-order modal logics provide a rich source of examples when a different syntax (motivated by a different philosophy of logic) inspired important and useful studies both in Logic and Artificial Intelligence.

In summary, we believe that HiLog offers significant advantages over Prolog, and deserves serious consideration as the basis for a new logic programming language. Acknowledgments: We are grateful to Thom Fruehwirth, Sanjay Manchanda, Shuky Sagiv, Rodney Topor and James Wu for their comments on the contents of this paper. Especially, we thank James Wu for suggesting the encoding described in Section 3. Suggestions of the referees are also appreciated.

References

[1] Abiteboul, S. and Grumbach, S. [1987] COL: A Logic-Based Language for Complex Objects, in Proc. Workshop on Database Programming Languages, Roscoff, France, September 1987, pp. 253–276.

[2] Abramson, H. [1988] Metarules and an Approach to Conjunction in Definite Clause Translation Grammars: Some Aspects of Grammatical Metaprogramming, in Proceedings of the Fifth International Conference and Symposium on Logic Programming, R.A. Kowalski and K.A. Bowen, eds. Seattle, Washington, August 1988, pp. 233–248.

[3] Apt, K.R., Blair, H. and Walker, A. [1988] Towards a Theory of Declarative Knowledge, in Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 89–148.

[4] Apt, K.R. and Van Emden, M.H. [1982] Contributions to the Theory of Logic Programming, in JACM 29, 841–862.

[5] Beeri, C., Naqvi, S., Shmueli, O. and Tsur, S. [1987] Sets and Negations in a Logic Database Language (LDL), MCC Technical Report, 1987.

[6] Chang, C.L. and Lee, R.C.T. [1973] Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York.

[7] Chen, W. [1987] A Theory of Modules Based on Second-Order Logic, in Proceedings of IEEE 1987 Symposium on Logic Programming, San Francisco, September, pp. 24–33.

[8] Chen, W. [1989] Modules for Logic Programming, Research Report, Department of Computer Science, SUNY at Stony Brook.

[9] Chen, W., Kifer, M. and Warren, D.S. [1989] HiLog as a Platform for Database Language (or why predicate calculus is not enough), 2nd Intl. Workshop on Database Programming Languages, Oregon Coast, OR, June 1989, pp. 315–329.

[10] Chen, W., Kifer, M. and Warren, D.S. [1989] HiLog: A First-Order Semantics of Higher-Order Logic Programming Constructs, in Proceedings of North American Conf. on Logic Programming, 1090–1114.

[11] Chen, W. and Warren, D.S. [1989] C-logic for Complex Objects, in Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 1989, pp. 369–378.

[12] Church, A. [1940] A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, 5, pp. 56–68.

[13] Clocksin, W.F. and Mellish C.S. [1981] Programming in Prolog, Springer Verlag, 1981

[14] Dershowitz, N. and Manna, Z. [1979] Proving Termination with Multiset Orderings, in CACM, Vol. 22, No. 8, 1979.

[15] Enderton, H.B. [1972] A Mathematical Introduction to Logic, Academic Press, Inc.

[16] Fruehwirth, T. [1988] Type Inference by Program Transformation and Partial Evaluation, IEEE Intl. Conf. on Computer Languages, Miami Beach, FL, 1988, pp. 347–355.

[17] Fruehwirth, T. [1989] Polymorphic Type Checking for Prolog in HiLog, 6th Israel Conference on Artificial Intelligence and Computer Vision, Tel Aviv, December 1989.

[18] Fruehwirth, T. and Warren, D.S. [1990] Putting HiLog to Work, manuscript, SUNY Stony Brook

[19] Gelfond, M., Lifschitz, V. [1988] The Stable Model Semantics for Logic Programming, Logic Programming: Proceedings of the Fifth Conference and Symposium, MIT Press, pp. 1070–1080, 1988.

[20] Goldfarb, W.D. [1981] The Undecidability of the Second-Order Unification Problem, Theoretical Computer Science. 13, pp. 225–230.

[21] Smith, D.A., Hickey, T. [1990] private communication.

[22] Henkin, L. [1950] Completeness in the Theory of Types, Journal of Symbolic Logic, 15, 81-91.

[23] Kifer, M. and Lausen, G. [1989] F-Logic: A Higher-Order Language for Reasoning about Objects, Inheritance, and Scheme, ACM SIGMOD Conf. on Management of Data, May 1989, pp. 134–146.

[24] Kifer, M., Lausen, G. and Wu, J. [1990] Logical Foundations of Object-Oriented and Frame-Based Languages, Technical Report 90/14, Department of Computer Science, SUNY at Stony Brook, July 1990.

[25] Kifer, M. and Lozinskii, E.L. [1991] A Logic for Reasoning with Inconsistency, Journal of Automated Reasoning, 1991, to appear.

[26] Kifer, M. and Subrahmanian, V.S. [1989] On th Expressive power of Annotated Logic Programs, North American Conference on Logic Programming, 1069–1089.

[27] Kifer, M. and Wu, J., A Logic for Object-Oriented Logic Programming (Maier’s O-logic Revisited), in Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 1989, 379–393.

[28] Krishnamurthy, R. and Naqvi, S., Towards a Real Horn Clause Language, MCC Report ACA-ST-077-88, Austin, TX, 1988.

[29] Kuper, G., Logic Programming with Sets, in Proc. 6th ACM Conf. on PODS, San Diego, 1987, pp. 11–20.

[30] Kuper, G., An Extension of LPS to Arbitrary Sets, IBM Research Report, 1987.

[31] Kuper, G., Vardi, M.Y., A New Approach to Database Logic, PODS, 1984.

[32] Lassez, J.-L., Maher, M.J. and Marriott, K. [1988] Unification Revisited, in Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, pp. 587–625.

[33] Lifschitz, V. [1988] On the Declarative Semantics of Logic Programs with Negation, in Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 177–192.

[34] Lloyd, J.W. [1987] Foundations of Logic Programming (Second Edition), Springer Verlag.

[35] Maida, A. and Shapiro, S. [1982] Intensional Concepts in Propositional Semantic Networks, Cognitive Science, 6:4 (1982) pp. 291–330.

[36] Maida, A. [1983] Knowing Intensional Individuals, and Reasoning about Knowing Intensional Individuals, in Proc. 8th IJCAI, West Germany, 1983, pp. 382–384.

[37] Maier, D. [1986] A Logic for Objects, in Preprints of Workshop on Foundations of Deductive Database and Logic Programming, ed. Jack Minker, Washington DC, August 1986.

[38] Martelli, A. and Montanari, U. [1982] An Efficient Unification Algorithm, in ACM Trans. on Progr. Lang. and Systems, 4:2 (1982), pp. 258–282.

[39] Meyer, A.R. [1982] What Is a Model of the Lambda Calculus, Information and Control, 52 (1982), pp. 87–122.

[40] Motro, A. [1986] BAROQUE: A Browser for Relational Databases, ACM Trans. on Office Information Systems, 4:2 (1986), pp. 164–181.

[41] Miller, D.A. and Nadathur, G. [1986] Higher-Order Logic Programming, in Proceedings of the Third International Conference on Logic Programming, London, United Kingdom, July 1986, pp. 448–462.

[42] Maier, D., Warren, D.S. [1988] Computing with Logic, Benjamin/Cummings Publ., 1988.

[43] Montague, R. [1973] The Proper Treatment of Quantification in English, in Approaches to Natural Languages, K.J.J. Hintikka, et al., (ed.), Dordrecht, 221–242, 1973.

[44] Nadathur, G. [1987] A Higher-Order Logic as the Basis for Logic Programming, Ph.D. Dissertation, University of Pennsylvania, June 1987.

[45] Naqvi, S., Tsur, S. [1989] A Logical Language for Data and Knowledge Bases, Computer Science Press, Rockville, MD, 1989.

[46] Pereira, F.C.N. and Warren, D.H.D. [1980] Definite Clause Grammars for Language Analysis: A Survey of the Formalism and a Comparison with Augmented Transition Networks, Artificial Intelligence 13, pp. 231-278.

[47] Przymusinski, T.C. [1988] On the Semantics of Stratified Deductive Databases, in Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 193–216.

[48] Przymusinski, T.C. [1989] Every Logic Program has a Natural Stratification and an Iterated Least Fixed Point Model, in Proc. ACM PODS, 1989.

[49] Ramesh R., Ramakrishnan I.V. and D.S. Warren [1990] Automata-Driven Indexing of Prolog Clauses, Proceedings of POPL, January 1990.

[50] Ross, A. [1989] A Procedural Semantics for Well Founded Negation in Logic Programs, in Proc. ACM PODS, 1989.

[51] Ross, A. [1990] On Negation in HiLog, manuscript, 1990.

[52] Van Emden, M.H. and Kowalski, R.A. [1976] The Semantics of Predicate Logic as a Programming Language, in JACM 23, 733–742.

[53] Van Gelder, A. [1989] The Alternating Fixpoint of Logic Programs with Negation, in Proc. ACM PODS, 1989, pp. 1–10.

[54] Van Gelder, A. and Ross, K. and Schlipf, J.S. [1988] Unfounded Sets and Well-Founded Semantics for General Logic Programs, in Proc. ACM PODS, 1988, pp. 221–230.

[55] Warren, D.H.D. [1982] Higher-Order Extensions to Prolog: Are They Needed? Machine Intelligence, 10:441–454.

[56] Warren, D.H.D. [1983] An Abstract Prolog Instruction Set, Report 309, AI Center, SRI International, Menlo Park, CA, October 1983.

[57] Wu, J. [1989] private communication.