Elimination of Negation in a Logical Framework

Alberto Momigliano

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A.

                              mobile@cs.cmu.edu

Abstract. Logical frameworks with a logic programming interpretation such as hereditary Harrop formulae (HHF) [12] cannot express directly negative information, although negation is a useful specification tool. Since negationas-failure does not fit well in a logical framework, especially one endowed with hypothetical and parametric judgments, we adapt the idea of elimination of negation introduced in [17] for Horn logic to a fragment of higher-order HHF. This entails finding a middle ground between the Closed World Assumption usually associated with negation and the Open World Assumption typical of logical frameworks; the main technical idea is to isolate a set of programs where static and dynamic clauses do not overlap.

1 Introduction

Deductive systems consist of axioms and rules defining derivable judgments; they can be used to specify logics and aspects of programming languages such as operational semantics or type systems. A logical framework is a meta-language for the specification, implementation and verification of deductive systems and possibly their meta-theory. A logical framework must provide tools which make encodings as simple and direct as possible. One well known example is higher-order abstract syntax, which moves renaming and substitution principles to the meta-language. Logical frameworks should be by design as weak as possible to simplify proofs of adequacy of encodings, effective checking of the validity of derivations and proof-search as well as unification. Many logical framework have been proposed in the literature (see [16] for an overview) and many extensions are also under consideration. However, we must carefully balance the benefits that any proposed extension can bring against the complications its meta-theory would incur.

This paper discusses the introduction of a logically justified notion of negation in logical frameworks with a logic programming interpretation such as hereditary Harrop formulae (HHF) [12] and its implementation in λProlog [15]. We intend this to form the basis for type-theoretic frameworks such as LF [9] and its implementation Twelf [19]. Those systems do not provide a primitive negation operator. Indeed, constructive logics usually implement negative information as ¬A ≡ A →⊥, where ⊥ denotes absurdity and the Duns Scoto Law is the elimination rule. Thus negative predicates have no special status; that would correspond to explicitly code negative information in a program, which is entirely consistent with the procedural interpretation of hypothetical judgments available in logical frameworks with a logic programming interpretation. However, this would not only significantly complicate goal-oriented proof search, but providing negative definitions seems to be particularly error-prone, repetitive and not particularly interesting; more importantly, in a logical framework we have also to fulfill the proof obligation that the proposed negative definition does behave as the complement (of its positive counterpart). Automating the synthesis of negative information has not only an immediate practical relevance in the logic programming sense, but it may also have a rather dramatic effect on the possibility of implementing deductive systems that would prove to be too unwieldy to deal with otherwise. The synthesis of the negation of predicates such as typable, well-formed, canonical form, subsort, value etc.–as well as Prolog-like predicates such as equality, set membership and the like–will increase the amount of meta-theory that can be formalized.

Traditionally, negation-as-failure (NF ) [5] has been the overwhelmingly used approach in logic programming (see [2] for a recent survey): that is, infer ¬A if every proof of A fails finitely. The operational nature of this rule motivates the lack of a unique semantics and some of its related troublesome features: possible unsoundness, incompleteness and floundering. Furthermore, even if we manage to isolate a well-behaved logical fragment, such as acyclic normal programs, allowing NF in a logical framework would make adequacy theorems more difficult to prove, as both provability and unprovability must now be considered. The situation is even further complicated when we step to frameworks with hypothetical judgments; as recognized first by Gabbay [6], the unrestricted combination of NF and embedded implication is particularly problematic, since it leads to the failure of basic logic principles such as cut-elimination.

The approach to negation that we adopt is transformational, also known as intensional negation, initiated in [17] and developed in Pisa [3] for Horn logic with negation. Roughly, given a clause with occurrences of negated predicates, say Q ← G, ¬P, G′, where P is an already defined atom, the aim is to derive a positive predicate, say non P which implements the complement of P, preserving operational equivalence; then, it is merely a question of replacement, yielding the negation-less clause Q ← G, non P, G′. This has the neat effect that negation and its problems are eliminated, i.e. we avoid any extension to the (meta) language. Technically, we can achieve this by transforming a Horn program into negation normal form and then by negating atoms via complementing terms, a problem first addressed in [10] for firstorder terms. A final issue, which we do not tackle here, is dealing with local variables, which, during the transformation, become (extensionally) universally quantified [1].

Unfortunately, this approach does not scale immediately to logical frameworks such as HHF, for three main reasons:

1. The simply-typed λ-calculus is not closed under term complement.

2. Negation normal forms are incompatible with the operational semantics required by HHF.

3. There is an intrinsic tension between the Closed World Assumption (CWA), which is associated with negation, and the Open World Assumption (OWA) typical of languages with embedded implication.

The first problem has been solved in [14], by introducing a strict λ-calculus where term complement in the simply typed λ-calculus can be embedded and performed.

The second issue is orthogonal and requires an operational notion of normal form. The third one is rooted in the fundamental difference between Horn and HHF formulae: as well known, a Horn predicate definition can be seen as an inductive definition of the same predicate. The minimality condition of inductive definitions excludes anything else which is not allowed by the base and step case(s). This corresponds in Horn logic to the existence of the least model and to the consistency of the CWA and its finitary approximation, the completion of a program [5]: every atom which is not provable from a program is assumed to be false. Languages which provide embedded implication and universal quantification are instead open-ended and thus require the OWA; in fact, dynamic assumptions may, at run-time, extend the current signature and program in a totally unpredictable way. This makes it in general impossible to talk about the closure of such a program. In the literature the issue has been addressed in essentially three ways:

1. By enforcing a strict distinction between CWA and OWA predicates and applying NF only to the former [8], where the latter would require minimal negation.

2. By switching to a modal logic, which is able to take into account arbitrary extensions of the program as possible worlds (see the completion construction in [7] for N-Prolog and [4] for Hypothetical Datalog).

3. By embracing the idea of partiality in inductive definitions and using the rule of definitional reflection to incorporate a proof-theoretical notion of closure analogous to the completion [11].

None of those approaches are satisfactory for our purposes: most of the predicates we want to negate are open-ended; similarly, definitional reflection is not well-behaved (for example cut is not eliminable) for that very class of programs we are interested in. Moreover, we need to express the negation of a predicate in the same language where the predicate is formulated. Our solution is to restrict the set of programs we deem deniable in a novel way, so as to enforce a Regular Word Assumption (RWA): we define a class of programs whose dynamic assumptions extend the current database in a specific regular way. This constitutes a reasonable middle ground between the CWA which allows no dynamic assumption but is amenable to negation and the OWA, where assumptions are totally unpredictable. The RWA is also a promising tool in the study of the meta-logical frameworks [18]. Technically, this regularity under dynamic extension is calibrated so as to ensure that static and dynamic clauses never overlap. This property extends to the negative program; in a sense, we maintain a distinction between static and dynamic information, but at a much finer level, i.e. inside the definition of a predicate. The resulting fragment is very rich, as it captures the essence of the usage of hypothetical and parametric judgments in a logical framework; namely, that they are intrinsically combined to represent scoping constructs in the object language. This is why we contend that this class of programs is adequate for the practice of logical frameworks.

It is clear that elimination of negation makes sense only when negation is stratified, i.e. the negative predicates ultimately refers (in the call graph) to a positive one. While there may be a place in logic programming for non-stratified negation, this does not seem to be the case for a logical framework. Another difference from traditional logic programming is that negation applies only to terminating programs; thus it refers not to finite failure but to unprovability tout court, as we refrain from negating programs whose negation is not recursively axiomatizable. We will thus identify negation with a complement operation.

The rest of the paper is organized as follow: in Sect. 2 we give an informal view of the complement algorithm by means of examples, while Sect. 3 introduces the language. Section 4 describe term and clause complementation. We conclude in Sect. 5 with some remarks on future work. We refer to [13] for more details and proofs omitted here for reasons of space.

2 A Motivating Example

Consider the expressions of the untyped λ-calculus:

e ::= x | Λx . e | e_{1} e_{2}

We encode these expressions as terms in (labeled) HHF via the usual techniques of higher-order abstract syntax as canonical forms over the following signature:

Σ = exp : type, lam : (exp → exp) → exp, app : exp → (exp → exp)

The representation function is given by:

⌜x⌝ = x  ⌜Λx . e⌝ = lam (λx:exp. ⌜e⌝)  ⌜e_{1} e_{2}⌝ = app ⌜e_{1}⌝ ⌜e_{2}⌝

A term is linear if every functional subterm uses each argument exactly once: in particular, we check for linearity of a function making sure that the latter is linear in its first argument and then recurring on the rest of the expression.

linapp : linear(app E_{1} E_{2}) ← linear(E_{1}) ∧ linear(E_{2}).
linlam : linear(lam(λx . E x))
← linx(λx . E x) ∧ (∀y:exp. linear(y) → linear(E y)).
linxx : linx(λx . x).
linxap1 : linx(λx . app (E_{1} x) E_{2}) ← linx(λx . E_{1} x).
linxap2 : linx(λx . app E_{1} (E_{2} x)) ← linx(λx . E_{2} x).
linxlm : linx(λx . lam(λy . E x y)) ← (∀y:exp. linx(λx . E x y)).

This is clearly a decision procedure, which can be complemented; an expression is not linear if there is some function which either does not use its argument or uses it more than once. First, the complement of linapp does not pose any problem, as it is a Horn clause: an application is not linear if either the first element or the second is not linear. Next, a lambda expression is not linear in two cases: one, if it is not linear in its first argument:

¬linlam1 : ¬linear(lam λx . E x) ← ¬linx(λx . E x).

Secondly, if its body is not linear. Now, this poses a new problem, as we have to negate a hypothetical and parametric goal. Let us reason by example and suppose we are given, in the empty context, a goal linear(lam(λx . lam(λy . x))), which is unprovable, since the second lambda term is not linear in y; the proof tree yields the failure leaf linx(λx . z), for a new parameter z, in the context z:exp; linear(z). Our guiding intuition is that we want to mimic a failure derivation so as to provide a successful derivation from the negative definition, i.e. a proof of ¬linx(λx . z) from z:exp; linear(z); this shows one prominent feature of complementation of an HHF formula: negation ‘skips’ over ∀ and →, since it needs to mirror failure from assumptions. Now, let us examine clause linxlm and reconsider the above failure leaf; in a first attempt, according to the idea above, the complement would be:

¬^{?} linxlm : ¬linx(λx . lam(λy . E x y)) ← (∀y:exp. ¬linx(λx . E x y)).

