The Relative Complement Problem for Higher-Order Patterns Alberto Momigliano Carnegie Mellon University joint work with Frank Pfenning ICLP’99, December 1st, 1999

1. The Relative Complement Problem

2. Higher-Order Patterns

3. A Strict λ-Calculus

4. The Complement Algorithm

5. Intersection and Other Boolean Operations

Complement

• A term t with free variables as the intensional representation of its ground instances.

• Unification of two terms t = s as intersection t ∩ s of the (ground instances of) s and t.

• The complement of t is the set of ground terms which are not instances of t.

• Example: take the signature of numerals:

Not (s(0)) = {0, s(s(0)), s(s(s(0))) …} = {0, s(s(Y))}

Relative Complement

• Notation: a term stands for the set of its instances, ’,’ represents union.

• ’Multiple Complement’: by De Morgan rules:

Not {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:

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

Applications  1/2

• Functional programming:

1. Determination of exhaustivity and exclusivity 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  2/2

• Logic Programming:

1. Answers to negative goal as the complement of answers to its positive version [Kunen 1987].

2. Compilation of constructive negation [Chan 1989, Stuckey 1995].

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

• Our Aim: extend the latter to the higher-order case, both for higher-order languages (λ-Prolog) and Logical Frameworks (Twelf ).

First-Order Term Complement

Consider a finite (untyped) language L and a linear term t:

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

{g(z⃗) | for all g ∈ L distinct from f} ∪ {f(z_{1}, …, z_{i−1}, s, z_{i+1} , …, z_{n}) | s ∈ Not_{L}(t_{i}), i ∈ [1, n]}

• Problem: irrelevant outcomes. Example:

Not (0.nil) = {0, s(X), nil, s(X).L, 0.X.L}

• Solution: typing.

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 (full) second-order relative complement problem is not semi-decidable.

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

• Higher-order disunification (which encompasses complement problems) on higher-order patterns is decidable [Lugiez 1995].

Encoding the (untyped) λ-calculus  1/2

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

• The representation function:

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

• The encoding a β-redex as a pattern using logic variables E_{exp→exp} and F_{exp}:

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

Encoding the (untyped) λ-calculus  2/2

• Complement of the β-redex in the empty context: λx . e, (e_{1} e_{2}) e_{3}, that is

· ⊢ Not (app (lam (λx:exp. (E x)) F) =

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

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

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

• Hence e does not depend on x. Intuitively its complement should contain those application sub-terms where E does depend on x:

lam(λx:exp. ( app F #x ) (H x))

Fully vs. Non-Fully Applied Patterns

• The crux of the matter is whether a pattern is fully applied, i.e. if all bound variables appearing in the binder are mentioned in the scope of a logic variable. Example: λxλyλz . (E y x z). Non-example: λxλyλz . E y.

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

• The simply typed λ-calculus theory is not strong enough to directly represent the complement of non-fully applied patterns.

Strictness

• We need to have a notion of strictness in the language to express variable occurrence constraints.

• We internalize strictness as a type system, rather than promote constraints to first-class objects as in [Lugiez 1995] (technically awkward).

• 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 ::= P | A_{1} →^{k} A_{2}
Terms M ::= c | x | λx^{k}:A.M | (M N)^{k}
Contexts Γ ::= · | Γ, x:A

• Three labels: 1 ’must occur’, 0 ’must not occur’, u ’undetermined’.

• Three different forms of abstraction and application.

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

Complementing Patterns in the Strict Calculus

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

• 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 must be

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

• Constants (and bound variables) are strict functions, higher order functions must be undetermined.

Simple Terms

• Example:

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

• Bring to full application:

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

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

• The resulting language:

Simple Terms M ::= λx^{u}:A.M | (… (h M_{1})^{1} … M_{n})^{1} | E_{A} 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 proceed dually.

• Example:

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}}

Complement of Not (lam(λx^{u}:exp. app (E x^{0}) x))

different from first coordinate E x^{0}

{lam(λx^{u}:exp. app ( H x^{1} ) (H′ x^{u})),

different from second coordinate x

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}) ),

different from (app (E x^{0}) x)

lam(λx^{u}:exp. lam(λy^{u}:exp. H x^{u} y^{u}) ),

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

different from top lam(…) functor

app H H′ }

Unification of Simple Terms

• Unification as intersection of labels, (analogous to conjunction in three-valued logic).

• Finite sets of most general unifiers exist.

• Example: since x is strict in the LHS, it can be strict either in the first or second subterm of c:

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

Results

• Theorem If M is a simple term, so is Not (M).

• Theorem M is a ground instance of Not (N) if and only if M is not a ground instance of N.

• Theorem M is a ground instance of N_{1} and N_{2} if and only if M is a ground instance of N_{1} ∩ N_{2}.

• Corollary Finite sets of simple terms form a boolean algebra.

Towards Intensional Negation

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

Infer its negation by computing: Not (app (lam (λx^{u}:exp. E x^{u})) F)∩Not (lam(λx^{u}:exp. app (M x^{0}) x))

\begin{matrix}nb1 : & non isredx(lam(λx^{u}:exp. app (H x^{1}) (H′ x^{u}))) \\ nb2 : & non isredx(lam(λx^{u}:exp. app (H x^{u}) (app H′ x^{u}H′′ x^{u}))) \\ nb3 : & non isredx(lam(λx^{u}:exp. app (H x^{u}) (lam(λy^{u}:exp. H′ x^{u} y^{u})))) \\ nb4 : & non isredx(lam(λx^{u}:exp. lam(λy^{u}:exp. H x^{u} y^{u}))) \\ nb5 : & non isredx(lam(λx^{u}:exp. x)) \\ nb6 : & non isredx(app (app H_{1} H_{2}) H_{3} ) \end{matrix}

Conclusions

• The (relative) complement problem is interesting.

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

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

• We have shown how to perform any boolean operation on finite sets of simple terms.

Future work

• Combine term complement with clause complement to obtain intensional negation in higher-order logic programming [Done].

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

• Extend to the intuitionistic and linear dependently-typed case.