The Transformational Approach to Negation in Higher-Order and Type-Theoretic Logic Programming

Languages

Thesis Proposal

Alberto Momigliano Department of Philosophy Carnegie Mellon University 15213 Pittsburgh PA, USA

                         mobile@lcl.cmu.edu

April 12, 1994

1 Introduction

The aim of this thesis is to develop a framework for the synthesis of the negation of (logic) programs in type-theoretic programming languages such as Elf [70] and in general in higher-order logic. This has an immediate practical relevance in programming in those languages, since it relieves the programmer from the burden of explicitly encoding negative information in the form of type families (higher-order clauses). The main point is to avoid resorting to an operational interpretation of negation-as-failure, NF, whose ultimately troublesome semantics is a serious threat to the implementation and verification of the meta-theory of deductive systems, which is one of the ultimate objectives of logical frameworks such as LF [35] or Hereditary Harrop formulae (hhf) [56]. As hinted in the title, the approach that we shall investigate is transformational, started in [79] and refined in [7]. Roughly, given an Elf (hhf) program with occurrences of negated types (predicates), the aim is to derive a new program where the former have been replaced by new positive types (predicates) which correspond to their complement (in a way to be clarified below).

While the topic of negation has been pursued to the extreme in first-order logic programming (we shall try a review in Section 4), the field is almost virgin as far as higher-order logic and type theory is concerned: languages such as λProlog implement NF with the usual cut-fail combination: a logical reconstruction for the first order fragment can be found in Harland’s thesis [32].

Intuitionistic type theories from the simply typed λ-calculus on, say, to Martin-Löf’s Type Theory implement negative types under the Curry-Howard isomorphism as expected, i.e. ¬A ≡ A →⊥, where ⊥ denotes the empty type and DSL is an elimination rule. Thus negative types have no special status, since the emphasis is on functional programs extraction^{1}, rather that giving a search (logic programming-like) operational reading to types.

Under the latter interpretation of dependent function types this would correspond to including explicit negative information in the program. Although this is entirely consistent with the procedural interpretation of function types (hypothetical judgments), it has, beyond the aforementioned obvious disadvantage, some additional ones, as we shall argue next.

Though the impetus of this enterprise may seem at first sight mainly pragmatic, it should not be underrated. In short, we are trying to design a reasonable notion of negation, a basic building block of any logic under severe constraints: to quote from [42]:

1Note that the double negation interpretation has been investigated in the context of computational irrelevance.

“The problem is difficult because it seeks a notion of negation which is simultaneously semantically elegant and computationally feasible: in both execution and mathematical/logical semantics the extended language should cleanly extend the definite clause language”.

The reason why NF is so popular in the logic programming (LP) paradigm is that it essentially requires no modification to the search structure of an LP interpreter. Hence most of the effort is to try and show that it also satisfies the other criteria Lassez et al. pointed out. Nonetheless this is just a part of it: quoting from [20]

“... this notion [NF] is a basic logical notion, a notion of value to pure logic (as studied since the Ancient Greeks) of equal importance and theoretical standing as notion like Possibility, Deduction, Axiom and the like. The role of negation by failure in LP in only a special case: one manifestation of its role in logic”.

Without going overboard, our answer to this plea, will be to show that, paradoxically, the best way to deal with negation in the LP setting (but see 4.8 for more) is to eliminate it through transformation.

Now, let us see more concretely what it means to us; this reduces to the two intertwined questions: why Elf ^{2}? and why adding negation?

1. Elf: its main edge seems to me the easiness to formalize and verify the metatheory of deductive systems: without mentioning the pedagogical value, Martin-Löf’s idea of judgmentsas-types and proof checking as type checking has revolutionized the otherwise painful task of programming proof-checkers. Moreover Elf’s idea of verification of metaproof as programming can be safely (perhaps) compared to Kowalski’s motto (Algorithms = Logic + Control). Also the analogy with the difference between the success of logic programming and the unsatisfactory results of general theorem proving may be enlightening (but I cannot elaborate on that here). There is perhaps a reasonable middle way between Poincare’s derision to the logicist approach:

“If you need 27 steps to prove that one is a natural number, how many will you need for a real theorem?”.

and Wos’ ambition to have solved with OTTER real mathematical open questions (see [94] for a (distressing) list of them).

2. Negation: Elf is one of the purest, hence poorest in terms of programming language features, systems around; of course this is a conscious design decision to achieve the possibility of expressing, verifying and eventually automating the meta-theory of deductive systems. Indeed, every enlargement of the expressive power of the language has to be carefully crafted, in a declarative way (i.e. without spoiling its inductive character), as in the case of refinement types [73] or otherwise expressed as an outside argument (schema-checking [72]). More explicitly, this amounts to show that every extension is conservative on the operational and declarative semantics of Elf. In our case the obligation is to show that the transformation is the identity function on positive signatures and that no new queries involving only positive types can be successful from the transformed program.

An appropriate negation operator may have a rather dramatic effect on the possibility of implementing (i.e. programming) topics that would prove to be too unwieldy to deal with otherwise. Automating the negation of predicates as say typable, well-formed, canonical form etc. will increase the amount of meta-theory that can be checked. Moreover providing negative definitions seems to be particularly error-prone, repetitive and not particularly interesting, thus a good candidate to mechanization. Following this trend a good analogy is the use of higher-order abstract syntax [69]: although it may seem unintuitive at the beginning w.r.t. “named” syntax, it does, notwithstanding the Nuprl group [14], make the difference between being able to master meta-proofs and spending enormous amounts of time in implementing low-level (and tedious) features such as renaming or substitution. To bring this to the extreme, of course, everything can be expressed eventually in first-order logic and ideally proved-checked or even demonstrated by, say, a resolution theorem prover or more likely by an interactive one. In practice, this has turned out to be very problematic, if not a total failure; hence the refinement of the tools to higher-order logic and type-theory. And this is the bottom line: adding another (practically) essential tool to Elf^{3}.

2It may be argued that this is more of relevance to Elf seen as a LP language rather that to LF as a specification metatheory; yet the operational interpretation of LF signatures is independent from the idea of synthesizing negative types: e.g. the specification of LF into LF itself would greatly benefit from that.

This has an analogy with recent developments in the design of “standard” Prolog-like languages; for external reasons, namely, program transformation, there has been a trend in “logicizing” here at a first-order level built-in predicates such as term comparison, arithmetic, metalogical predicates and so on. The limit of this process is perhaps Lloyd’s Gödel language [37] where everything is supposedly declarative^{4}.

Hence the motto seems to be: add features, keep them logical (and constructive, if possible).

The rest of this proposal is organized as follows: Section 2 contains the core of the proposed work: after a brief delineation of an improved version of the transformational approach to firstorder logic programs in [7] (2.2), we describe the bulk of our contribution, namely, extension to

1. Higher-order terms (patterns) (2.4)

2. Implicational goals (2.5)

3. Generic goals (2.6)

In Section 3 we list some related topics that we would like to investigate; in particular the connection with inductive definitions (3.1), the possibility of using regular tree languages to escape some of the known limitations of the method (3.2) and other more general types of higher-order program transformations (3.3). Section 4 tries to situate our work in an historical perspective and lists some of the alternative approaches to negation in LP. Eventually in Section 5 I summarize what appears to me as the essential ingredients of the proposed work and present a potential time frame.

2 Synthesis of Negative Types

2.1 Background

For the sake of this document we assume familiarity with the basic notion and properties of logic programming (classical references are [44] and [4]), hhf and uniform proofs [56], LF and Elf. We shall instead spend a few words on negation (see [5] for a recent survey).

The idea of a proof under the NF (meta)rule is a very natural one: suppose you have a set of axioms and some kind of inference mechanism which produces a recursively enumerable set of theorems, and that you are asked to verify the truth of a negative conjecture ¬C under NF; then you try to prove C from your theory; if you succeed, then ¬C does not hold, while if you realize (in a finite time) that C is not provable, then you are entitled to assert that ¬C holds. NF is a computational approximation to the Closed World Assumption (CWA) [77]. Its basic idea is to state that a goal is false if we are able to prove that it cannot be proved by the program. We answer no to a goal because our attempt to say yes failed, so we say no because we cannot say yes.

Differently from other kind of negation, NF ([20] p. 8)

3Naturally, there is always the problem of enhancing the metalanguage so much that it actually overkills the object level it is trying to specify. Even if the proposed framework is conservative over more manageable systems, we run the risk of having to deal with a overwhelmingly complicated metatheory of the framework for suspicious gains. This is, in my opinion, the case of the usage of framework based on full linear logic, for contexts where the manipulation of resources is not so vital.

4This has very recently allowed the construction of a self-applicable partial evaluator for the whole language.

“ ... does not follow from some constructive knowledge, but from lack of knowledge.”

That motivates two specific features of NF: its inability of finding instantiations for the variables of the goals and its non-monotonicity. In logic programming, NF works this way ([44] p. 87):