However, there is no way to obtain a proof of ¬linx(λx . z) from the current context. Indeed, the linxlm clause does not carry enough information so that its complement can mimic the failure proof. In a sense, the clause is not assumption-complete: once it has introduced a new parameter, the clause only specifies how to use it in a positive context. It is up to us to synthesize its dynamic negative definition, in this case simply ∀y:exp. ¬linx(λx . y). More in general, it is a characteristic of HHF that the negation of a clause is not strong enough to determine the behavior of a program under complementation. We will have to insert (via a source-to-source transformation) additional structure in a predicate definition, in order to completely determine the provability or failure of goals which mention parameters. By observing the structure of all possible assumption that a predicate definition can make, we will augment those assumptions with their negative definition. In particular, we first augment the clause linxlm:

aug_{D}(linxlm) : linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . y) → linx(λx . E x y)).

so that, by complementation, we obtain:

¬aug_{D}(linxlm) : ¬linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

Unfortunately, the procedure we have outlined is not possible in general. Consider a clause encoding the introduction rule for implication in natural deduction, which can be used to check whether an implicational formula trivially holds:

Σ = form : type, imp : form → (form → form), a : form, b : form, c : form
impi : nd(A imp B) ← (nd(A) → nd(B)).

Following our earlier remark its complement would be:

¬impi1 : ¬nd(a).
¬impi2 : ¬nd(b).
¬impi3 : ¬nd(c).
¬^{?} impi : ¬nd(A imp B) ← (nd(A) → ¬nd(B)).

This specification is clearly incorrect since both nd(a imp a) and ¬nd(a imp a) are derivable from the empty context. We can isolate one major problem: in clause impi the assumption nd(A) which is dynamically added to the (static) definition of the nd predicate overlaps with the head of the clause. A symmetrical problem can occur when dynamic and static clause do differ but their complements do not. We have thus isolated two main issues:

1. Exhaustivity: we need to enrich clauses so that every (ground) goal or its negation is provable.

2. Exclusivity: we need to isolate a significant fragment where it is not the case that both a goal and its negation are provable.

We will achieve exhaustivity (Theorem 2) by augmenting the program with the complement of assumptions; moreover, we will achieve exclusivity (Theorem 1) with the restriction to complementable programs. To anticipate the idea, a clause is complementable if every assumption contains some eigenvariable at execution time.

3 Provability and Unprovability

We will use the following somewhat unusual language:

Simple Types A ::= a | A_{1} → A_{2}
Terms M ::= c | x | λx:A. M | M_{1} M_{2}
Atoms Q ::= q \overline{M_{n}} | ¬q \overline{M_{n}}
Clauses D ::= ⊤ |⊥| Q ← G | D_{1} ∧ D_{2} | D_{1} ∨ D_{2} | ∀x:A. D
Goals G ::= Q | ⊤ |⊥| \overline{M_{n}} =^{·} \overline{N_{n}} | \overline{M_{n}} ≠^{·} \overline{N_{n}} |
G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | D → G | ∀x:A. G
Signatures Σ ::= · | Σ, a:type | Σ, c:A
Parameter Contexts Γ ::= · | Γ, x:A
Assumptions D ::= ⊤ | D ∧ D

There is a distinguished type o for propositions which can occur only as the target of some A. We remark that ‘¬’ is not a connective, but a name constructor for atomic formulae; ‘facts’ are represented, for convenience, by Q ← ⊤, although in examples we will omit to mention ⊤. We assume that existential variables occur only once in the head of program clauses (i.e. clauses are left-linear); this can always be achieved by introducing disequations in the body. In this paper we restrict ourselves to programs such that all assumptions are Horn and which can be proven to be terminating under some well-founded ordering. We introduce the uniform proofs system [12] for (immediate) provability and denial in Fig. 1. For terminating programs, we can prove that the failure to achieve a proof of G translates into (a derivation of) the denial of G. Note also that due to the presence of disjunction as a clause constructor, uniform proofs are not complete for our language. We will remedy this situation in Sect. 4.

Γ; D ⊢_{P} G  Program P and assumption D uniformly entail G.
Γ; D ⊬_{P} G  Program P and assumption D uniformly deny G.
Γ; D ⊢_{P} D>>Q Clause D from P and D immediately entails atom Q.
Γ; D ⊬_{P} D>>Q Clause D from P and D immediately denies atom Q.

\frac{⊢ ⊤}{Γ; D ⊢_{P} ⊤}  \frac{⊬_{⊥}}{Γ; D ⊬_{P}⊥}

\begin{aligned}Γ; D ⊢_{P} G_{1}  Γ; D ⊢_{P} G_{2} \\ & ⊢∧ \\ Γ; D ⊢_{P} G_{1} ∧ G_{2} \end{aligned}  \begin{aligned}Γ; D ⊬_{P} G_{1}  Γ; D ⊬_{P} G_{2} \\ & ⊬∨ \\ Γ; D ⊬_{P} G_{1} ∨ G_{2} \end{aligned}

\begin{aligned}Γ; D ⊢_{P} G_{i} \\ & ⊢ ∨_{i} \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}  \begin{aligned}Γ; D ⊬_{P} G_{i} \\ & ⊬ ∧_{i} \\ Γ; D ⊬_{P} G_{1} ∧ G_{2} \end{aligned}

