The Relative Complement Problem for Higher-Order Patterns

Alberto Momigliano Carnegie Mellon University

joint work with Frank Pfenning September 9 1999

Overview:

1. The Relative Complement Problem

2. Higher-Order Patterns

3. A Strict λ-Calculus

4. The Complement Algorithm

Complement Problem

• An open term t as the intensional representation of its ground instances, denoted ∥t∥.

• The complement of t, say Not (t), is the set of all ground terms which are not instances of t i.e. are not in ∥t∥.

• Example: take the signature of numerals:

\begin{matrix}Not (s(0)) = \{0, s(s(Y))\} \\ ∥z_{nat}∥ − ∥s(0)∥ = ∥0, s(s(Y))∥ = \{0, s(s(0)), s(s(s(0))) …\} \end{matrix}

• ’Multiple Complement’:

∥z_{nat}∥ − ∥0, s(s(Y))∥ = Not (0) ∩ Not (s(s(Y)) =
∥s(X)∥ ∩ ∥0, s(0)∥ = {s(0)}

Relative Complement

• All the ground instances of a given (finite) set of terms

which are not instances of another given one.

∥t_{1}, …, t_{n}∥ − ∥u_{1}, …, u_{m}∥

• Example: integer addition modulo 2.

s(s(0)) ⟼ 0
y + 0 ⟼ y
0 + y ⟼ y
y + y ⟼ 0

• A relative complement problem (sufficient completeness): ∥x_{1} + x_{2}∥ − ∥s(s(0)), 0 + y, y + 0, y + y∥ = ∅

Applications

• Functional programming:

1. Determination of exhaustivity and disjointness of a function definition by patterns.

2. Improved compilation by analysis of pattern applicability.

• Rewriting systems:

1. Sufficient completeness of an algebraic (equational) specification.

2. Infinite transition systems (temporal analysis of communicating processes).

Applications II

• Machine learning: a concept as a term with some (finite) exceptions.

• Inductive theorem proving: induction-less induction or proof by consistency.

• Logic Programming

1. Answers to negative goals as complement of answers to positive ones [Kunen 1987].

2. The transformational approach to negation [Sato& Tamaki 1985, Barbuti et al. 1990].

Our Aim: extend the latter to Logical Frameworks.

First-Order Term Complement

• Consider a finite (untyped) signature Σ and a term t:

Not_{Σ} (x)  = ∅
Not_{Σ} (f(t_{n})) =

{g(x⃗) | for all g ∈ Σ distinct from f} ∪

{f(z_{1}, …, z_{i−1}, s, z_{i+1} , …, z_{n}) |

s ∈ Not_{Σ} (t_{i}), i ∈ [1, n]}

• The ’Not’ function tends to produce irrelevant outcomes; Not_{ListN}(0) in the signature of lists of numerals contains not only s(X) but also nil and (cons X Xs).

• Complementation must be typed.

Linearity

• CAUTION: the intensional representation of terms is not

closed under complementation. Let Σ = a : i, f : i → i → i:

∥z∥ − ∥f(y, y)∥ = {a} ∪ {f(x, z) | x ≠ z}

But, incorrectly Not (f(y, y)) =^{?} {a}

• Correct only for linear terms, i.e. terms without repeated occurrence of a free variable [Lassez & Marriot 1987].

• Left-linearization [Plaisted, Stickel].

• Constrained terms, i.e. f(x, z) | x ≠ z.

• Complement operations based on disunification [Comon].

Higher-Order Patterns over Simple Types.

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

• Note: the second-order relative complement problem is not semi-decidable, but disunification on higher-order patterns is decidable [Lugiez 1995].

• Patterns [Miller 1991]: terms where every free variable is applied to distinct bound variables.

Examples: λx. c(E x), λxλy . F y x. Non-Examples: λx. E c, λx. F (E x), λx. E x x.

Fully Applied Pattern

• Complementation differentiates depending on whether the term is fully applied, i.e. when all variables appearing in the binder are mentioned in the scope of a free variable:

– Example: λxλyλz . c(E(y, x, z))

– Non-Example: λxλyλz . E y

• For fully applied terms proceed similarly to first-order with an additional case for bound variables: the complement is taken w.r.t. both the signature and the current context.

• In the non-fully applied case the complement has to take into account the occurrence issue.

Encoding the the (untyped) λ-calculus

Σ ::= exp : type , app : exp → exp → exp, lam : (exp → exp) → exp
e ::= x | lam (λx. e) | app e_{1}e_{2}

The representation function:

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

Encoding a β-redex:

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

Complement of the latter:

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

FAHP Complement

\frac{Γ, x:A ⊢ Not (M) = N : B}{Γ ⊢ Not (λx:A. M) = λx:A. N : A → B}

\frac{g ∈ Σ ∪ Γ, g:A_{1} → … → A_{m} → P m ≥ 0, h ≢ g}{Γ ⊢ Not (h M_{n}) = (… (g (Z_{1}Γ)) … (Z_{m}Γ)) : P}

h ∈ Σ ∪ Γ, Γ ⊢ h:A_{1} → … → A_{n} → P, 1 ≤ i ≤ n, Γ ⊢ Not (M_{i}) = N : A_{i} Γ ⊢ Not (h M_{n}^{1}) = (… (h (Z_{1}Γ)) … (Z_{i−1}Γ) N (Z_{i+1} Γ) … (Z_{m}Γ)) : P

(Z Γ)’s denotes the application of a fresh variable of correct typing to a context Γ.

Not (M : A) = {N | · ⊢ Not (M) = N : A}

NFA Patterns

• Encoding a η-redex, where x ∉ F V (e):

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

• Hence E does not depend on x and the term is not fully applied. Its complement should contain those applications where E does depend on x.

• The simply typed λ-calculus is not strong enough to directly represent the complement of non-fully applied patterns expressed as a finite set of patterns.

• This cannot be avoided similarly to left-linearization. We need to have a notion of strictness in the language.

Strictness

• Lugiez modifies the language of terms to promote constraints to first-class objects (awkward).

• We internalize strictness in the type-system.

• We generalize our language to include:

1. strict functions of type A →^{1} B (which are guaranteed to depend on their argument).

2. invariant functions of type A →^{0} B (which are guaranteed not to depend on their argument).

3. The full function space A →^{u} B.

The Language of Strict Types

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

• Three form of abstractions, given the label on bound variable.

• Three form of applications, as a postfix operation.

• The calculus is well-behaved (unique canonical forms exist).

Typing rules

\begin{aligned}c:A ∈ Σ \\ & Con \\ Γ; Ω; · ⊢ c : A \end{aligned} no Id^{0} rule
\frac{Id^{u}}{(Γ, x:A); Ω; · ⊢ x : A} \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

Typing rules, continued^{Γ; Ω; Δ ⊢ 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}

16

Complement Desiderata

• (Disjointness) It is not the case that M is both a ground instance of N and of Not (N).

• (Exhaustivity) M is a ground instance of N or M is a ground instance of Not (N).

• How we embed the original λ-calculus, and is the calculus now closed under complement?

• Exhaustivity does not hold in general as we allow logic variables in NFA terms.

• Restrict to a class of terms (that we call simple) for which exhaustivity holds and bring to full application those terms.

Embedding the simply-typed λ-Calculus

• Example:

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

• Argument to the first occurrence of ‘lam’ is strict, argument to the second is invariant. Type can only be

(exp →^{u} exp) →^{1} exp.

• Constants (and bound variables) are strict functions.

• Second order functions must be undetermined.

lam (λx:exp. lam (λy:exp. x)) ⇒ lam (λx^{u}:exp. lam (λy^{u}:exp. x)^{1})^{1}

Simple Terms

• In general:

1. positive occurrence of function types are translated to strict functions.

2. negative occurrences to undetermined functions.

• Make NFA terms fully applied:

λxλyλz . E y ⇒ λx^{u}λy^{u}λz^{u} . E x^{0} y^{u} z^{0}

• The resulting language:

Simple Terms M ::= λx^{u}:A.M | (… (h M_{1})^{1} … M_{n})^{1} | E x_{n}^{l}

The Complement Algorithm

• For logic variables consider each argument in turn:

1. If an argument variable is undetermined it does not contribute to the negation.

2. If an argument variable is strict complement the corresponding label from 1 to 0 while all other arguments are undetermined.

3. For vacuous argument variables we proceed dually.

\frac{1 ≤ j ≤ n k ∈ \{1, 0\}}{Not (E x_{1}^{l_{1}} … x_{j−1}^{l_{j−1}} x_{j}^{k} x_{j+1}^{l_{j+1}} … x_{n}^{l_{n}}) = Z x_{1}^{u} … x_{j−1}^{u} x_{j}^{Not (k)} x_{j+1}^{u} … x_{n}^{u} : P}

no rule for k = u

The Complement Algorithm II

\frac{Γ, x:A ⊢ Not (M) = N : B}{Γ ⊢ Not (λx^{u}:A. M) = λx^{u}:A. N : A → B}

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

Γ ⊢ Not (h M_{n}^{1}) = (… (g (Z_{1}Γ^{u}))^{1} … (Z_{m}Γ^{u}))^{1} : P

h ∈ Σ ∪ Γ, Γ ⊢ h:A_{1} →^{1} … →^{1} A_{n} →^{1} P, 1 ≤ i ≤ n, Γ ⊢ Not (M_{i}) = N : A_{i}

Γ ⊢ Not (h M_{n}^{1}) = (h (Z_{1}Γ^{u}))^{1} … (Z_{i−1}Γ^{u}) N^{1} (Z_{i+1} Γ^{u})^{1} … (Z_{m}Γ^{u}))^{1} : P