“The basic idea is to use SLD-resolution augmented by NF rule. When a positive literal is selected, we use essentially SLD-derivation to derive a new goal. However, when a ground negative literal is selected, the goal answering process is entered recursively in order to try to establish the negative subgoal … Having selected ground negative literal ¬A in some goal, an attempt is made to construct a finitely failed SLDNF tree with root ← A before continuing with the remainder of the computation. If such a tree is constructed, then the subgoal ¬A succeeds. Otherwise, if a SLDNF -refutation is found for ¬A, then the subgoal fails”.

The completion of a program comp(P) [11] is the most well-known way to motivate the usage of NF, which is otherwise unsound w.r.t. the classical notion of logical consequence: when a negative goal succeeds from P, it can be shown to follow from comp(P) (see Section 4 for a refinement of that). Completeness is instead a whole different issue: it can be achieved only for restricted classes of programs or by switching to many-valued models [82], [38]. In this thesis we shall opt for the former alternative and take the notion of completion as the intended meaning of the given program. Briefly it consists of extending the latter with its only-if side (the closure condition in inductive definitions, see 3.1).

Definition 2.1 Let p be a n-ary relation symbol; we assume that it is defined by n clauses whose head has the form p(…) and the i-th clause has n_{i} literals in its body, i.e. has the form

p(t_{i,1} … t_{i,n}) ← L_{i,1} … L_{i,n_{i}}

The completion of p is the following axiom:

∀\overline{x}(p(\overline{x}) ↔ ⋁_{i=1}^{n} ∃\overline{y}(\overline{x} = \overline{t_{i}} ∧ ⋀_{k=1}^{n_{i}} L_{i,k}))

where \overline{x} is an array of n of new variables, whereas \overline{y_{i}} are those appearing in the i-th clause.

Example 1 Consider the usual program for membership in lists:

\begin{matrix}member(X, X.XS). \\ member(X, Y.Y S) ← member(X, Y S). \end{matrix}

Its completion is

∀z, zs(member(z, zs) ↔ ∃x, y, xs, ys, (zs = x.xs ∧ x = z) ∨ (zs = y.ys ∧ y = z ∧ member(x, ys)))

Another ingredient is Clark’s equational theory (CET) [11], which is required to proof-theoretically simulate unification: those axioms force equations introduced by the completion to be interpreted as the identity relation on the domain of interpretation. This (infinite) equational theory, also known as E_{F T}, completely axiomatizes the algebra of finite trees under an infinite signature [38]. When the signature is finite we need an addition to CET in the form of the Domain Closure Axiom (DCA) [50]: for a signature Σ = {f_{1},…, f_{n}} the axiom states:

∀x(⋁_{i=1}^{n} ∃\overline{y}(x = f_{i}(\overline{y})))

This amounts to saying that every model is reachable, i.e. every element is denoted by at least a term construed out of the signature. For the above example it asserts (glossing over typing for the time being – we remedy this in the next section):

∀x(∃y, ys(x = nil ∨ x = y.ys))

Finally, we recall how to express the (relative) complement problem as an elementary equational formula [40] [12]. Let [t] denotes the set of ground instances of a term t. The problem is to compute [t]/[u_{1},…, u_{n}]. Assuming that \overline{z} are the free variables of t disjoint from \overline{y}, i.e. the free variables of u_{1},…, u_{n}, everything boils down to solving:

∃\overline{z}∀\overline{y}(x = t ∧ ⋀_{i=1}^{m} x ≠ u_{i})

2.2 The Transformational Approach in Normal LP

Here we give a brief summary (and a slight improvement) of Barbuti’s approach [7]; see 4.3 for a comparison with others, in particular 4.3.1 for a more close scrutiny of the relationship with Sato’s. This is the starting point since we wish to improve this in several ways, generalizing through what will occur as a natural hierarchy.

Proceeding bottom-up, the first thing is to define a complement operation on terms (Not). Informally an open (left-linear, see below) term can be seen as a representation of the set of its ground instances; hence its complement should represent the set-theoretic complement of such a set. An algorithm for first-order terms is given in [7] which specializes [40]

Standard Prolog is not typed: that means that a straightforward Not operation will produce a lot of irrelevant results (this has some analogy with the proposal in [17]). For example, towards the synthesis of the nonmember operations on list of numerals the result of Not(0) contains not only s(x) as expected, but also nil, 0.nil… This is going to increase exponentially with the size of the signature. A type discipline would solve this problem.

Definition 2.2 Let C be a Church simple typing for a finitary signature Σ. We define Not(t^{τ}) by structural induction, where we assume that t_{i} has type τ_{i}:

Not(x^{τ}) = {}

Not(f(t_{1},…, t_{n})^{τ}) =

\{g(x_{1},…, x_{n})^{τ} | g ∈ Σ, g ≠ f\} ∪ \{f(x_{1},…, x_{i−1}, \overline{t}, x_{i+1},…, x_{n})^{τ} | i ∈ [1, n], \overline{t} ∈ Not(t_{i})^{τ_{i}}\}

Example 2 Given Σ = {0^{nat}, nil^{nlist}, s^{nat→nat}, .^{nat→nlist→nlist}}

Not(s(x).nil) = {nil, 0.nil, y.z.xs}

This corresponds to the solution of the formula

∃z∀x.z = w ∧ z ≠ s(x).nil

At this level of details, the transformation on predicates is better described in words: basically for every clause p(\overline{t}) ← Γ in the predicate definition A, a table of facts nonp(\overline{t}^{c}) is created for \overline{t}^{c} = Not(\overline{t}), plus a new clause derived by the disjunction of the literals in the original body Γ, introducing universal quantifiers for (distinct) local variables. Eventually the “negative” contribution of each clause is merged through unification to yield the new predicate definition (hereafter denoted with nonA). The process is iterated for every predicate occurring negatively in the original program.

The algorithm asks for a specific format in the input program: clauses should be left-linear, i.e. multiple occurrences of the same variable in the head are disallowed, and every local variable must have a single occurrence within a literal in the body; since left-linearization is always possible by introducing unification constraint on the right [87] with a new predicate, say, eq, and localization by introducing new predicates, in this document we shall leave those steps implicit; yet see 3.2 for ways to lift the former restriction on terms. The possibility of this pre-transformation could, nevertheless, be deceiving, since it actually induces a shift from pure Horn LP towards Constraint Logic Programming (CLP) [88] on the Herbrand Universe. A possibility would be to restrict to classes of programs that satisfy the aforementioned conditions; on the other hand, similarly to the case of allowed programs to avoid floundering [81], this fragment is too limited to be of practical utility. Moreover the complement operation takes care of disunification, as explained in more details in (4.3.1). Eventually, a departure from pure Horn logic is unavoidable, as shown in example 4.

Example 3 Given the above program for membership in lists, its negation is synthesized as expected:

\begin{matrix}nonmember(X, nil). \\ nonmember(X, Y.Y S) ← noneq(X, Y), nonmember(X, Y S). \end{matrix}

Note that, even starting with a Horn program, the transformed one may contain universal quantification in the body, stemming from local variables. Consider a program for (irreflexive) transitive closure of a relation:

Example 4

path(X, Y) ← edge(X, Y).
path(X, Y) ← edge(X, Z), path(Z, Y).
edge(a, b).
edge(b, c).

The complement of the program follows:

nonpath(X, Y) ← nonedge(X, Y), ∀Z.nonpath3(X, Y, Z).
nonpath3(X, Y, Z) ← nonedge(X, Z); nonpath(Z, Y).
nonedge(a, a).
nonedge(a, c).
nonedge(b, a).
nonedge(b, b).
nonedge(c, a).
nonedge(c, b).
nonedge(c, c).

This raises two important questions:

1. What is the operational reading of universal quantification in this setting and how it mingles with generic judgments (discussed in 2.6) ?

2. How can this be reflected in the theory of inductive definitions [1] (discussed in 3.1) ?

The soundness and completeness of the transformation w.r.t. the completion of P and (an extension) of SLD-refutation is proved in [7].

Assuming that we have a good understanding of the technique at this level, the real work starts with the extension to hhf/LF.

2.3 Two Words on hhf/LF.

For the sake of simplicity, all the examples in this document will be hhf. Without further ado, we recall the syntax and the operational semantics, where for atoms we assume the usual backchaining rule and A_{r} is a rigid atom:

\begin{matrix}D ::= A_{r}|G ⊃ D|∀xD|D_{1} ∧ D_{2}| \\ G ::= A|G_{1} ∧ G_{2}|G_{1} ∨ G_{2}|∀xG|∃xG|D ⊃ G \end{matrix}