\begin{aligned}Γ; D ⊢_{P} [t/x]G \\ & ⊢ ∃ \\ Γ; D ⊢_{P} ∃x:A. G \end{aligned}  \begin{aligned}for all n Γ; D ⊬_{P} [n/x]G \\ & ⊬ ∃ \\ Γ; D ⊬_{P} ∃x:A. G \end{aligned}

\begin{aligned}Γ; (D ∧ D) ⊢_{P} G \\ & ⊢ → \\ Γ; D ⊢_{P} D → G \end{aligned}  \begin{aligned}Γ; (D ∧ D) ⊬_{P} G \\ & ⊬ → \\ Γ; D ⊬_{P} D → G \end{aligned}

\begin{aligned}(Γ, y:A); D ⊢_{P} [y/x]G \\ & ⊢∀^{y} \\ Γ; D ⊢_{P} ∀x:A. G \end{aligned}  \begin{aligned}(Γ, y:A); D ⊬_{P} [y/x]G \\ & ⊬∀^{y} \\ Γ; D ⊬_{P} ∀x:A. G \end{aligned}

\begin{aligned}Γ; D ⊢_{P} (P ∧ D)>>Q \\ & ⊢ & At \\ Γ; D ⊢_{P} Q \end{aligned}  \begin{aligned}Γ; D ⊬_{P} (P ∧ D)>>Q \\ & ⊬ & At \\ Γ; D ⊬_{P} Q \end{aligned}
\frac{>> ⊥}{Γ; D ⊢_{P}⊥ >>Q}  \frac{≯>⊤}{Γ; D ⊬_{P} ⊤>>Q}

\begin{aligned}Γ; D ⊢_{P} [t/x]D>>Q \\ & >>∀ \\ Γ; D ⊢_{P} ∀x:A. D>>Q \end{aligned}  \begin{aligned}for all n Γ; D ⊬_{P} [n/x]D>>Q \\ & ≯>∀ \\ Γ; D ⊬_{P} ∀x:A. D>>Q \end{aligned}

\begin{matrix}Γ; D ⊢_{P} D_{i}>>Q \\ >> & ∧_{i} \\ Γ; D ⊢_{P} D_{1} ∧ D_{2}>>Q \end{matrix}  \begin{matrix}Γ; D ⊬_{P} D_{i}>>Q \\ ≯> & ∨_{i} \\ Γ; D ⊬_{P} D_{1} ∨ D_{2}>>Q \end{matrix}

Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q

>>∨

Γ; D ⊢_{P} D_{1} ∨ D_{2}>>Q

Γ; D ⊬_{P} D_{1}>>Q Γ; D ⊬_{P} D_{2}>>Q

≯>∧

Γ; D ⊬_{P} D_{1} ∧ D_{2}>>Q
\overline{N_{n}} = \overline{M_{n}} Γ; D ⊢_{P} G

>> →

Γ; D ⊢_{P} (q \overline{N_{n}} ← G)>>q \overline{M_{n}}