Not (M : A) = {N | · ⊢ Not (M) = N : A}

Examples of Complementation

If E is a variable, it has the canonical form λx_{n}^{u}.E x_{n}^{u}: hence Not (E) = ∅

Not (E x^{u}y^{1}) = {F x^{u}y^{0}}
Not (E x^{0}y^{1}) = {F x^{1}y^{u}, G x^{u}y^{0}}

Not (lam(λx^{u}:exp. app (E x^{0}) x^{u})) = {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′}

Results

• Theorem If M is a simple term, so is N, for all N ∈ Not (M).

• Theorem It is not the case that both Γ ⊢ M ∈ ∥N∥ : A and Γ ⊢ M ∈ ∥Not (N)∥ : A.

• Lemma Let M be a simple patterns:

If (Γ, x:C); ·; · ⊢ M ⇑↓ A then Γ; ·; x:C ⊢ M ⇑↓ A or Γ; x:C; · ⊢ M ⇑↓ A.

• Theorem

if D :: Γ ⊢ M : A then Γ ⊢ M ∈ ∥N∥ : A or Γ ⊢ M ∈ ∥Not (N)∥ : A.

Elimination of negation in a logical framework

• Consider the following ‘program’:

\begin{matrix}isredx(app (lam (λx^{u}:exp. E x^{u})) F) \\ isredx(lam(λx^{u}:exp. app (E x^{0}) x^{u}) \end{matrix}

• What about its negation? We can compute:

∥Z_{exp}∥−∥app (lam (λx^{u}:exp. E x^{u})) F, lam(λx^{u}:exp. app (M x^{0}) x∥

by intersecting Not (app (lam (λx^{u}:exp. E x^{u})) F) and Not (lam(λx^{u}:exp. app (M x^{0}) x^{u}))

• We can implement intersection as unification of simple terms (not detailed here).

Elimination of negation in a logical framework, II^{\begin{matrix}non isredx(lam(λx^{u}:exp. app (H x^{1}) H′ x^{u})) \\ non isredx(lam(λx^{u}:exp. app (H x^{u}) (app H′ x^{u}H′′ x^{u}))) \\ non isredx(lam(λx^{u}:exp. app (H x^{u}) (lam(λy^{u}:exp. H′ x^{u} y^{u})))) \\ non isredx(lam(λx^{u}:exp. lam(λy^{u}:exp. H x^{u} y^{u}))) \\ non isredx(lam(λx^{u}:exp. x)) \\ non isredx(app (app H_{1} H_{2}) H_{3} ) \end{matrix}}

25

Conclusions

• The (relative) complement problem is interesting.

• Even restricted to patterns, it does not generalize immediately to the higher-order case: we need to have an intrinsic notion of strictness.

• We have presented a strict λ-calculus, which we think gives a contribution to the understanding of sub-structural calculi.

• It is possible to perform any boolean operation on sets of simple terms.

Future work

• Combine term complementation with clause complementation in higher-order hereditary formulae.

• Address the issue of complement and intersection on any strict term.

• Extend to the intuitionistic and linear dependent type case.