AND: P ⊢ G_{1} ∧ G_{2} only if P ⊢ G_{1} and P ⊢ G_{2} OR: P ⊢ G_{1} ∨ G_{2} only if P ⊢ G_{1} or P ⊢ G_{2} INSTANCE: P ⊢ ∃xG only if there is a term t s.t. P ⊢ [t/x]G AUGMENT: P ⊢ D ⊃ G only if D, P ⊢ G GENERIC: P ⊢ ∀xG only if P ⊢ [a/x]G for a eigenvariable ’a’

At first sight LF (Elf) can be seen as the type-theoretic version of hhf (λProlog) and thus answers suited to the latter could be transferred to the former. Moreover translation of dependent function types into higher-order logic, namely into HOL [24] or hhf [16], have been explored. Unfortunately, these translations use the familiar idea of sending (dependent) types into predicates, similarly as the case of many-sorted into first-order logic, whereas the main idea in the Martin-Löf’s tradition is exactly the opposite, namely squeezing the most of information inside the type discipline. Hence we shall come back to the translation approach (and if any to Felty’s [16], due to its parenthood with Elf) only as a last resort, in case everything else fails. Moreover this entails compiling a carefully orchestrated property as the decidability of type-checking in LF into a undecidable one such as theorem proving. Besides the operational interpretation given respectively in Elf and (λProlog) to Π and ∀ is strikingly different; while the latter is used exclusively to introduce new names, the former, as well known, subsumes function types: this may turn out to be connected to the difference between static and dynamic type families in Elf. Operationally, we are hopeful that most of the techniques developed for Elf would apply to higher-order logic and vice versa. Nevertheless, to minimize risks we shall investigate universal quantification and implication separately.

Finally, we may wonder whether there is a use of NF at the meta-level, i.e. in the formalization of meta-proofs. Although there is plenty of “negative” theorems around of the form “given A there is no B such that...” that are in the scope of systems such as Elf, it is clear that the notion of negation involved is intuitionistic (if not minimal). While it is entirely feasible to incorporate this line of reasoning into the framework, much in the sense of [32], [61], it is unlikely that NF may turn out to be useful at this level; indeed, more than a way of proving, it is a license to assume ¬C, when every attempt to prove C have failed: hence, this concept is relative to a particular inference system in the background, and this cannot exhaust in any way our ability to prove C. For example, the current failure to prove Goldbach’s conjecture does not allow us to assume its falsity. In conclusion NF seems applicable at the level of “proposition-as-types”, rather than “judgments-as-types”.

2.4 Higher-Order Terms (Patterns)

The first extension we shall pursue is higher-order Horn logic: once we succeed in formulating a satisfactory notion of completion, the major point is computing the complement of lambda-terms. In [42] some examples are given regarding functional programs, but the treatment is strictly first-order. Since the (relative) complement problem is an instance of the more general issue of disunification [12], this seems to amount to searching for cases for which higher-order disunification is decidable. Reasoning by analogy, fragments for which unification is tractable are good candidates. The most well-studied one is higher-order patterns [55] which have a unary (and linear) unification problem. Patterns are lambda-terms such that all variables occurring in the scope of a free variable are bound and distinct.

Indeed, unpublished work by Lugiez [49] uses a method of quantifier elimination to achieve disunification of higher-order patterns. An extension to a fragment of second-order lambda-terms is achieved using regular tree languages, yet the linearity constraint is retained.

On the other hand, experience has shown that the undecidability of higher-order (dis)unification is very rarely of practical significance and should not prevent us to try to devise procedure for undecidable fragments. Of course this entails the Elf philosophy of keeping (dis)unification problems as constraints which may not be solved and in the end returned in some normal form.

2.5 Embedded Implication

One of the few extensions to Horn logic that has proved successful is allowing implicational goals. This was mildly started in NProlog [19] and was fully developed in the theory of hhf [56]. The possibility of hypothetical judgments has proven very useful especially to express declaratively the meta-theory of deductive system [74] and it is mandatory to preserve it.

The obvious extension of the transformational approach seems to be working in most cases.

Example 5 Given Σ = {all^{(i→o)→o}, imp^{o→o→o}, and^{o→o→o}}, the following defines the property of being a Horn clause, where we assume suitable predicates for “term”, “atom” and “conjunction”

horn(all(C)) ← ∀x.(term(x) ⊃ horn(C x)).
horn(imp(G, A)) ← atom(A), conjunction(G)
horn(A) ← atom(A).

This yield the following, where some, but not all redundancies (see the last clause) have been eliminated and we presuppose the negation of the other (horn) predicates:

nonhorn(all(C)) ← ∀x.(term(x) ⊃ nonhorn(C x)).
nonhorn(imp(G, A)) ← nonatom(A); nonconjunction(G)
nonhorn(and(A, B)) ← nonatom(and(A, B)).

Unfortunately, this does not seem to be general enough, perhaps depending on the difference between predicates under the Closed vs. Open World Assumption. Namely, predicates occurring negatively in an implication are taken to be open, since they are going to dynamically join the program and thus cannot be completed à la Clark. In the former example “term” is such a predicate. This seems to rule out non-stratified implications in the sense of [3].

Consider the following definition of a predicate which holds if the consequent of an implication directly appears in the antecedent:

Example 6

trivial(A → B) ← trivial(A) ⊃ trivial(B)

It seems that the only thing left is to describe a general technique to eliminate implications. The obvious answer is to introduce a new predicate that keeps assumptions explicit, instead of relying on the interpreter, yielding:

Example 7

trivial(A → B) ← trivial2(A, B)
trivial2(A, A).
trivial2(C, A → B) ← trivial2(C, B); trivial2(A, B).

The proof obligations is as follows:

Theorem 1 Let ϵ be the transformation. Then P ⊢ G iff ϵ(P) ⊢ ϵ(G)

While it is fairly clear how to describe the transformation, the real challenge is to make it efficient, i.e. to use it sparingly and to minimize the amount of explicit assumptions. For nonrecursive predicates it is maybe possible to eliminate implications through an extension of the idea of unfolding [47]. This does not work in general since recursive calls allow self-unfolding.

One way to reduce the amount of predicates which are to be moved in the list of explicit assumptions is to modify the notion of stratification to reflect hypothetical dependencies rather than negative ones.

2.6 Generic Goals

Similarly to implication, several attempts to allow universally quantification in goals in a controlled way were proposed in the mid 80’s (see NQ-Prolog [19], NI [20], clausal intuitionistic logic [53]). They all showed, as far as I am concerned, an amazing amount of technicalities, restrictions, lack of clear operational semantics and mostly the absence of a programming language significance, which is the original sin of all dead languages^{5}.

A possible source of misunderstanding was perhaps the confusion between what we now know as the intensional [56] vs. extensional [7] interpretation of ∀, as well as the implicit assumption of the CWA. More formally:

• Extensional:

∀^{e}x.G holds if for all closed terms t, [t/x]G holds^{6}

• Intensional:

∀^{i}x.G holds if for a parameter a, [a/x]G holds

There is an obvious relation with what we intend the domain of computation to be (recall that in the LP tradition this is central to define the intended term model).

• Closed Domain:

the signature is fixed once and for all as the one underlying the program; this can be enforced by the CWA or an approximation as the DCA.

• Open Domain:

the signature has no restriction; in operational terms this means that it is free to expand during execution by parameters.

This has some relevant model-theoretic consequences that we may not pursue here. At the risk of being trivial we instead give the following:

Example 8 Consider the “program” q(a); the query ∀^{e}x.q(x) follows logically from P + DCA and accordingly succeeds; symmetrically ∀^{i}x.q(x) fails, as it should. Yet take the slighter more complicated program:

\begin{matrix}p(0) \\ ∀x.p(s(x)) \end{matrix}

the query ∀^{e}x.p(x) apparently fails to terminate even it follows logically from P + DCA. ∀^{i}x.q(x) still fails.

Before declaring the intensional approach the obvious winner, let me point out the following

1. It does not seem entirely to be a problem of classical versus constructive logic; the above derivations exists in the minimal predicative calculus with equality and DCA. For finite signatures, it is a question of taste to take DCA as a constructive principle. Infinite ones do not arise because they conflict with the Closed Domain Assumption.

5To alleviate this, I have to mention that the impetus to develop NQ-Prolog was the attempt to formalize the British Nationality Act; yet this hardly qualifies as a development of programming languages feature as for instance λProlog has achieved.

6Note that we only introduce this distinction for goals.

2. The issue of choice of domain is strongly linked to (constructive) negation: going back to the first example above: a query of the type ∃x.¬q(x) succeeds in the Open Domain with answer something like x ≠ a. Moreover, it seems that only reasonable interpretation of universal quantification originating from local variables. Coming back to Example 4, you may check that the intensional version of ∀Z.nonpath(X, Y, Z) makes no sense, while, for instance nonpath(b, X) succeeds with X = b, X = a and nonpath(a, c) fails.

3. Abandoning the problematic generate-and-test approach in [7], extensionality can be refined to proof by case analysis [52] and [32] for fohh. The idea is to use a covering [42], i.e. a finite representation of the underlying signature, on whose members new goals are generated and tested.