\begin{aligned}\overline{N_{n}} ≠ \overline{M_{n}} \\ & ≯>→_{1} \\ Γ; D ⊬_{P} (q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}  \begin{aligned}\overline{N_{n}} = \overline{M_{n}}  Γ; D ⊬_{P} G \\ & ≯>→_{2} \\ Γ; D ⊬_{P} (q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

Fig. 1. (Immediate) Provability and Denial

Some brief comments are in order: the (in)equalities rules simply mirror the object logic symbols =^{·}, ≠^{·} as meta-level (in)equalities and are omitted. ≯>∀ and ⊬ ∃ are infinitary rules, given the meta-linguistic extensional universal quantification on all terms. Rules ⊢ ∀, ⊬ ∀ are instead parametric in y, where the ()^{y} superscript reminds us of the eigenvariable condition. The denial rules for implication and universal quantification reflect the operational semantics of unprovability that we have discussed earlier.

We start by putting every program in a normalized format w.r.t. assumptions, so that every goal in the scope of an universal quantifier is guaranteed to depend on some assumption, possibly the trivial clause ⊤. This has also the effect of ‘localizing’ the trivial assumption to its atom, a property will be central while complementing assumptions; for example we re-write linxlm as follows:

linxlm : linx (λx . lam(λy . E x y))
← (∀x:exp. ⊤_{linx} → linx (λx . E x z)).

For the sake of this paper, we also need to modify the source program so that every term in a clause head is fully applied, i.e. it is a lambda term where every variable mentioned in the binder occurs in the matrix; this makes term complementation (Sect. 4) much simpler. For example clause linxap1 is rewritten as:

linxap1 : linx(λx . app (E_{1} x) (E_{2} x)) ← linx(λx . E_{1} x) ∧ vac(λx . E_{2} x).

where vac(λx . E_{2} x) enforces that x does not occur in E_{2} x. Its definition is typedirected, but we have shown in [14] how to internalize these occurrence constraints in a strict type theory, so that this further transformation is not needed.

We now discuss context schemata. As we have argued in Sect. 2, we cannot obtain closure under clause complementation for the full logic of HHF, but we have to restrict ourselves to a smaller (but significant) fragment. This in turn entails that we have to make sure that during execution, whenever an assumption is made, it remains in the fragment we have isolated. Technically, we proceed as follows:

– We extract from the static definition of a predicate the general ‘template’ of a legal assumption.

– We require dynamic assumptions to conform to this template.

We thus introduce the notion of schema satisfaction, which uses the following data structure: a context schema abstracts over all possible instantiations of a context during execution. To account for that, we introduce a quantifier-like operator, say SOME Φ .D, which takes a clause and existentially bounds its free variables, if any, i.e. Φ = F V (D). The double bar ‘∥’, not to be confused with the BNF ‘|’ that we informally use in the meta-language, denotes schema alternatives, while ‘∘’ stands for the empty context schema.

Contexts Schemata S ::= ∘ | S∥(Γ; SOME Φ .D)

The linear predicate yields this (degenerate) example of context schema:

S_{linear} = ∘ | S_{linear}∥x:exp; linear(x) | S_{linear}∥x:exp; ⊤_{linx}

We extract a context schema by collecting all negative occurrences in a goal; this is achieved by simulating execution until an atomic goal is reached and the current list of parameters and assumptions is returned, with their correct existential binding. Different clauses may contribute different schema alternatives for a given predicate definition. A run-time context consists of a set of blocks, each of which is an instance of the context schema, for example:

y_{1}:exp, y_{2}:exp, x_{1}:exp; ⊤_{linx} ∧ ⊤_{linx} ∧ linear(x_{1})

We will need to disambiguate blocks in run-time contexts; overlapping may indeed happen when the alternatives in a context schema are not disjoint. Intuitively, a block is complete when an atomic conclusion is reached during the deduction. Any bracketing convention will do:

⌈y_{1}:exp⌉, ⌈y_{2}:exp⌉, ⌈x_{1}:exp⌉; ⌈⊤_{linx}⌉ ∧ ⌈⊤_{linx}⌉ ∧ ⌈linear(x_{1})⌉

We then define when a formula satisfies a schema. We start by saying that a completed block belongs to a schema when the block is an alphabetic variant of some instantiation of one of the alternatives of the schema. Then, the empty run-time context is an instance of every schema. Secondly, if Γ′ and D′ are completed blocks which belong to S, and Γ; D in an instance of S, then (Γ, ⌈Γ′⌉); (D ∧ ⌈D′⌉) is an instance of S, provided that D′ is a valid clause. The latter holds when each of its subgoals satisfies the schema. This is achieved by mimicking the construction on the run-time schema until in the base case we check whether the resulting context is an instance of the given schema.

We can prove that if a context schema is extracted from a program, then any instance of the latter satisfies the former. Moreover, execution preserves contexts, i.e. every subgoal which arises in any given successful or failed (immediate and nonimmediate) sub-derivation satisfies the context schema. See [13] for the formal development.

4 Clause Complementation

We restrict ourselves to programs with:

– Goals where every assumption is parametric, i.e. it is in the scope of a positive occurrence of a universal quantifier and the corresponding parameter occurs in head position in the assumption.

– Clauses Q ← G such that the head of every term in Q is rigid.

Note that the rigidity restriction applies only to non-Horn predicate definitions and can be significantly relaxed; see [13] for a detailed account.

The first ingredient is higher-order pattern complement, Not(M), investigated in the general case in [14]; we give here the rules for complementing fully applied patterns:

\frac{Not F lx}{Γ ⊢ Not(E \overline{x_{n}}) ⇒ ∅}

Γ, x:A ⊢ Not(M) ⇒ N : B
Not Lam
Γ ⊢ Not(λx:A. M) ⇒ λx:A. N : A → B
g ∈ Σ ∪ Γ, g : A_{1} → … → A_{m} → a, m ≥ 0, h ≢ g
Not App^{1}
Γ ⊢ Not(h \overline{M_{n}}) ⇒ g (Z_{1}Γ) … (Z_{m}Γ) : a
∃i : 1 ≤ i ≤ n Γ ⊢ Not(M_{i}) ⇒ N :
Not App^{2}
Γ ⊢ Not(h \overline{M_{n}}) ⇒ h (Z_{1}Γ) … (Z_{i−1}Γ) N (Z_{i+1}Γ) … (Z_{n}Γ) : a

where the Z’s are fresh variables which may depend on the domain of Γ, h ∈ Σ ∪ Γ, and Γ ⊢ h : A_{1} → … → A_{n} → a. Γ ⊢ Not(M) = N : A iff N = {N | Γ ⊢ Not(M) ⇒ N : A}. For example:

· ⊢ Not(λx . x) = {λx . lam(λy . E x y), λx . app (E_{1} x) (E_{2} x)}

If we write Γ ⊢ M ∈ ∥N∥ : A when M is a ground instance of a pattern N at type A, we can show that Not behaves as the complement on sets of ground terms, i.e.

1. (Exclusivity) Not (Γ ⊢ M ∈ ∥N∥ : A and Γ ⊢ M ∈ ∥Not(N)∥ : A).

2. (Exhaustivity) Either Γ ⊢ M ∈ ∥N∥ : A or Γ ⊢ M ∈ ∥Not(N)∥ : A.

Complementing goals is immediate: we just put the latter in negation normal form, respecting the operational semantics of failure.

\frac{Not_{G}⊤}{Not_{G}(⊤) =⊥}  \frac{Not_{G} ⊥}{Not_{G}(⊥) = ⊤}  \frac{Not_{G}At}{Not_{G}(Q) = ¬Q}

\frac{Not =^{·}}{Not_{G}(\overline{M_{n}} =^{·} \overline{N_{n}}) = (\overline{M_{n}} ≠^{·} \overline{N_{n}})}  \frac{Not ≠^{·}}{Not_{G}(\overline{M_{n}} ≠^{·} \overline{N_{n}}) = (\overline{M_{n}} =^{·} \overline{N_{n}})}
Not_{G}(G) = G′
Not_{G}∀
Not_{G}(∀x:A. G) = ∀x:A. G′

Not_{G}(G) = G′
Not_{G} →
Not_{G}(D → G) = D → G′
Not_{G}(G_{1}) = G′_{1} Not_{G}(G_{2}) = G′_{2}
Not∧
Not_{G}(G_{1} ∧ G_{2}) = G′_{1} ∨ G′_{2}
Not_{G}(G_{1}) = G′_{1} Not_{G}(G_{2}) = G′_{2}
Not∨
Not_{G}(G_{1} ∨ G_{2}) = G′_{1} ∧ G′_{2}

Clause complementation is instead more delicate: given a rule q \overline{M_{n}} ← G, its complement must contain a ‘factual’ part motivating failure due to clash with the head; the remainder Not_{G}(G) expresses failure in the body, if any. Clause complementation must discriminate whether (the head of) a rule belongs to the static or dynamic definition of a predicate. In the first case all the relevant information is already present in the head of the clause and we can use the term complementation algorithm. This is accomplished by the rule Not_{D} →, where a set of negative facts is built via term complementation Not(\overline{M_{n}}), namely ⋀_{\overline{N_{n}}∈Not(\overline{M_{n}})} ∀(¬q \overline{N_{n}} ← ⊤), whose fresh free variables are universally closed; moreover the negative counterpart of the source clause is obtained via complementation of the body. The original quantification is retained thanks to rule Not_{D}∀.

\frac{Not_{D}⊤}{Not_{D}(⊤) =⊥}  \frac{Not_{D} ⊥}{Not_{D}(⊥) = ⊤}
Not_{G}(G) = G′
Not_{D} ←

Not_{D}(q \overline{M_{n}} ← G) = ( ⋀_{\overline{N_{n}}∈Not(\overline{M_{n}})} ∀(¬(q \overline{N_{n}}) ← ⊤)) ∧ (¬q \overline{M_{n}} ← G′)

Not_{D}(D) = D′
Not_{D}∀
Not_{D}(∀x:A. D) = ∀x:A. D′
Not_{D}(D_{1}) = D′_{1} Not_{D}(D_{2}) = D′_{2}
Not∧
Not_{D}(D_{1} ∧ D_{2}) = D′_{1} ∨ D′_{2}
Not_{D}(D_{1}) = D′_{1} Not_{D}(D_{2}) = D′_{2}
Not∨
Not_{D}(D_{1} ∨ D_{2}) = D′_{1} ∧ D′_{2}

Otherwise, we can think of the complement of an atomic assumption (q M_{1} … x … M_{n}), which is by definition parametric in some x, as static clause complementation w.r.t. x, i.e. Not_{D}(q_{x} M_{1} … M_{i−1} M_{i+1} … M_{n}). However, most of those M_{i}, which at compile-time are variables, will be instantiated at run-time: therefore it would be incorrect to compute their complement as empty. Since we cannot foresee this instantiation, we achieve clause complementation via the introduction of disequations. This is realized by the judgment Γ ⊢ Notα(D). We need the following notion: a parameter x:a is relevant to a predicate symbol q (denoted xR^{i}q) if Σ(q) = A_{1} → ⋯ → A_{n} → o and for some 1 ≤ i ≤ n the target type of A_{i} is a.

\frac{Notα⊤}{Γ ⊢ Notα(⊤_{q}) = ⋀_{x∈dom(Γ)}( ⋀_{xR^{i}q} Not_{x}^{i}(⊤_{q}))}

Notα ←

Γ ⊢ Notα(Q ← G) = ( ⋀_{x∈dom(Γ)}( ⋀_{xR^{i}q} Not_{x}^{i}(Q))) ∧ (¬Q ← G′)

Both rules refer to an auxiliary judgment Not_{x}^{i}(D):

Not_{x}^{i}⊤
Not_{x}^{i}At

Not_{x}^{i}(q \overline{M_{n}}) = ⋀_{1≤j≤n,j≠i}(∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬(q \overline{Z_{e_{x}}^{i}}) ← M_{j} ≠^{·} Z_{j})

The idea is to:

Not_{G}(G) = G′ Σ(q) = A_{1} → ⋯ → A_{n} → o · ⊢ sh(x, A_{i}) = e_{x}

Not_{x}^{i}(⊤_{q}) = ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬(q \overline{Z_{e_{x}}^{i}}) ← ⊤ Σ(q) = A_{1} → ⋯ → A_{n} → o · ⊢ sh(x, A_{i}) = e_{x}

– Pivot on x:a ∈ Γ.

– Locate a type A_{i} such that x:a is relevant to q at i.

– Complement D w.r.t. x and i.

– Repeat for every A_{i} and for every x.

The rest of the rules for Γ ⊢ Notα(D) are completely analogous to the ones for Not_{D}(D) and are omitted. Both simply recur on the program respecting the duality of conjunction and disjunction w.r.t. negation. Notice the different treatment of the trivial clause ⊤ by rules Not_{D}⊤ and Notα⊤: if no parameter has been assumed, then ⊤ truly stands for the empty predicate definition and its complement is the universal definition ⊥. If, on the other hand Γ is not empty, it means that ⊤_{q} has been introduced during the ⊤-normalization preprocessing phase and has been localized to the predicate q. The rule Not_{x}^{i}⊤ allows to build a new negative assumption w.r.t. q, x, i in case ⊤_{q} is the only dynamic definition of q. As ⊤_{q} carries no information at all concerning q, the most general negative assumption is added; the notation \overline{Z_{e_{x}}^{i}} abridges Z_{1} … Z_{i−1} e_{x} Z_{i+1} … Z_{n}, where the Z’s are fresh logic variables and e_{x} is a term built prefixing a parameter x by an appropriate number of lambda’s, according to the type of its position; this is specified by the Γ ⊢ sh(x, A) judgment, omitted here (but see it in action in Example 1).

Now that we have discussed how to perform clause, assumption and goal complementation, we synchronize them together in a phase we call augmentation, which simply inserts the correct assumption complementation into a goal and in turn into a clause. This is achieved by a judgment Γ; D ⊢_{Φ} aug_{D}(D), again omitted here for reasons of space.

For example, consider the copy clause on λ-terms:

cplam : copy (lam E) (lam F)
← (∀x:exp. copy x x → copy (E x) (F x)).

The augmentation procedure collects x:exp; copy x x and calls x:exp ⊢ Notα(copy x x).

First Not_{1}^{x}(copy x x) = (∀E′:exp. ¬copy E′ x ← x ≠^{·} E′), secondly Not_{2}^{x}(copy x x) =

(∀F′:exp. ¬copy x F′ ← x ≠^{·} F′), yielding:

aug_{D}(cplam) : copy (lam E) (lam F)
← (∀x:exp.

(∀E′:exp. ¬copy E′ x ← x ≠^{·} E′) ∧

(∀F′:exp. ¬copy x F′ ← x ≠^{·} F′) →

(copy x x → copy (E x) (F x))).

Let us see how rule Not_{x}^{i}⊤ enters the picture; recall the normalized linxlm clause. From · ⊢ sh(y, exp → exp) = λx . y we have Not_{1}^{y}(⊤_{linx}) = ¬linx (λx . y):

aug_{D}(linxlam) : linx (λx . lam(λy . E x y))
← (∀y:exp. ¬linx (λx . y) → linx (λx . E x y)).

Let us apply the complement algorithm to the linx predicate definition. The strict predicate is simply the complement of the vac predicate previously introduced. Again, these annotations can be internalized in a strict type theory [14].

Not_{D}(def(linx)) = Not_{D}(linxx) ∨ Not_{D}(linxap1) ∨ Not_{D}(linxap2) ∨ Not_{D}(linxlm) = (¬linx(λx . app (E_{1} x) (E_{2} x)) ∧ ¬linx(λx . lam(λy . (E x y)))) ∨ (¬linx(λx . x) ∧ ¬linx(λx . lam(λy . (E x y))) ∧ ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{2} x) ∧ ¬linx(λx . app (E_{1} x) (E_{2} x)) ← ¬linx(λx . E_{1} x)) ∨ (¬linx(λx . x) ∧ ¬linx(λx . lam(λy . (E x y))) ∧ ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{1} x) ∧ ¬linx(λx . app (E_{1} x) (E_{2} x)) ← ¬linx(λx . E_{2} x)) ∨ (¬linx(λx . x) ∧ ¬linx(λx . app (E_{1} x) (E_{2} x)) ∧ ¬linx(λx . lam(λy . (E x y))) ← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y))).

