The Relative Complement Problem for Higher-Order Patterns

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

                mobile@cs.cmu.edu

Frank Pfenning Department of Computer Science Carnegie Mellon University Pittsburgh, PA 15213, U.S.A.

                  fp@cs.cmu.edu

Abstract

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a finite set of patterns. We therefore generalize the simply-typed λ-calculus to include an internal notion of strict function so that we can directly express that a term must depend on a given variable. We show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and unification. Our principal application is the transformational approach to negation in higher-order logic programs.

Keywords: Relative complement, strict λ-calculus, higher-order logics, intensional negation.

1 Introduction

APPIA-GULP-PRODE’99

In most functional and logic programming languages the notion of a pattern, together with the requisite algorithms for matching or unification, play an important role in the operational semantics. Besides unification other problems such as generalization or complement also arise frequently. In this paper we are concerned with the problem of pattern complement in a setting where patterns may contain binding operators, so-called higher-order patterns [10]. Higher-order patterns have found applications in logic programming [10], logical frameworks [13], term rewriting [12], and functional logic programming [5]. Higher-order patterns inherit many pleasant properties from the first-order case. In particular, most general unifiers [10] and least general generalizations [14] exist, even for complex type theories.

A version of this paper will appear in ICLP99

Unfortunately, the complement operation does not generalize as smoothly. Lugiez [8] has studied the more general problem of higher-order disunification and had to go outside the language of patterns and terms to describe complex constraints on sets of solutions. We can isolate one basic difficulty: a pattern such as λx. E x for an existential variable E matches any term of appropriate type, while λx. E matches precisely those terms λx. M where M does not depend on x. The complement then consists of all terms λx. M such that M does depend on x. However, this set cannot be described by a pattern, or even a finite set of patterns.

This formulation of the problem suggests that we should consider a λ-calculus with an internal notion of strictness so that we can directly express that a term must depend on a given variable. For reasons of symmetry and elegance we also add the dual concept of invariance expressing that a given term does not depend on a given variable. As in the first-order case, it is useful to single out the case of linear patterns, namely those where no existential variable occurs more than once.^{1} We show that patterns in our calculus have the following properties:

1. The complement of a linear pattern is a finite set of linear patterns.

2. Unification of two patterns is decidable and leads to a finite set of most general unifiers.

Consequently, finite sets of linear patterns in the strict λ-calculus are closed under complement and unification. If we think of finite sets of linear patterns as representing the set of all their ground instances, then they form a boolean algebra under simple union, intersection (implemented via unification) and the complement operation.

The paper is organized as follows: Section 2 briefly reviews related work, while Section 3 introduces some preliminary definitions. In Section 4 we introduce a strict λ-calculus and note some basic properties such as the existence of canonical forms. Section 5 introduces a restriction of the language for which complementation is possible. The algorithm for negation is presented in Section 6. In Section 7 we give a unification algorithm for our fragment. We conclude in Section 8 with some applications and speculation on future research. For reasons of space, a number of lemmas and proofs are omitted here and can be found in [11].

2 Related Work

The Relative Complement Problem for Higher-Order Patterns

Complement problems have a number of applications in theoretical computer science (see [4] for a list of references). For example, they are used in functional programming to produce non-ambiguous function definitions by patterns and to improve their compilation and in rewriting systems to check whether an algebraic specification is sufficiently complete. They can also be employed to analyze communicating processes expressed by infinite transition systems. Other applications lie in the areas of machine learning and inductive theorem proving. In logic programming Kunen [6] used term complement to represent infinite sets of answers to negative queries. Our main motivation has been the explicit synthesis of the negation of higher-order logic programs, as discussed in Section 8.

1This notion of linearity should not be confused with the eponymous concept in linear logic and λ-calculus.

Lassez and Marriot [7] proposed the seminal uncover algorithm for computing relative complements and introduced the now familiar restriction to linear terms. We quote the definition of the “¬” algorithm for the (singleton) complement problem given in [1] which we generalize in Definition 11. Given a finite signature Σ and a linear term t we define:

¬_{Σ}(x)  = ∅
¬_{Σ}(f(\overline{t_{n}})) =
{g(x⃗) | for all g ∈ Σ distinct from f} ∪
{f(z_{1}, …, z_{i−1}, s, z_{i+1}, …, z_{n}) | s ∈ ¬_{Σ}(t_{i}), i ∈ [1, n]}