Definition 2.3 Given a signature Σ and a type τ hereby declared, a set of terms S = {t_{1},…, t_{n}} is a covering for τ iff for all ground t^{τ} there is i ∈ [1, n] and a substitution θ s.t. t = θt_{i}. A minimal covering set is a covering set such that no proper subset is a covering set. A covering for a signature is a covering for all the declared types.

Example 9 {0, s(y)} is a minimal covering for the signature of numerals, where y is a new free variable.

The soundness of the proof by case analysis (a sort of inversion) can be proven; roughly if a formula is provable from P +CET +DCA for every choice in the covering, then its universalization is provable from the same assumptions.

This has to be extended to higher-order terms, but I do not foresee particular problems.

Of course, proof by case analysis must not be confused with induction^{7}:

Example 10

\begin{matrix}p(0) \\ ∀x.p(s(x)) ← p(x) \end{matrix}

the query ∀^{e}x.p(x) fails, since an inductive step is required.

What about parametricity? It seems that intensional quantification is preserved under the negative transformation, (see the “horn” example) though one would have to keep track of the extension of the signature. There is an obvious tension between OWA and CWA that could turn out to be problematic. Hopefully, we shall use case analysis for ∀^{e} and the GENERIC operation for ∀^{i}.

3 Extensions/Related Topics

3.1 On Inductive Definitions

It is remarkable how much the LP community has ignored the connection between Horn logic and inductive definitions (ID) as codified in [1] (up to [29] [26]and [86]). Most of the (fixpoint) semantics developed in [2] is a literal transliteration of the basic ideas of ID in terms of term models. Namely given an ID P, ID(P) defined as the intersection of all P -closed sets is nothing else than M_{P}, the minimum model of P seen as a set of clauses. Moreover the completion of a program can be seen as syntactic way of enforcing the minimality of ID(P), which now turns out to be the only model (up to isomorphic copies). Similarly the theory of T_{P} is just a transcription of the (monotonic) operator ϕ associated to P. Some of the work on intended models for normal clauses (see Section 4) can be reformulated for non-monotonic ϕ. For instance an extension of the notion of P -closedness leads to the idea of stable models.

Apart from the polemics, what I think can be a interesting problems by itself is:

7Although there is some connection (still to be understood) with the usage of the ω-rule for cut-elimination in arithmetic.

If, given an ID P, its inductive set ID(P) is uniquely determined in some universe U, are there any non-trivial conditions on P or more easily on ϕ such that taking the complement U − ID(P) =_{def} (ID(P)^{C}) yield a dual inductive definition P^{c}, i.e. the complement is an homorphism: ID(P^{c}) = (ID(P)^{C}).

Of course there some trivial answers, as when P is a decidable property in a recursive universe: moreover some remarks in [2] on the convergence among the least and greatest fixpoint of T_{P} may be relevant.

What I find worth investigating are the limits of Horn-definability: for example the complement of the definition of transitive closure is not Horn anymore: hence it should not be in the form of an inductive definition. Yet, from a logic programming point of view the problem seem to depend from the presence of local variables, whose relevance in the theory of ID’s is not clear (to me). Things are going to get nastier once we step to hhf, where, among other things, classical and minimal provability differ, which was not an issue for Horn logic.

It is very likely that the theory of partial inductive definitions [29] (PID) is the right framework. Here (partial) inductive definitions are allowed to be construed by iteration on the arrow in the body of the definition. By analogy, since the closure condition of ID corresponds to the completion of Horn programs, it is possible that a suitable restriction of (finite) PID could provide a semantics for the negative transformation of hhf programs.

As remarked below 4.5, PID are currently being tested as a basis of a programming language which extends languages founded on hhf, but at a very high price in terms of control. More is discussed in 4.5

3.2 Regular Tree Languages

Regular tree languages [21] have been intensively studied and adopted, among others, to provide a type discipline to standard Prolog [59] [95] [15] [36]. Their usefulness lies in the fact that they provide a generalization of regular languages, without losing their nice closure properties. In particular, languages described by non-deterministic grammars are closed under complement: this means that there are algorithms to compute the negation of types described by those languages. It is also known (see [49] for results and references) that sometimes the set of (dis)unifiers of lambdaterms can be seen as a word in a regular language. The move to regular tree languages provides additional decidability results, although the linearity condition, i.e. the disallowance of multiple occurrence of the same variable in terms, is retained.

Indeed this approach can be used to break the chains of left-linearization in terms.

Example 11 Given the usual signature for triples of numerals a representation of {(u, 0, v)}/{(u, 0, u)} is {(s(u), 0, 0), (0, 0, s(u)), (s(u), 0, s(v)) ← (u, 0, v)}.

This can be used to compute the complement of the sum program without requiring the introduction of constraints.

3.3 Program Transformation in Higher-Order Logic Programming

At the best of my knowledge, program transformation of higher-order logic programs has not been investigated per se. The negative transformation as well as the elimination of implications can provide insights for more general questions. Both seem to have strong ties with partial evaluation [47]: this essentially consists of two steps: specialization and unfolding. Without stretching the connection too much, the negative transformation in a sense is a form of specialization since it makes (negative) information explicit that is left implicit in the original program. Moreover the target program may contain redundancies that can be optimized through partial evaluation. As mentioned above elimination of implications can be sometimes achieved via unfolding. Hence a procedure for partial evaluation in higher-order logic programming would be a welcome side-effect of this enterprise. Again the problem is not so trivial, since all three extensions to Horn logic carry some complications. If we do not want to restrict ourselves to patterns, the notion of higher-order uniform proof on which partial evaluation works will have to be extended to take into account possibly infinite unifiers. Similarly there is an obvious problem in pre-evaluating universal goals whose only aim is to introduce new names. The implicational fragment seems the less problematic, since it essentially requires a compile-time version of the deduction theorem.

4 Related Work

The history of LP coincides in a large part with the attempt to extend the expressive power of Horn logic without incurring in computational inefficiencies or declarative nonsense. NF is probably the most common keyword in this paradigm. What is problematic here is well known and let me refer to [4] and [5]. We list the mainstream achievements in the following

Brief Chronology

• 1970 Hill/Kowalski/Kuehner: SLD-resolution

• 1972 Kowalski/Colmerauer: Prolog, with control

• 1976 Kowalski & Van Emden: T_{P} -fix-point semantics = minimum model semantics for Horn logic

• 1977 (Tarnlund) Computational adequacy of definite programs

• 1978 Reiter [77]: Formulation of the CWA

• 1978 Clark [11]: Introduction of NF. Contains

1. the first (unfounded) def. of SLDNF-resolution

2. restriction to safe computation rules

3. notion of completion (no reference to inductive definitions)