We can now establish exclusivity and exhaustivity of clause complementation. Let Not_{D}(P) = P^{−}:

Theorem 1 (Exclusivity). For every run-time context Γ; D instance of a schema S extracted from an augmented program P:

1. It is not the case that Γ; D ⊢_{P} G and Γ; D ⊢_{P^{−}} Not_{G}(G).

2. It is not the case that Γ; D ⊢_{P} (P ∧ D)>>Q and Γ; D ⊢_{P^{−}} (P^{−} ∧ D)>>¬Q.

Proof. (Sketch) By mutual induction on the structure of the derivation of Γ; D ⊢_{P} G and Γ; D ⊢_{P} (P ∧ D)>>Q. The proof goes through as there is no ‘bad’ interaction between the static and dynamic definition of a predicate; namely there is no overlap between a clause from P and from D since in every atomic assumption there must be an occurrence of an eigenvariable and every corresponding term in a program clause head must start with a constructor. If both clauses are dynamic, it holds because an appropriate disequation is present; this approximates what happens in the static case, which is based on term exclusivity.

The denial system comes in handy in the following proof.

Theorem 2 (Exhaustivity). For every substitution θ, σ and run-time context Γ; [θ]D instance of a schema S extracted from an augmented program P:

1. If for all θ Γ; [θ]D ⊬_{P} [θ]G, then there is a σ such that Γ; [σ]D ⊢_{P^{−}} [σ]Not_{G}(G). 2.1 If, for all θ Γ; [θ]D ⊬_{P} [θ]P>>[θ]Q, then here is a σ such that Γ; [σ]D ⊢_{P^{−}}