An alternative solution to the relative complement problem is disunification (see [4] for a survey and [8] for an extension to the simply-typed λ-calculus): here operations on sets of terms are translated into conjunctions or disjunctions of equations and disequation under explicit quantifiers. Non-deterministic application of a few dozen rules eventually turns a given problem into a solved form. Though a reduction to a significant subset of the disunification rules is likely to be attainable for complement problems, control is a major problem. We argue that using disunification for this purpose is unnecessarily general. Moreover the higher-order case results in additional complications, such as restrictions on the occurrences of bound variables, which fall outside an otherwise clean framework. As we show in this paper, this must not necessarily be the case. We believe that our techniques can also be applied to analyze disunification, although we have not investigated this possibility at present.

3 Preliminaries

In this section we introduce some preliminary definitions and examples which guide our development. We write P for atomic types, c for term-level constants, and x for term-level variables.

Simple Types A ::= P | A_{1} → A_{2}
Terms M ::= c | x | λx:A. M | M_{1} M_{2}
Signatures Σ ::= · | Σ, P:type | Σ, c:A
Contexts Γ ::= · | Γ, x:A

We require that signatures and contexts declare each constant or variable at most once. Furthermore, we identify contexts which differ only in their order and promote “,” to denote disjoint set union. As usual we identify terms which differ only in the names of their bound variables. We restrict attention to well-typed terms, omitting the standard typing rules.

In applications such as logic programming or logical frameworks, λ-abstraction is used to represent binding operators in some object language. In such a situation the most useful notion of normal form are long βη-normal forms (which we call canonical forms), since the canonical forms are almost always the terms in bijective correspondence with the objects we are trying to represent. Every well-typed term in the simply-typed λ-calculus has a unique canonical form—a property which persists in the strict λ-calculus introduced in Section 4.

We denote existential variables of type A (also called logical variables, metavariables, or pattern variables) by E_{A}, although we mostly omit the type A when it is clear from the context. We think of existential variables as syntactically distinct from bound variables or free variables declared in a context. A term possibly containing some existential variables is called a pattern if each occurrence of an existential variable appears in a subterm of the form E x_{1} … x_{n}, where the arguments x_{i} are distinct occurrences of free or bound variables (but not existential variables).

Semantically, an existential variable E_{A} stands for all canonical terms M of type A in the empty context with respect to a given signature. We extend this to arbitrary well-typed terms in the usual way, and write Γ ⊢ M ∈ ∥N∥ : A when a term M is a ground instance of a pattern N at type A. In this setting, unification of two patterns without shared existential variables corresponds to an intersection of the set of terms they denote [10, 14]. This set is always either empty, or can be expressed again as the set of instances of a single pattern. That is, patterns admit most general unifiers.

The class of higher-order patterns inherits many properties from first-order terms. However, as we will see, it is not closed under complement, but a special subclass is. We call a canonical pattern Γ ⊢ M : A fully applied if each occurrence of an existential variable E under binders y_{1}, …, y_{m} is applied to some permutation of the variables in Γ and y_{1}, …, y_{m}. Fully applied patterns play an important role in functional logic programming and rewriting [5] because any fully applied existential variable Γ ⊢ E x_{1} … x_{n} denotes all canonical terms with free variables from Γ. It is this property which makes complementation particularly simple.

Example 1 Consider the untyped λ-calculus.

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

We encode these expressions using the usual techniques of higher-order abstract syntax (see, for example, [9]) 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}⌝

The representation of an object-language β-redex then has the form

⌜(λx . e) f⌝ = app (lam (λx:exp. ⌜e⌝)) ⌜f⌝

where ⌜e⌝ my have free occurrences of x. When written as a pattern with variables E_{exp→exp} and F_{exp} ranging over closed terms, this is expressed as app (lam (λx : exp. (E x)) F). The complement of the right-hand side considered as a pattern with respect to the empty context contains every top-level λ-abstraction plus every application where the first argument is not an abstraction:

¬(app (lam (λx:exp. (E x)) F) = {lam (λx:exp. H x), app (app H_{1} H_{2}) H_{3}}

For patterns which are not fully applied, the complement cannot be expressed as a finite set of patterns, as the following example illustrates.

Example 2 The encoding of an η-redex takes the form

⌜λx . e x⌝ = lam(λx:exp. app ⌜e⌝ x)

where ⌜e⌝ may contain no free occurrence of x. The side condition is expressed in a pattern by introducing an existential variable E_{exp} which does not depend on x. Hence, its complement with respect to the empty context should contain, among others, also all terms

lam (λx:exp. app (Ex) x)

where E does depend on x.

Note that there is no finite set of patterns which has as its ground instances exactly those terms M which depend on a given variable x. Following standard terminology, we call such terms strict in x and the corresponding function λx:A. M a strict function. As the example above shows, the complement of patterns which are not fully applied can therefore not be represented as a finite set of patterns. This failure of closure under complementation cannot be avoided similarly to the way in which left-linearization bypasses the limitation to linear patterns and it needs to be addressed directly.

One approach is taken by Lugiez [8]: he modifies the language of terms to permit occurrence constraints. For example λxyz. M{1, 3} would denote a function which depends on its first and third argument. The technical handling of those objects then becomes awkward as they require specialized rules which are foreign to the issues of complementation.

Since our underlying λ-calculus is typed, we use typing to express that a function must or must not depend on its argument. In the next section we develop such a λ-calculus and generalize the complement algorithm to work on such terms.

4 A Strict λ-Calculus

As we have seen in the preceding section, the complement of some patterns in the simply-typed λ-calculus cannot be expressed in a finitary manner within the same calculus. We thus generalize our language to include strict functions of type A →^{1} B (which are guaranteed to depend on their argument) and invariant functions of type A →^{0} B (which are guaranteed not to depend on their argument). Of course, any concretely given function either will or will not depend on its argument, but in the presence of existential variables we still need the ability to remain uncommitted. Therefore our calculus also contains the full function space A →^{u} B.

Labels k ::= 1 | 0 | u
Types A ::= P | A_{1} →^{k} A_{2}
Terms M ::= c | x | λx^{k}:A. M | M_{1} M_{2}^{k}
Contexts Γ ::= · | Γ, x:A

Note that there are three different forms of abstractions and applications, where the latter are distinguished by different labels on the argument. It is not really necessary to distinguish three forms of application syntactically, since the type of function determines the status of the application, but it is convenient for our purposes. A label u it is called undetermined; other labels are determined and denoted by d.

We use a formulation of the typing judgment with three zones, containing the undetermined, irrelevant and strict hypotheses, denoted by Γ, Ω, and Δ, respectively.

Γ; Ω; Δ ⊢ M : A

We implicitly assume a fixed signature Σ which would otherwise clutter the presentation.

Our system is biased towards a bottom-up reading of the rules in that variables never disappear, i.e., they are always propagated from the conclusion to the premises, although their status might be changed.

Let us go through the typing rules in detail. The requirement for the strict context Δ to be empty in the Id^{u} and Id^{1} rules expresses that strict variables must be used, while undetermined variables in Γ or irrelevant variables in Ω can be ignored. Note that there is no rule for irrelevant variables, which expresses that they cannot be used.

The introduction rules for undetermined, invariant, and strict functions simply add a variable to the appropriate context and check the body of the function.

The difficult rules are the three elimination rules. First, the undetermined context Γ is always propagated to both premises. This reflects that we place no restriction on the use of these variables.

Next we consider the strict context Δ. Recall that this contains the variables which should occur strictly in a term. An undetermined function M : A →^{u} B may or may not use its argument. An occurrence of a variable in the argument to such a function can therefore not be guaranteed to be used. Hence we must require in the rule →^{u} E for an application M N^{u} that all variables in Δ occur strictly in M. This ensures at least one strict occurrence in M and no further restrictions on occurrences of strict variables in the argument are necessary. This is reflected in the rule by adding Δ to the undetermined context while checking the argument N. The treatment of the strict variables in the vacuous application M N^{0} is similar.

In the case of a strict application M N^{1} each strict variable should occur strictly in either M or N. We therefore split the context into Δ_{M} and Δ_{N} guaranteeing that each variable has at least one strict occurrence in M or N, respectively. However,

\begin{aligned}c:A ∈ Σ \\ & Con \\ Γ; Ω; · ⊢ c : A \end{aligned}

\frac{Id^{u}}{(Γ, x:A); Ω; · ⊢ x : A} no Id^{0} rule  \frac{Id^{1}}{Γ; Ω; x:A ⊢ x : A}
(Γ, x:A); Ω; Δ ⊢ M : B

→^{u} I Γ; Ω; Δ ⊢ λx^{u}:A. M : A →^{u} B

Γ; (Ω, x:A); Δ ⊢ M : B

→^{0} I

Γ; Ω; Δ ⊢ λx^{0}:A. M : A →^{0} B

Γ; Ω; (Δ, x:A) ⊢ M : B

→^{1} I

Γ; Ω; Δ ⊢ λx^{1}:A. M : A →^{1} B

Γ; Ω; Δ ⊢ M : A →^{u} B (Γ, Δ); Ω; · ⊢ N : A

→^{u} E Γ; Ω; Δ ⊢ M N^{u} : B

Γ; Ω; Δ ⊢ M : A →^{0} B (Γ, Ω, Δ); ·; · ⊢ N : A

→^{0} E Γ; Ω; Δ ⊢ M N^{0} : B

(Γ, Δ_{N}); Ω; Δ_{M} ⊢ M : A →^{1} B (Γ, Δ_{M}); Ω; Δ_{N} ⊢ N : A

→^{1} E Γ; Ω; (Δ_{M}, Δ_{N}) ⊢ M N^{1} : B

Figure 1: Typing rules for λ^{→^{l}}

strict variables can occur more than once, so variables from Δ_{N} can be used freely in M, and variables from Δ_{M} can occur freely in N. As before, we reflect this by adding these variables to the undetermined context.

Finally we consider the irrelevant context Ω. Variables declared in Ω cannot be used except in the argument to an irrelevant function (which is guaranteed to ignore its argument). We therefore add the irrelevant context Ω to the undetermined context when checking the argument of a vacuous application M N^{0}.

Our strict λ-calculus satisfies the expected properties, culminating in the existence of canonical forms which is critical for the intended applications. A full account can be found in [11].

Let us examine the structural properties of contexts. Exchange is directly built into the formulation. Weakening is allowed in the undetermined and in the irrelevant contexts. Contraction holds anywhere. We also have the possibility to lose track of occurrences, if we are so inclined. This follows by structural inductions on the typing judgment.

Theorem 3 (Loosening)

1. If Γ; (Ω, x:C); Δ ⊢ M : A then (Γ, x:C); Ω; Δ ⊢ M : A.

2. If Γ; Ω; (Δ, x:C) ⊢ M : A then (Γ, x:C); Ω; Δ ⊢ M : A.

The notions of reduction and expansion derive directly from the ordinary β and η rules.

\begin{matrix}(λx^{k}:A. M) N^{k} & ⟶^{β} & [N/x]M \\ M : A →^{k} B & ⟶^{η̄} & λx^{k}:A. M x^{k} \end{matrix}

The subject reduction and expansion theorems are an immediate consequence of the structural and substitution properties generalized to this three-zoned calculus. The substitution properties again follow by straightforward structural inductions.

Theorem 4 (Subject Reduction and Expansion)

1. If Γ; Ω; Δ ⊢ M : A and M ⟶^{β} M′ then Γ; Ω; Δ ⊢ M′ : A.

2. If Γ; Ω; Δ ⊢ M : A and M : A ⟶^{η̄} M′ then Γ; Ω; Δ ⊢ M′ : A.

The above results culminate in the canonical form theorem: for every term M such that Γ; Ω; Δ ⊢ M : A, there exists a unique N in canonical (= β-normal ηlong) form, denoted Γ; Ω; Δ ⊢ N ⇑ A, such that M is convertible to N. The proof employs the standard method of logical relations, adapted to the specific λ-calculus we consider.

The following lemma establishes a consistency property of the type system relevant to complementation.

Lemma 5 (Exclusivity) It is not the case that both Γ; Ω; (Δ, x:A) ⊢ M : C and Γ; (Ω, x:A); Δ ⊢ M : C.

5 Embedding the Simply-Typed λ-Calculus

Now that we have developed a calculus which is potentially strong enough to represent the negation of linear patterns, we need to answer two questions: how do we embed the original λ-calculus, and is the calculus now closed under complement?

In this paper, we do not answer the second question conclusively. However, our algorithm is sound and complete for the fragment which results from the natural embedding of the original simply-typed λ-calculus which is sufficient for all applications we have presently considered (see Section 8).

Recall that we introduced strictness to capture occurrence conditions on variables in canonical forms. This means that constants (and by extension bound variables) should be considered strict functions of their argument, since these arguments will indeed occur in the canonical form. On the other hand, if we have a second order constant, we cannot restrict the argument function to be either strict or vacuous, since this would render our representations inadequate.

Example 6 Continuing Example 1, we see

⌜λx. λy. x⌝ = lam (λx:exp. lam (λy:exp. x))

so the argument to the first occurrence of ‘lam’ is a strict function, while the argument to the second occurrence is an invariant function. If we can give only one type to ‘lam’ it must therefore be (exp →^{u} exp) →^{1} exp.

Generalizing this observation means that positive occurrence of function types are translated to strict functions, while negative occurrences to undetermined functions. We can formalize this as an embedding of the simply-typed λ-terms into a fragment of strict terms via two mutually recursive functions ()^{−} and ()^{+}. First, the definition on types.

(A → B)^{−} = A^{+} →^{u} B^{−}
(A → B)^{+} = A^{−} →^{1} B^{+}
P^{−} = P^{+} = P

We extend it to canonical terms (including existential variables), signatures, and contexts as follows:

(λx:A. M)^{−} = λx^{u}:A^{+}. M^{−}
M^{−} = M^{+} for M of base type
x^{+} = x
c^{+} = c
(E_{A} x_{1} … x_{n})^{+} = F_{A^{−}} x_{1}^{u} … x_{n}^{u}
(M N)^{+} = M^{+} (N^{−})^{1}
(·)^{+} = ·
(Γ, x:A)^{+} = Γ^{+}, x:A^{+}
(Σ, P:type)^{+} = Σ^{+}, P:type
(Σ, c:A)^{+} = Σ^{+}, c:A^{+}

The image of the embedding of the canonical forms of the simply-typed λ-calculus gives rise to the following fragment, which we call simple terms.

Simple Terms M ::= λx^{u}:A^{+}. M | h M_{1}^{1} … M_{n}^{1} | E_{A^{−}} x_{1}^{u} … x_{n}^{u}

We sometimes abbreviate h M_{1}^{1} … M_{n}^{1} as h \overline{M_{n}^{1}}. Note that by the restriction to long normal forms such terms and applications of pattern variables must be of base type. For every judgment J on simple terms, we will shorten Γ; ·; · ⊢ J into Γ ⊢ J.

The correctness of the embedding is easily established by induction over the structure of canonical forms.

Theorem 7 If Γ ⊢ M ⇑ A then Γ^{+} ⊢ M^{−} ⇑ A^{−}.

From now on we drop the ± embedding annotations from terms, types and contexts. We may also hide the ()^{1} decoration from strict application of constants in examples.

Simple terms enjoy the tightening property which is related to loosening (Theorem 3) and exclusivity (Theorem 5) and is crucial for the correctness proof of our complement algorithm. It expresses that every closed simple term is either strict or vacuous in a given undetermined variable. After appropriate generalization, the result follows by induction on the given derivation.

Theorem 8 (Tightening) Let M be a simple term without existential variables such that (Γ, x:C); Ω; Δ ⊢ M ⇑ A. Then Γ; Ω; (Δ, x:C) ⊢ M ⇑ A or Γ; (Ω, x:C); Δ ⊢ M ⇑ A.

It simplifies the presentation of the algorithms for complement and later unification if we extend every existentially quantified variable to be applied to all bound variables in their declaration order. This is possible for simple linear patterns without changing the set of its ground instances. We just insert vacuous applications, which guarantees that the extra variables are not used. We furthermore permute the argument to the standard order, which also does not affect the set of ground instances of linear patterns. In slight abuse of notation we call the resulting terms fully applied.

Example 9 The simple term from Example 2,

lam (λx^{u}:exp. app E x)

, has fully applied form

lam (λx^{u}:exp. app (Z x^{0}) x)

for a fresh existential variable Z of type exp →^{0} exp.

The translation to fully applied terms is proven correct by induction over the structure of the given canonical form, using a few straightforward lemmas regarding variable occurrences in simple terms. We use the judgment Γ ⊢ M ∈ ∥N∥ : A to denote that a term M of type A is a ground instance of N in context GG.

Theorem 10 Let N be a simple term and Q its fully applied translation. Then Γ ⊢ M ∈ ∥N∥ : A iff Γ ⊢ M ∈ ∥Q∥ : A.

From now on we tacitly assume that all simple terms are fully applied. We call a term E x_{1}^{l_{1}} … x_{n}^{l_{n}} (of base type) a generalized variable.

6 The Complement Algorithm

The idea of complementation for applications and abstractions is quite simple and similar to the first-order case. For generalized variables we consider each argument in turn. If an argument variable is undetermined it does not contribute to the negation. If an argument variable is strict then any term where this variable does not occur contributes to the negation. We therefore complement the corresponding label from 0 to 1 while all other arguments are undetermined. For vacuous argument variables we proceed dually. In preparation for the rules we define.

Not(1) = 0 Not(0) = 1

If Γ = x_{1}:A_{1}, …, x_{n}:A_{n}, we write E Γ^{u} for the application of E x_{1}^{u} … x_{n}^{u}. Such an application represents the set of all terms without existential variables and free variables from Γ.

Definition 11 (Higher-Order Pattern Complement) Fix a signature Σ. For a linear simple term M such that Γ ⊢ M : A define Γ ⊢ Not(M) ⇒ N : A by the following rules. Note that a given M may be related to several terms N all of which belong to the complement of M.

1 ≤ i ≤ n k ∈ {1, 0}
Not F lx

Γ ⊢ Not(E x_{1}^{l_{1}} … x_{i−1}^{l_{i−1}} x_{i}^{k} x_{i+1}^{l_{i+1}} … x_{n}^{l_{n}}) ⇒ H x_{1}^{u} … x_{i−1}^{u} x_{i}^{Not(k)} x_{i+1}^{u} … x_{n}^{u} : P

Γ, x:A ⊢ Not(M) ⇒ N : B
Not Lam

Γ ⊢ Not(λx^{u}:A. M) ⇒ λx^{u}:A. N : A →^{u} B

g ∈ Σ ∪ Γ, g : A_{1} →^{1} … →^{1} A_{m} →^{1} P, m ≥ 0, h ≢ g

Not App^{1}

Γ ⊢ Not(h \overline{M_{n}}^{1}) ⇒ g (H_{1}Γ^{u})^{1} … (H_{m}Γ^{u})^{1} : P

Γ ⊢ Not(M_{i}) ⇒ N : A_{i} 1 ≤ i ≤ n
Not App^{2}

Γ ⊢ Not(h \overline{M_{n}}^{1}) ⇒ h (H_{1}Γ^{u})^{1} … (H_{i−1}Γ^{u})^{1} N^{1} (H_{i+1}Γ^{u})^{1} … (H_{n}Γ^{u})^{1} : P

where the H’s are fresh generalized variables, h ∈ Σ ∪ Γ, and Γ ⊢ h : A_{1} →^{1} … →^{1} A_{n} →^{1} P. Finally we define Γ ⊢ ¬(M) = N : A if N = {N | Γ ⊢ Not(M) ⇒ N : A}.

Note that if E_{A} is a generalized variable considered in the empty context, it has the canonical form λ\overline{x_{n}^{u}} . E \overline{x_{n}^{u}}. Hence · ⊢ ¬(E_{A}) = ∅ : A as expected.

Example 12 Let Γ be x:B, y:C:

Γ ⊢ ¬(E x^{u}y^{1}) = {F x^{u}y^{0}}
Γ ⊢ ¬(E x^{0}y^{1}) = {F x^{1}y^{u}, G x^{u}y^{0}}  (1)

We remark that the members of a complement set are not mutually disjoint, due to the indeterminacy of u. We can achieve a representation by exclusive patterns if we resolve this indeterminacy, that is, by considering for every argument x^{u} the two possibilities x^{1} and x^{0}. Thus, for example, the set from equation (1) may be transformed into

{F x^{1}y^{1}, G x^{1}y^{0}, H x^{0}y^{0}}

It is clear that in the worst case scenario the number of terms in a complement set is bound by 2^{n}; hence the usefulness of this further step needs to be pragmatically determined.

We can now revisit^{2} Example 2:

¬(lam(λx^{u}:exp. app (E x^{0}) x)) =
{lam(λx^{u}:exp. app (H x^{1}) (H′ x^{u})),
lam(λx^{u}:exp. app (H x^{u}) (app (H′ x^{u}) (H′′x^{u})),
lam(λx^{u}:exp. app (H x^{u}) (lam(λy^{u}:exp. H′ x^{u} y^{u})),
lam(λx^{u}:exp. lam(λy^{u}:exp. H x^{u} y^{u})),
lam(λx^{u}:exp. x),
app H H′}

We can show that simple terms are closed under complementation by induction over the construction of the complement.

Theorem 13 If M is a simple term, so is N, for all N ∈ Γ ⊢ ¬(M) : A.

We address the soundness and completeness of the complement algorithm. Termination is obvious as the algorithm is syntax-directed and only finitely branching. We write Γ ⊢ M ∈ ∥¬(N)∥ : A if Γ ⊢ Not(N) ⇒ Q : A and Γ ⊢ M ∈ ∥Q∥ : A.

Theorem 14 (Partition) For a fixed signature Σ, let Γ ⊢ N : A be a simple linear term. Then:

1. (Exclusivity) It is not the case that both Γ ⊢ M ∈ ∥N∥ : A and Γ ⊢ M ∈ ∥¬(N)∥ : A.

2. (Exhaustivity) If Γ ⊢ M : A then either Γ ⊢ M ∈ ∥N∥ : A or Γ ⊢ M ∈ ∥¬(N)∥ : A.

Note that exclusivity is based on Theorem 5, which holds for any strict term. In contrast, exhaustivity requires tightening (Theorem 8) which holds only for simple terms.

7 Unification of Simple Terms

We now address the issue of unification, i.e., intersection of simple linear higherorder patterns. We start by determining when two labels are compatible and define their intersection as follows:

2To avoid too many indices on existential variables, we adopt a convention that the scope of existential variables is limited to each member of a complement set.

1 ∩ 1 = u ∩ 1 = 1 ∩ u = 1
0 ∩ 0 = u ∩ 0 = 0 ∩ u = 0
u ∩ u = u

The remaining cases 1 ∩ 0 and 0 ∩ 1 are undefined since no variable can be both strict and vacuous in a given term.

We use Φ for sequences of labeled bound variables and write Φ(x) = k if x^{k} ∈ Φ. We then extend the intersection operations to these contexts:

· ∩ · = ·
(x^{k} Φ) ∩ (x^{k′} Φ′) = x^{k∩k′} (Φ ∩ Φ′) if k ∩ k′ is defined.

Following standard terminology with call atomic terms whose head is a free or bound variable rigid, while terms whose head is an existential variable is called flexible.

Definition 15 (Higher-Order Pattern Intersection) Fix a signature Σ. For simple linear terms M and N without shared variables such that Γ ⊢ M : A and Γ ⊢ N : A, we define Γ ⊢ M ∩ N ⇒ Q : A by the following rules.

\frac{∩ F lxF lx}{Γ ⊢ E Φ_{1} ∩ F Φ_{2} ⇒ H (Φ_{1} ∩ Φ_{2}) : P}

no rule for flex-flex with same variable

c ∈ Σ Γ ⊢ H_{1} Φ_{1} ∩ M_{1} ⇒ N_{1} : A_{1} ⋯ Γ ⊢ H_{n} Φ_{n} ∩ M_{n} ⇒ N_{n} : A_{n} ∩ F lxRgd^{c}

Γ ⊢ E Φ ∩ c \overline{M_{n}^{1}} ⇒ c \overline{N_{n}^{1}} : P

y ∈ Γ Γ ⊢ H_{1} Φ_{1} ∩ M_{1} ⇒ N_{1} : A_{1} ⋯ Γ ⊢ H_{n} Φ_{n} ∩ M_{n} ⇒ N_{n} : A_{n} ∩ F lxRgd^{y}

Γ ⊢ E Φ ∩ y \overline{M_{n}^{1}} ⇒ y \overline{N_{n}^{1}} : P

h ∈ Γ ∪ Σ Γ ⊢ M_{1} ∩ N_{1} ⇒ Q_{1} : A_{1} ⋯ Γ ⊢ M_{n} ∩ N_{n} ⇒ Q_{n} : A_{n} ∩ App

Γ ⊢ h \overline{M_{n}^{1}} ∩ h \overline{N_{n}^{1}} ⇒ h \overline{Q_{n}^{1}} : P

Γ, x:A ⊢ M ∩ N ⇒ Q : B

∩ Lam Γ ⊢ λx^{u}:A. M ∩ λx^{u}:A. N ⇒ λx^{u}:A. Q : A → B

where the H’s are fresh variables of correct typing and n ≥ 0.

We have omitted two rules ∩ RgdF lx^{c} and ∩ RgdF lx^{y} which are symmetric to ∩ F lxRgd^{c} and ∩ F lxRgd^{y}. The rules ∩ F lxRgd^{c} and ∩ RgdF lx^{c} have the following proviso: for all x ∈ Φ and 1 ≤ i ≤ n:

∀x.Φ(x) = 0 → ∀i . Φ_{i}(x) = 0
∀x.Φ(x) = u → ∀i . Φ_{i}(x) = u
∀x.Φ(x) = 1 → ∃i . Φ_{i}(x) = 1 ∧ ∀j, j ≠ i.Φ_{j}(x) = u

The rules ∩ F lxRgd^{y} and ∩ RgdF lx^{y} are subject to the proviso

∀x.Φ(x) = 0 → ∀i . Φ_{i}(x) = 0

∀x.Φ(x) = u → ∀i . Φ_{i}(x) = u
∀x.x ≠ y ∧ Φ(x) = 1 → ∃i . Φ_{i}(x) = 1 ∧ ∀j, j ≠ i.Φ_{j}(x) = u
Φ(y) = u ∨ (Φ(y) = 1 ∧ ∀i.Φ_{i}(y) = u)

Finally define Γ ⊢ M ˆ∩N : A = Q if Q = {Q | Γ ⊢ M ∩ N ⇒ Q : A}.

Some remarks are in order:

• In rule ∩ F lxF lx we can assume that the same list of variables, though possibly with different labeling, is the argument of E, F and H, since simple terms are fully applied and due to linearity we can always reorder the context to the same list. Since patterns are linear and M and N share no pattern variables, the flex-flex case arises only with distinct variables. This also means we do not have to apply substitutions or perform the customary occurs-check.

• In the flex/rigid and rigid/flex rules, the proviso enforces the typing discipline since each strict variable x must be strict in some premise. The modified condition on y takes into account that the head of an application constitutes a strict occurrence.

The following example illustrates how the Flex-Rigid rules, in this case ∩ F lxRgd^{c}, make unification on simple terms finitary.

Example 16 Consider the unification problem x:A ⊢ E x^{1} ˆ∩ c (F x^{u})^{1} (F′ x^{u})^{1}. Since x is strict in the LHS, there are two ways in which Φ can be split leading to the following sub-problems:

\begin{matrix}x:A ⊢ E′ x^{1} ∩ F x^{u} ⇒ H x^{1} & x:A ⊢ E′′ x^{u} ∩ F′ x^{u} ⇒ H′ x^{u} \\ x:A ⊢ E′ x^{u} ∩ F x^{u} ⇒ H x^{u} & x:A ⊢ E′′ x^{1} ∩ F′ x^{u} ⇒ H′ x^{1} \end{matrix}

Hence the result:

x:A ⊢ E x^{1} ˆ∩ c (F x^{u})^{1} (F′ x^{u})^{1} = {c (H x^{1})^{1} (H′ x^{u})^{1}, c (H x^{u})^{1} (H′ x^{1})^{1}}

Note that, similarly to complementation, intersection returns a solution with possible overlaps between the patterns. Again it is possible, in a post-processing phase, to transform the results into disjoint form.

As for complement, the termination of the algorithm is straightforward since the judgment is term-directed with finite branching. The adequacy proof for the unification algorithm on linear simple terms requires two implications which follow inductively, at the heart relying on properties of strict typing derivations.

Theorem 17 (Adequacy of Pattern Intersection) Fix a signature Σ. For simple linear terms N_{1} and N_{2} without shared variables such that Γ ⊢ N_{1} : A and Γ ⊢ N_{2} : A, Γ ⊢ M ∈ ∥N_{1}∥ : A and Γ ⊢ M ∈ ∥N_{2}∥ : A iff Γ ⊢ M ∈ ∥N_{1} ˆ∩N_{2}∥ : A.

8 Conclusion

We have shown that the complement of linear higher-order patterns cannot be expressed as a finite union of such patterns. To close the language under complement we generalized to a λ-calculus in which strict and vacuous functions can be expressed in the type system. The original language can be embedded compositionally into simple patterns. On this language, both complement and intersection (that is, unification) can be expressed as a finite union of simple linear patterns. From this it is easy to see that finite sets of simple linear patterns form a boolean algebra. Indeed, we can trivially define the relative complement of two terms via complement and intersection; namely, extending as expected the latter operation to operate on sets of terms, we have:

M − N = Mˆ∩¬N

Our main application lies in higher-order logic programming, where pattern complement is a necessary component in any algorithm to synthesize the negation of a given program. This synthesis includes two basic operations: negation to compute the complements of heads of clauses in the definition of a predicate, and intersection to combine results of negating individual clause heads. In this paper we have provided algorithms to compute both.

While this approach has been investigated for first-order Horn clauses [1] and CLP programs [2], the field has been little explored with respect to higher-order logics and logical frameworks. This is the most important future work we are considering; the algorithms presented here provide the central foundation.

We also plan to extend the results to dependent types to endow intentionally weak frameworks such as Twelf [15] with a logically meaningful notion of negation along the lines of [1]. Finally, we hope to address the general case of complementation and unification in the strict λ-calculus which is likely to be useful in linear logical frameworks as LLF [3].

Acknowledgments. We are grateful to Iliano Cervesato, Carsten Schürmann and Roberto Virga for useful comments on previous versions of this paper. This work has been partially supported by NSF Grant CCR-9619584.

References

[1] Roberto Barbuti, Paolo Mancarella, Dino Pedreschi, and Franco Turini. A transformational approach to negation in logic programming. Journal of Logic Programming, 8:201–228, 1990.

[2] P. Bruscoli, F. Levi, G. Levi, and M. C. Meo. Compilative constructive negation in constraint logic programs. In Sophie Tison, editor, Proc. Trees in Algebra and Programming - CAAP’94, 19th International Colloquium, volume 787, pages 52–76. Springer, 1994.

[3] Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264–275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[4] H. Comon. Disunification: a survey. In J-L. Lassez and G.Plotkin, editors, Computational Logic. MIT Press, Cambridge,MA, 1991.

[5] M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In Proc. Seventh International Conference on Rewriting Techniques and Applications (RTA’96), pages 138–152. Springer LNCS 1103, 1996.

[6] K. Kunen. Answer sets and negation-as-failure. In Jean-Louis Lassez, editor, Proceedings of the Fourth International Conference on Logic Programming (ICLP ’87), pages 219–228, Melbourne, Australia, May 1987. MIT Press.

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

[8] D. Lugiez. Positive and negative results for higher-order disunification. Journal of Symbolic Computation, 20(4):431–470, October 1995.

[9] Spiro Michaylov and Frank Pfenning. Natural semantics and some of its metatheory in Elf. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299–344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596.

[10] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497– 536, 1991.

[11] Alberto Momigliano. Elimination of negation in a logical framework. PhD thesis, Carnegie Mellon University, Forthcoming.

[12] Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 306–317, Utrecht, The Netherlands, May 1993.

[13] Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

[14] Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, The Netherlands, July 1991.

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