4. introduction of the free equational theory and statement (proven in [44] of two crucial lemmata relating it to unification

5. proof-theoretical soundness, i.e. outline of how to transform a SLDNF-refutation in a (classical) derivation somewhere. Shepherdson ([81]) observes it is Intuitionistic, Stärk [84] (and me [61]) that it is actually minimal

6. conjecture of a completeness result for hierarchical (i.e. terminating) programs.

• 1982 [2] Refinement of fix-point semantics to the completion, the actual beginning of the Herbrand semantics frenzy: everybody forgets that T_{P} is just generalized Modus Ponens.

• 1982 [57] First attempt to give a Herbrand semantics to non-Horn programs, known as the Generalized CWA in terms of minimal models: this has been endlessly refined (actually weakened) and ended it up under the label of Disjunctive LP [58]

• 1982 Bowen: first conservative extension of LP to first-order logic, as a sequent calculus + unification

• 1982 IC-Prolog (Clark) Prolog with non-ground computation rule for NF: given ?¬A open, proceeds either if ?A fails or if ?A succeeds without binding the free variables of A, now known as ESLDNF-resolution.

• 1983 [25] Completeness result for NF and Horn logic: if ¬A follows from comp(P) than P ∪ {A} fails finitely.

• 1984 [39] Finite failure semantics for NF, fair rule and connection with greatest fix points of T_{P}.

From now on things tend to become rather unwieldy: we then proceed analyzing trends in parallel.

4.1 Elaboration of the Herbrand Semantics for NF

We heavily borrow from [34], to whom we refer also for references. We start with the canonical model approach, where a particular model is constructed and identified as the meaning of the program, as M_{P} for P Horn.

• Perfect Models (Przymusinski) : minimal under a preference order relation.

• Stable Models (Gelfond). Take interpretation M and P and act as follows: for each non Horn clause C ∈ P and literals ¬A in the body of C:

i. if A ∈ M, delete C ii. else delete ¬A in C

The resulting program P^{∗} is Horn. If M_{P^{∗}} = M, then M is stable. So the construction of the model mimics SLDNFcomputations. Note that stable models need not exist nor be unique.

• Well-Founded Models (van Gelder)

• FixComp Models (Dung): unfold the (instances of the) clauses of P until only negative literals appearing it. Take the completion of it (which may either be infinite or inconsistent).

• Three(Four)-Valued Models (Kunen/Fitting): probably the more reasonable approach (as in [38] [84] and eventually in [88]). Every P has a unique Three-Valued minimum Model.

4.2 Connection to Non-monotonic Logic

The relationship lies in the way in which semantics for non-monotonic logics tend to be in some sense minimal. For instance a model of a circumscription of a predicate q is selected in so far it minimizes the extension of q. Under certain restriction logic programs can be shown to be semantically equivalents to well-known non-monotonic formalisms as circumscriptions, default theories or autoepistemic logic. Again let me refer to [5] for references.

4.3 Constructive Negation

Constructive Negation is an attempt to devise methods capable to provide logically justified answers to non-ground negative queries, in analogy with the witnessing property of constructive logics [91]. Formally, for a suitable derivability relation, this property holds when if ⊢ ∃xp(x) then there is a term t s.t. ⊢ p(t) . Accordingly, it is suggested that from ⊢ ∃x¬p(x) the same property infers a term t s.t. ⊢ ¬p(t). We can roughly distinguish two approaches

i. Program Transformation: [79], [17], [7].

ii. Negation by Constraints: [93] for datalog programs, [9] [10] and extended to CLP in [88]; Fail Substitutions: [83] [51].

Historically, the original attempt to deal with negation was simply to try avoiding the floundering phenomenon: given that the latter is in general undecidable, one possibility is to try to make sure that when a negative literal is called it has already been grounded: there are basically three possibilities:

1. Satisfy the syntactical, though very restrictive, conditions on allowed computations [81], which essentially reduces evaluation to ground evaluation.

2. Try to achieve grounding by delaying as in [M]NU-Prolog or Sicstus, where a goal may be declared to be “frozen” and is evaluated only when it reaches a sufficient degree of instantiation. This is obviously only a partial solution, since at run-time there is no guarantee to eventually ground the problematic query. A further improvement is offered by the computation rules of IC-Prolog (see [67], for a comprehensive analysis and references).

3. Covering the open negative query with a generator of values for the relevant variables.

4.3.1 Static Approaches

If we are dealing with datalog programs, i.e. with finite Herbrand Universe U_{P}, the naive approach would be to instantiate all the rules with potentially troublesome goal with terms from U_{P} [3], say through propagation in every negative literal in the program. This is clearly infeasible, since it may result in an intractable numbers of rules, proportional to all the permutation of arguments over U_{P}; besides, this may return many undesired (untypable) answers.

A sophistication of this idea can be found in [17]: the proposal is to automatically infer a ‘type’ for the problematic variables and transform the original program into one where grounding is ensured by coverage from those types. Then useless answers originating from general instantiation would be excluded by the typing discipline. The idea is therefore to transform the program into a typed one, where a type is a set of facts, say t(q, j, c), where q is a predicate name of arity n, j ranges over the natural numbers and c is in U_{P}. Although it can be shown that the new program is equivalent to the old one, this cannot be extended to full Prolog: function symbols make the type infinite and non-ground facts would undermine the instantiation capability of the type. What is required is a generator for infinite U_{P}, instead of a table of facts.

The transformational approach has a fairly long history – see [67],for a survey of the early 80’s. The idea is to implement negation using inequalities, so that the negation of any predicate occurring negatively in the original program P is synthesized so as to obtain an equivalent definite program P^{c} (in the sense of F_{P} = M_{P^{c}}). This was first proposed in [79]. In this seminal paper it is shown how to massage the completion so that the derived program mimics failed computation of the original one. The technique consists essentially in taking the contrapositive of the completion, putting the RHS in dnf and eliminating the universal quantified inequalities by introducing a ‘nonunifiable’ predicate. From the simplification of those constraints and by regarding the negated predicate as a new name and through the many-sorted discipline the new definition is obtained.

Two interrelated problems are involved in this simple transformation:

1. We need an explicit way to solve the aforementioned inequalities: this was first suggested in [40] in the general context of explicit representation of generalization and refined in [42]; there it is shown that the uncover algorithm may simplify those constraints into canonical forms but also that this elimination is not achievable in general. Another version, specifically calibrated to the negation issue in its being incremental is given in [32].

2. The presence of local variables, i.e. variables that appear in the body but not in the head is problematic, as they turnout to be universally quantified.

There have been several partial solution to the above problem: [79] proposes to use a more general fold/unfold transformation system. In [7] instead it is proposed to compute the set-theoretic complement of the terms in the negative predicate compiling away the inequalities.

In the light of the analysis in [42], it is worthwhile to compare the two approaches:

1. Sato/Tamaki:

• locally stratified many-sorted programs

• no local variables

• may be non-left linear

• no explicit mechanism to handle inequalities

• sketch of proof of F_{P} = M_{P^{c}}

2. Barbuti and co.

• left-linear non-stratified programs with no shared local variable in the body, thus reducing the complexity of extensional universal quantification (see below).

• local variables yield non-Horn programs with extensional universal quantification

• left linearization reintroduces inequalities motivating the move to CLP in [43]

• operational interpretation of ∀

Hence the following, where SS_{P} is the success set of P:

Theorem 2 Let β and σ respectively Barbuti’s and Sato’s transformations, and P be left-linear: then SS_{β(P)} = SS_{σ(P)}

The main idea (actually a lemma) is as follows: by Theorem 5 in [42] the substitution formulae in σ(P) have a finite representation that can be computed by uncover; analogously the latter computes the complement of terms in β(P) with the same result.

This should carry over to the general case: left-linearization in σ(P) produces inequalities which by the same theorem are not eliminable and are equivalent to the canonical forms of those coming from β(P).

4.3.2 Dynamic Approaches

Chan [9] is acknowledged to be the inventor of the term ’constructive’ negation; his approach can be roughly characterized as a mix of NF with a constraints-solving attitude. In essence it consists in taking a negative goal, calling the positive version and negating the answer obtained. As in the CLP family of languages, unification and disunification are kept explicit and returned as solutions. The key observation is that if G is a goal and A_{1}, ..., A_{n} the answer substitutions (treated as atoms), G ↔ A_{1} ∨… ∨ A_{n} is a logical consequence of the completed database. Therefore the constructive negation rule is simply ¬G ↔ ¬(A_{1} ∨… ∨ A_{n}), i. e. the answer to ¬G is the negation of answers to G. Of course, there is some work to do in keeping the (in)equalities tidy (normalized answers) and there are some obvious problems when dealing with computations that have infinite answers, fixed in [10], by quantifying over the answer substitutions. No proof of completeness is offered. A generalization to constraint logic programming over arbitrary structures is offered in [88]; it turns out to be sound and complete w.r.t. the three-valued models of the completion.

(E)SLDNF −S ([83]) The finite failure case in the definition of SLDNF -resolution is modified as follows: given the goal ?(Γ, ¬A), then it has a child ?θΓ, if there is a finitely failed-tree for ?θA, where dom(θ) ∈ vars(A). So NF instantiates under success, i.e. negative goals directly return substitutions: given P and G the aim is to look for a (fail) substitution θ s. t. P ∪ {θG} has a finitely failed tree; then by the soundness of the NF rule ∀θ¬G is a consequence of comp(P) and thus θ is an a.s. for the query ?¬G. This seems very costly, since it entails enumerating (guessing) every fail substitution.

This is refined in [51], where it is shown how to avoid to generate all possible substitutions in lieu of a maximal general fail substitution. Moreover, the improvement w.r.t. Chan’s work lies in the feature of always including some positive bindings for the variable in the negated goal. If the SLD-tree is infinite, the method, similarly to what dappwna eo - as enumerates the set of fail substitutions; this corresponds to the fact that in general negative queries cannot be represented by finite positive information alone (connected to [41]). Note anyway that (E)SLDNF − S turns out to be complete for a three-valued possible world semantics of comp(P).

4.4 Non-Failure Driven Negation

During the years ways of incorporating other more logical forms of negation than NF have appeared. Since most of the time this gives back full non clausal-logic, most of them are catalogued as ATP’s. In all these accounts, negative information has to be provided explicitly and specific rules are offered to deal with that. Sometimes it is possible to mix OWA and CWA predicates safely. For a more detailed account and bibliography, let us refer to [61].

• N(Q)Prolog [19] and Negation as Inconsistency ([19]): the former is a complete implementation of positive intuitionistic logic. By defining disjunction classically and allowing a restart rule, Gabbay shows it to be complete for full classical logic as well. The latter evaluates a query against an ordered pair ⟨P, N⟩, where P is a Horn program and N a set of queries that are required not to succeed; this is logically equivalent to adding to the program the negation of all the members of N, and permits importing negative facts and rules. Both systems have a very awkward first-order version.

• Stickel’s P T T P, supplementing SLD-resolution with the model elimination rule. This entails keeping track of the ancestors of the goal, loosing one of the key feature of Prolog, namely input resolution. Moreover, due to the directionality of SLD-resolution it requires the inclusion of the contrapositives of the clauses, causing a notable increase in the size of the theory.

• Loveland’s nHP rolog incorporating case analysis in SLD-resolution demands each time the invocation of a restart rule, until the stack of unsolved (disjunctive) heads is empty. Without requiring contrapositives it simulates case analysis with different runs of essentially the Prolog engine. Unfortunately naive nH-Prolog is incomplete and the new versions (Progressive nH and Inheritance nH) have a less natural and convincing description.

• Plaisted [75] instead is concerned with a difficult attempt to use sequent-based logic programming with a version of the cut rule which operates backwards leading to a problematic guessing of its premises. For a comparison, see [76].

• Another close relative goes under the name of disjunctive logic programming (see [58] and references therein). It aims to deal with full clausal logic by extending the machinery for Horn Logic. In particular the procedural semantic, called SLO-resolution, extends the SLD-step by having the selection function choose a clause in the current goal (a sequence of clauses) and trying to find a clause whose head subsumes it; if successful, the goal is incremented by the body, without deleting the selected clause.

4.5 Proof-Theoretic Approaches to Negation and NF

Lately we have participated in an attempt to tie LP to proof-theory, where it belongs: and this has brought new insights, particularly on NF.

The first step is to view Horn clauses positively as rules and goals as existentially closed conjunctions of atoms to be proved by the former. Historically this can probably be dated back to Gabbay and Reyle [19]. We can distinguish among two approaches:

1. Clauses as axioms (programs as theories) and some form of Gentzen sequent calculus to infer goals, as it is very clearly expressed in a series of papers by Miller et al. [56]. This approach is also motivated by the enlarged language in consideration (hhf), where every connective and quantifier is allowed by the syntax, though not arbitrarily.

2. Clauses as rules [30]: Horn (and beyond) programs should be seen as set of inference rules for the derivation of (not necessarily ground) atoms. This view is coherent with the idea of programs defining a continuos mapping on the lattice of Herbrand interpretations: then logic programs can be seen as inductive definitions of such interpretations. A formal system C(P) is associated to a program P consisting of rules. They define a specialized calculus, called linear derivation, which proves pairs of the form ⟨G, θ⟩, and demonstrate it to be sound and complete w.r.t. C(P). A linear derivation is essentially a SLD-derivation upside-down, in a structure-sharing, forward chaining style, i.e. where substitutions are split from goals. Moreover, Elf itself [70] can be seen under this perspective.

This has the following relation with negation:

1. Minimal, intuitionistic and classical negation can be superimposed over Uniform Proofs [54], [32], [61]: Minimal negation, being camouflaged implication, is executed through the AUGMENT/backchain operation ; the evaluation of ¬D consists in the assumption of D and in the attempt to prove ⊥ from the enlarged theory. The Duns Scoto Law and Reductio ad Absurdum for atoms formalize the latter, preserving the feature of abstract logic programming languages [56].

2. GCLA [6] is based on the rule-based definitional approach to LP: it has intuitionistic negation built-in, originating when the definiens operator D returns an empty set of atoms. The calculus D(P) [31] is obtained by adding a definitional rule to C(P) (see [6] for a richer set of rules and the programming language GCLA based on them). Note that although G is derived in D(P) using (P ⊢), the former may not be a logical consequence of the program, nor of any standard extension known in the literature like comp(P) or CW A(P). Indeed the system does not need a logical language at all and has, as a semantics, the theory of partial inductive definitions [29]. The only relationship with NF of which I am aware of the possibility of showing the containment of the SLDNF -resolution into D(P), under the proviso of A-sufficiency. Let me refer to [63] for more details and the proof.

W.r.t. negation-as-failure Stärk [84] has given a sequent calculus NF (P) consisting of

• Clark’s equality and freeness axioms

• Negation rules (see below ¬ − R)

• cut rules, where Σ is a set of equations and Γ of literals.

Σ ⊢ s = t , s = t, Γ ⊢ Δ Σ, Γ ⊢ Δ  Σ ⊢ A , A, Γ ⊢ Σ, Γ ⊢

• Program rules from P, divided into positive and negative introduction. For example, given the non-stratified program for even we have:

Σ ⊢ t = 0 Σ ⊢ even(t)  Σ ⊢ t = s(X) Σ ⊢ ¬even(X) Σ ⊢ even(t)

{t = 0, Γ ⊢ t = s(X), ¬even(X), Γ ⊢ \atop even(t), Γ ⊢}

Much more is however contained in Stärk’s thesis; to quote a few, he shows that a sequent is provable in NF (P) iff it is true in all 3-valued model of the completion. Furthermore a completeness result is proved w.r.t SLDNF - resolution for program satisfying the cut-property [85].

4.6 NF in Intuitionistic Logic Programming

Recently there has been some interest in combining NF with what is known as intuitionistic logic programming [8] [23] [68]. Unfortunately, the underlying languages are either version of N-Prolog or clausal intuitionistic logic. Due to the inherently difficulty with universal quantification mentioned in 4.4, the treatment is either propositional or deprived of generic goals. Moreover the emphasis is on Kunen’s semantics and/or Gabbay’s modal interpretation of NF into G, the modal logic of Peano arithmetic, another facet of negation in logic programming that we cannot pursue here.

Harland [34] instead proposes a sequent calculus based on intuitionisic logic that directly incorporates NF without referring to the completion. The usual rules, restricted to deal with Horn logic, induce a positive derivability relation; furthermore, he introduces a negative system of disprovability, denoted by ⊢^{−} with judgments of the type: if a conjunction fails then so does one of the conjuncts and so forth. The two systems are interlinked by the rules for NF.

Γ ⊢^{−} F (¬ − R+) Γ ⊢ ¬F  Γ ⊢ F  (¬ − R−) Γ ⊢^{−} ¬F

Structural rules have a paramount importance in this calculus: due to the nonmonotonic nature of NF, weakening in the positive fragment is restricted to introduce only already provable formulae on the left, resulting in a dual to contraction. In the negative system structural rules, cut included, are not eliminable. This is not strictly a calculus of finite failure, since sequents of the form p ← p ⊢^{−} p are provable, although with the essential use of weakening. Of course, due to the recursion-theoretic complexity of unprovability, every such an axiomatic formulation is bound to be incomplete. Moreover the boundary seems fuzzy, as, for example, p is independent from the program p ← q, q ← p. The calculus without structural rules is shown [32] to be sound and complete w.r.t. finite failure and SLDNF -resolution (extended to first-order hereditary Harrop formulae). Having to model the operational behavior of NF, both the positive and the negative system make explicit references to unification, Skolem functions and so forth. Still, the system is not meant for proof search and requires a relative complement algorithm to provide answers to open negative queries.

Harland’s thesis [32] is an in-depth analysis of Uniform Proofs and NF at the first-order level. Distinguishing between CWA and OWA predicates, NF makes sense only for the formers, since they exclude everything else, while the latter srequires some form of real (say minimal) negation, much as in [62]. The distinction is enforced by user declarations.

Eventually, he shows how to formulate the completion as an object fohh formulae so as to simulate NF as derivability in the uniform proof system. This entails giving a completion procedure for fohh clauses; note that only CWA predicates are completed. Programs are assumed to be locally stratified, hence the completion is consistent. An equality/inequality solver on U_{P} is described. The executable completion is formulated through contraposition, much as in my thesis [62], though in a more detailed and convoluted way. A completeness result is proven w.r.t. failure, which is conservative over Horn clauses; the treatment of implicational goals is somehow ad hoc.

4.7 My Previous Work

It is worthwhile to review very briefly my past work on the subject: [60] is essentially an expository survey of NF from the usual semantic point of view. In [61] and more fully developed in [62] negation in the context of fohh is investigated much (though independently) in the sense of [34]. In [63] a proof-theoretic approach to LP based on the notion of axiom-application rule and regularity is developed. This is refined and applied to constructive negation in [64] through the idea of regular splitting, a manipulation of the completion so as to achieve the same properties of SLD-resolution.

4.8 Complement Problems and Elimination of Negation in Term Algebrae

Complement problems and elimination of negation are not restricted to LP, but has some other relevant application in computer science. Actually the more general question of disunification has become a fast growing field in its own which is impossible to summarize here. Extension of disunification in order-sorted signatures is under research as well as in the presence of equational theories, inequalities (≤) and symbolic constraints. Let me refer to [42] and [12] for more details and references.

More specifically, complement problems and variants of the uncover algorithm have been used in several ways:

• To determine whether the definition of a function by pattern matching in functional programming is exhaustive and disjunct and to take into account the assumed sequential application of the rules for compilation.

• Its connection with the notion of ground reducibility in term rewriting makes it a candidate to check whether an algebraic (equational) specification is sufficiently complete.

• In term rewriting systems describing infinite transition systems, the complement of LHS returns the states from which no transition is achievable, giving thus a tool for the temporal analysis of communicating processes.

• Applications to inductive theorem proving have also been investigated.

5 Thesis Outline

The fundamental ingredients are as follows

• Sato-Barbuti’s synthesis technique for the complement of first-order logic programs

• Harland’s notion of completion for fohh

• Lassez-Lugiez’s disunification technique for handling inequalities stemming from the completion.

What’s left to do is mix them together and lift it to hhf/LF and voila’! More seriously, an ideal approach goes like this: the transformational approach is rooted in the notion of completion for Horn logic. Its extension to higher-order Horn logic and LF’s Horn fragment has not been investigated so far and may turn out to be an interesting subject in its own. In particular, we need to understand the higher-order version of CET and the DCA and their connection with the induction principle and the algebra of higher-order terms. This is not only vital to give a semantics to a suitably generalization of the idea of proof by cases to the higher-order case, but it also seems to recur in other sectors of Elf theory (i.e. open vs. closed terms and the (im)possibility of implementing metaproofs such as strong normalization (cut-elimination) for PA which are not formalizable in first-order arithmetic).

Once this has been accomplished, Lugiez’s disunification technique should give us a first approximation to negating L_{λ} programs [55]. To deal with full higher-order Horn clauses we still need to analyze the use of regular term languages to incorporate non-patterns. Moreover we have to be aware that perhaps the best choice to deal with non non-left linear programs is to switch to an explicit CLP, which is also onsistent with Elf approach to unification.

It is entirely possible that already at this level we may have to restrict ourselves to certain (hopefully syntactically defined) classes of programs to achieve first a sensible behavior and eventually completeness. Note that the latter is a front-line research topic [5], where wider and wider classes of programs are explored. Nonetheless, given the emphasis on practicality of this thesis, we shall probably have to restrict to narrower, more understood fragments that make sense in the higher-order setting.

Next, following Harland’s notion of completion for fohh, we ought to re-introduce intensional quantification and embedded implication in the picture. As already mentioned, this in turn leads to several questions:

1. The interaction between intensional and extensional quantification and the related assumptions on the domain of computation is very delicate and has not been adequately investigated. Moreover, its extension to LF’s Π operator is still shrouded in mystery.

2. Non-stratified implications may have to be eliminated in a judicious way, or at least brought to some sort of normal form to be dealt with by the proposed approach.

Eventually (and ideally) we would like to come up with a broad, neatly defined and useful class of higher-order programs amenable to the transformational idea and at the same time shed some light on the notion of negation-as-failure in the higher-order setting.

Time Plan:

1. Higher-order terms (patterns): 4 months

2. Implicational goals: 4 months

3. Generic goals: 4 months

4. Write-up: 3 months

Exploring related topics and/or an implementation could add 6 – 9 additional months.

References

[1] Aczel A. An Introduction to Inductive Definitions. In Handbook of Mathematical Logic, Barwise J. (ed.), North-Holland, 1977.

[2] Apt K.A. & Van Emden M.H. Contributions to the Theory of Logic Programming. JACM, vol. 29, no. 3, pp. 841 - 862, 1982.

[3] Apt K.A., Blair H. A. & Walker A. Towards a Theory of Declarative Knowledge. In: Foundations of Deductive Databases and Logic Programming, Minker J. (ed.), pp. 89 - 148, Morgan Kaufmann, 1988.

[4] Apt K.A. Logic Programming, Handbook of Theoretical Computer Science, Leuween J. (ed.), Elsevier, 1990.

[5] Apt K.A. & Bol R. Logic Programming and Negation: A Survey. To appear.

[6] Aronson M. , Eriksson L-H. , HallnßL. & Kreuger P. A Survey of GCLA: a Definitional Approach to Logic Programming. In: Extensions of Logic Programming, Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.

[7] Barbuti R., Mancarella P., Pedreschi D. & Turini F. A Transformational Approach to Negation in Logic Programming. Journal of Logic Programming, pp. 201-228, 1990.

[8] Bonner A. J. & McCarthy L. T. Adding NF to Intuitionistic Logic Programmninhg. NACLP92, pp. 681 – 73, MIT Press 1990. Proc

[9] Chan D. Constructive Negation Based on the Completed Database. In : Proc. 5th Conf. Logic Programming, Kowalski B. & Bowen K. (eds.), pp. 111 - 125, 1988.

[10] Chan D. An Extension of Constructive Negation and its Application in Coroutining. In: Proc. North American Conf. on Logic Programming, pp. 477 - 493, 1989.

[11] Clark K.L. Negation as Failure. In: Logic and Data Bases, Gallaire H. & Minker J. (eds.), Plenum Press, New York, pp. 293-322, 1978.

[12] Comon H. Disunification: A Survey. In: Computational Logic, Lassez & Plotkin (eds.), MIT Press 1991.

[13] Comon H. Elimination of Negation in Equational Theories. Technical Report, Paris-Sud, 1993.

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

[15] Dart P.W. & Zobel J. A Regular Type Language for Logic Programs. In Types in Logic Programming, Pfenning F. (ed.), pp. 157 - 187, MIT Press, 1992.

[16] Felty A. Encoding Dependent Types in an Intuitionistic Logic. in: Logical Frameworks, Huet & Plotkin (eds.), Cambridge University Press, pp. 215 - 251, 1991.

[17] Foo N, Rao A., Taylor A. & Walker A. Deduced Relevant Types and Constructive Negation. Proc. 5th Conf. Logic Programming, Kowalski B. & Bowen K. (eds.), pp.126 - 139, 1988.

[18] Gabbay D. M. Modal Provability Interpretations of NF. In: Extensions of Logic Programming, Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.

[19] Gabbay D. M. & Reyle U. N-Prolog: an Extension of Prolog with Hypothetical Implications: 1. Journal of Logic Programming, 4, pp. 319 - 355, 1984

[20] Gabbay D. & Sergot M. Negations as Inconsistency: I. Journal of Logic Programming, pp. 1 - 36, 1986.

[21] Gecseg F. & Steinby M. Tree Automata. Akademiai Kiado, Budapest, 1984.

[22] Ginsberg M L. Negative Subgoals with Free Variables, Journal of Logic Programming,11, pp. 271 - 293, 1991.

[23] Giordano L. & Olivetti N. NF in Intuitionistic Logic Programming. In Apt K. (Ed.), JCSLP92, pp. 431 – 445, MIT Press 1992.

[24] Jacobs B. & Melham T. Translating Dependant Type Theory into Higher-Order Logic. In: Typed λ-Calculi and Applications, Bezem & Groote (eds.), pp. 209 - 229, Springer- Verlag, 1993.

[25] Jaffar J., Lassez J-L. & Lloyd J.W. Completeness of the Negation as Failure Rule. In: IJCAI-83, Karlsurhe, pp. 500 - 506, 1983.

[26] Jäger G. Between Constructive Mathematics and PROLOG. Arch Math. Logic, 30:297-310, 1991.

[27] Jäger G. Some Proof-Theoretic Aspects of Logic Programming. In: H. Schwichtenberg (ed.) Algebra And Logic of Specification, Springer-Verlag, Berlin 1993.

[28] Johansonn I. Der Minimal Kalkł, ein Reduzierter Intuitionistischer Formalismus, Compositio Mathematica, vol. 4, pp. 119 - 136, 1936.

[29] Hallnäs L. Partial Inductive Definitions. Theoretical Computer Science, v. 87 no. 1, pp. 115 - 147, 1991.

[30] Hallnäs L. & Schroeder-Heister P. A Proof-Theoretic Approach to Logic Programming: Clauses as Rules. Journal of Logic and Computation, v.1 no. 2. pp. 261 - 283, 1990.

[31] Hallnäs L. & Schroeder-Heister P. A Proof-Theoretic Approach to Logic Programming: Programs as Definitions. Journal of Logic and Computation, v.1 no. 5. pp. 635 - 660,1991.

[32] Harland J. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD Thesis, Edinburgh 1991.

[33] Harland J. A Clausal Form of the Completion of Logic Programs, ICLP′91, pp. 711 - 725, 1991.

[34] Harland J. Towards a Static Proof System for Negation as Failure. Citri/TR-92-49, University of Melburne, 1992.

[35] Harper R., Honsell F. & Plotkin G. A Framework for Defining Logics. JACM, 40(1):143–184, 1993.

[36] Heintze N. & Jaffar J. Semantic Types for Logic Programs. In Types in Logic Programming, Pfenning F. (ed.), pp. 141 - 156, MIT Press, 1992.

[37] P.M. Hill and J.W. Lloyd. The Gödel Programming Language, MIT Press, 1994.

[38] Kunen K. Negation in Logic Programming. Journal of Logic Programming, 4, pp. 289-308, 1987.

[39] Lassez J.-L. & Maher M J. Closure and Fairness in the Semantics of Logic Programming, T CS, 29:167 - 184 1984.

[40] Lassez J-L. & Marriot K. Explicit Representation of Terms Defined by Counter Examples. Journal of Automated Reasoning, pp. 301-317, 1987.

[41] Lassez J-L., Maher M.J. & Marriot K. Unification Revisited. In: Foundations of Deductive Databases and Logic Programming. Minker J. (ed.), Morgan Kaufmann, pp. 587 -626, 1988.

[42] Lassez J-L., Maher M.J. & Marriot K. Elimination of Negation in Term Algebras. In: Mathematical Foundations of Computer Science. Tarlecki A. (ed.), Springer-Verlag, pp. 1 - 16, 1991.

[43] Levi F. Constructive Negation and Universal Quantification. M.S. Thesis, Universita’ di Pisa, 1992.

[44] Lloyd J.W. Foundations of Logic Programming. Second Extended Edition, Springer-Verlag, Berlin, 1987.

[45] Lloyd J.W. & Topor R.W. Making Prolog more Expressive. Journal of Logic Programming, 1, 3, pp. 225 - 240.

[46] Lloyd J.W. & Topor R. W. A Basis for Deductive Database Systems I and II. Journal of Logic Programming, 2, 2, pp. 93 - 109, 3, 1, pp. 56 - 67.

[47] Lloyd J.W. & Shepherdson J. Partial Evaluation In Logic Programming, Journal of Logic Programming, v.11, pp. 217 - 242, 1991.

[48] Loveland D. Near-Horn Prolog and Beyond, Technical Report CS-1988-25, Duke University, 1988.

[49] Lugiez D. Higher-Order Disunfication: Some Decidable Cases. Manuscript.

[50] Maher M. J. Complete Axiomatization of the Algebras of Finite, Rational and Infinite Trees. In: LICS’88, pp. 348 – 357, 1988.

[51] Maluzinski J. & Naslund T. Fail Substitutions for Negation as Failure. Proceedings of NACLP ’89, Lusk & Overbeek (eds.), MIT Press, pp. 461 - 476, 1989.

[52] Mancarella P. , Martini S. & Pedreschi D. Complete Logic Programs with Domain Closure Axiom. Journal of Logic Programming, 5, pp. 263 - 276, 1988.

[53] McCarty L. F. Fixed Point Semantics and Tableau Proof Procedures for a Clausal Intuitionistic Logic, Technical Report LRP-TR-18, Rutgers,1986.

[54] Miller D. A Logical Analysis of Modules in Logic Programming. Journal of Logic Programming, pp. 79 - 108, 1989.

[55] Miller D. A Logical Programming Language with Lambda-Abstraction, Function Variables and Simple Unification. In: Schroder-Heister P. (ed.) Extensions of Logic Programming, LNAI 475, Springer-Verlag, pp. 253 – 281, 1991.

[56] Miller D., Nadathur G., Pfenning F., Scedrov A. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic, 51, pp. 125-157, 1991.

[57] Minker J. On Indefinite Data Bases and the Closed World Assumption. Proc. 6th Conf. Automated Deduction, LNCS 138, Springer-Verlag, Berlin, 1982.

[58] Minker J., Rajasekar A. & Lobo J. A Theory of Disjunctive Logic Programs, in: Computational Logic, Lassez J.L. & Plotkin G. (eds.), MIT Press, 1991.

[59] Mishra P. Towards a Theory of Types in Prolog. In: Proc. of the 1984 Symposium on Logic Programming, pp. 289 – 298, 1984.

[60] Momigliano A. Prolog and Negation, M. S. Thesis, Computing Laboratory, Department of Mathematics, Oxford University, 1989.

[61] Momigliano A. Hereditary Harrop Formulae and Minimal Negation, in: Logic Foundations of Computer Science, Nerode A. (ed.) LNCS no. 676, Springler-Verlag, 1992.

[62] Momigliano A. Some Remarks on Uniform Proofs and Constructive Negation , M. S. Thesis, Department of Philosophy, Carnegie Mellon University, 1993.

[63] Momigliano A. & Ornaghi M. Regular Search Spaces as a Foundation of Logic Programming. In: Extensions of Logic Programming, Dyckhoff R. (ed.), LNAI no. 425, Springler-Verlag, 1994.

[64] Momigliano A. & Ornaghi M. Constructive Negation via Regular Splitting. Manuscript.

[65] Murthy C. Classical Logic as a Programming Language: Typing Nonlocal Control, submitted, 1993.

[66] Nadathur G. A Proof Procedure for the Logic of Hereditary Harrop Formulas, Journal of Automated Reasoning, 11, pp. 115-145, 1993.

[67] Naish L. Negation and Control in Prolog. LNCS no. 239, Springer-Verlag, 1985.

[68] Olivetti N. & Terracini L. N-Prolog and the Equivalence of Logic Program. I. Logic Language and Information, pp. 253 - 339, 1992.

[69] Pfenning F. & Elliot C. Higher-Order Abstrct Syntax, in: Proc. of SIGPLAN’88, ACM Press, pp. 537 - 551, 1988.

[70] Pfenning F. Logic Programming in the LF Logical Framework, in: Logical Frameworks, Huet & Plotkin (eds.) pp. 149-182, Cambridge University Press 1991.

[71] Pfenning F. Unification and Anti-Unification in the Calculus of Constructions. Proceedings of the IEEE Symposium on Logic in Computer Science, 1991, pp. 74-85, 1991.

[72] Pfenning F. & Rohwedder E. Implementing the Metatheory of Deductive Systems. In CADE-11, Kapur (ed.), LNAI, Springer-Verlag, pp. 537 - 551, 1992.

[73] Pfenning F. Refinement Types for Logical Frameworks. In: Geuvers H. (ed.) Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, University of Nijmegen, pp. 285–299, 1993.

[74] Pfenning F. Computation and Deduction, Manuscript 199?.

[75] Plaisted D.A. Non Horn Logic Programming without Contrapositives. Journal of Automated Reasoning, 4, pp. 287-325, 1988.

[76] Reed D. W. & Loveland W.D. A Comparison of three Prolog Extensions. Journal of Logic Programming, 12, pp. 25-50, 1992.

[77] Reiter R. On Closed World Data Bases. In Logic and Data Bases, Gallaire & Minker (eds.), Plenum Press, New York, 1978.

[78] Robinson J. A. A Machine-Oriented Logic Based on the Resolution Principle. JACM, 12, pp. 23 - 41, 1965.

[79] Sato T. & Tamaki H. Transformational Logic Program Synthesis. Proc. Int. Conf. on Fifth Generation Computer Systems, 1984.

[80] Schwichtenberg H. Proofs as Programs. In: Proof Theory. A Selection of Papers from the Leeds Proof Theory Program 1990, S. Wainer (Ed.), Cambridge University Press 1992.

[81] Shepherdson J.C. Negation as Failure. (II) Journal of Logic Programming, 3, pp.185 - 202, 1985.

[82] Shepherdson J.C. Negation in Logic Programming. In: Foundations of Deductive Databases and Logic Programming, Minker J. (ed.), Morgan Kaufmann, 1988.

[83] Shepherdson J.C. A Sound and Complete Semantics for a Version of NF. TCS, 65(3): 343 - 371, 1989

[84] Stärk R. The Proof-Theory of Logic Programs with Negation. PhD. Thesis, University of Bern, 1992.

[85] Stärk R. Cut-Property and Negation as Failure, Technical Report, University of Bern, 1992.

[86] Stärk R. From Logic Programs to Inductive Definitions. Technical Report, University of München, 199e.

[87] Stickel M. A Prolog Technology Theorem Prover: a New Exposition and Implementation in Prolog. 464 SRI International, Technical Note, 46, 4. Menlo Park, California, 1989.

[88] Stuckey P. Constructive Negation for Constraint Logic Programming, Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 328 - 339, 1991.

[89] Tamaki H. & Sato T. Unfold/Fold Transormation of Logic Programs. Proc. ICLP84, pp. 127 - 138, 1984.

[90] Tarnlund S. A. Horn Clause Computability. BIT, 17, 2 pp. 215 - 226, 1977.

[91] Troesltra A.S. & van Dalen D. Constructivism in Mathematics, vol 1-2. North-Holland, Amsterdam, 1988.

[92] Van Emden M.H. & Kowalski R.A. The Semantic of Predicate Logic as a Programming Language. JACM, vol. 23, no. 4, pp. 733 - 742, 1976.

[93] Wallace M. Negation by Constraints: a Sound and Efficient Implementation of Negation in Deductive Databases. Proc. 1987 Symp. on Logic Programming, Computer Society Press, pp. 253 - 263, 1987.

[94] Wos L. & McCune W. Automated Theorem Proving and Logic Programming: A Natural Symbiosis. Journal of Logic Programming, pp. 1 - 53, 1991.

[95] Yardeni E. & Shapiro E. A Type System for Logic Programs. Journal of Logic Programming, 10, pp. 125 – 153, 1991.