[σ]Not_{D}(D)>>[σ]¬Q. 2.2 If, for all θ Γ; [θ]D ⊬_{P} [θ]D>>[θ]Q, then here is a σ such that Γ; [σ]D ⊢_{P^{−}}

[σ]Notα(D)>>[σ]¬Q.

The proof is by mutual induction on the structure of the given derivations. As a corollary, we are guaranteed that clause complementation satisfies the boolean rules of negation.

Finally, we show how to eliminate from clauses the ‘∨’ operator stemming from the complementation of conjunctions, while preserving provability; this will recover uniformity in proof-search.

The key observation is that in this context ‘∨’ can be restricted to a program constructor inside a predicate definition; therefore it can be eliminated by simulating unification in the definition, that is (Q_{1} ← G_{1}) ∨ (Q_{2} ← G_{2}) ≡ θ(Q_{1} ← G_{1} ∧ G_{2}), where θ = mgu(Q_{1}, Q_{2}).

However, the (strict) higher-order unification problem is quite complex, even more so due to the mixed quantifier structure of HHF; since we have already parameter (dis)equations introduced by the augmentation procedure, as well as variable-variable (dis)equations stemming from left-linearization, we first compile clauses in an intermediate language which keeps the unification problems explicit and then we perform constraint simplification as in Twelf. Continuing with our example and simplifying the constraints:

Not_{D}(linxx) ∨ Not_{D}(linxap1) =
¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{2} x) ∧
¬linx(λx . app (E_{1} x) (E_{2} x)) ← ¬linx(λx . E_{1} x) ∧
¬linx(λx . lam(λy . E x y)).

The final definition of ¬linear and in turn ¬linx is:

¬linapp : ¬linear(app E_{1} E_{2})
← ¬linear(E_{1}) ∨ ¬linear(E_{2}).
¬linlam1 : ¬linear(lam(λx . E x))
← ¬linx(λx . E x)
∨ (∀y:exp. (¬linx(λx . y) ∧ linear(y)) → ¬linear(E y)).
¬linxap0 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{1} x) ∧ strict(λx . E_{2} x).
¬linxap1 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{2} x) ∧ ¬linx(λx . E_{1} x).
¬linxap2 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← strict(λx . E_{1} x) ∧ ¬linx(λx . E_{2} x).
¬linxap3 : ¬linx(λx . app (E_{1} x) (E_{2} x)) ← ¬linx(λx . E_{1} x) ∧ ¬linx(λx . E_{2} x).
¬linxlm : ¬linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

5 Conclusions and Future Work

We have presented elimination of negation in a fragment of higher-order HHF; our next task is to overcome some of the current restrictions, to begin with the extension to any order, which requires a more refined notion of context. The issue of local variables is instead more challenging. The proposal in [1] is not satisfactory and robust enough to carry over to logical frameworks with intensional universal quantification. Our approach will be again to synthesize a HHF definition for the clauses with local variables which during the transformations has became extensionally quantified. Our final goal is to achieve negation elimination in LF. Acknowledgments. I would like to thank Frank Pfenning for his continuous help and guidance. The notion of context schema is inspired by Schürmann’s treatment of analogous material in [18].

References

[1] D. P. A. Brogi, P. Mancarella and F. Turini. Universal quantification by case analysis. In Proc. ECAI-90, pages 111–116, 1990.

[2] K. Apt and R. Bol. Logic programming and negation. Journal of Logic Programming, 19/20:9–72, May/July 1994.

[3] R. Barbuti, P. Mancarella, D. Pedreschi, and F. Turini. A transformational approach to negation in logic programming. Journal of Logic Programming, 8:201–228, 1990.

[4] A. Bonner. Hypothetical reasoning with intuitionistic logic. In R. Demolombe and T. Imielinski, editors, Non-Standard Queries and Answers, volume 306 of Studies in Logic and Computation, pages 187–219. Oxford University Press, 1994.

[5] K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322. Plenum Press, New York, 1978.

[6] D. M. Gabbay. N-Prolog: An extension of Prolog with hypothetical implications II. Logical foundations and negation as failure. Journal of Logic Programming, 2(4):251– 283, Dec. 1985.

[7] L. Giordano and N. Olivetti. Negation as failure and embedded implication. Journal of Logic Programming, 36(2):91–147, August 1998.

[8] J. Harland. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD thesis, Edinburgh, Jan. 1991.

[9] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, Jan. 1993.

[10] J.-L. Lassez and K. Marriot. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):301–318, Sept. 1987.

[11] R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In G. Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, June 1997.

[12] D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[13] A. Momigliano. Elimination of Negation in a Logical Framework. PhD thesis, Carnegie Mellon University, 2000. Forthcoming.

[14] A. Momigliano and F. Pfenning. The relative complement problem for higher-order patterns. In D. D. Schreye, editor, Proceedings of the 1999 International Conference on Logic Programming (ICLP’99), pages 389–395, La Cruces, New Mexico, 1999. MIT Press.

[15] G. Nadathur and D. Miller. An overview of λProlog. In K. A. Bowen and R. A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810–827, Seattle, Washington, Aug. 1988. MIT Press.

[16] F. Pfenning. Logical frameworks. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 2000. In preparation.

[17] T. Sato and H. Tamaki. Transformational logic program synthesis. In International Conference on Fifth Generation Computer Systems, 1984.

[18] C. Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. forthcoming.

[19] C. Schürmann and F. Pfenning. Automated theorem proving in a simple meta-logic for LF. In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286–300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.