Elimination of Negation in a Logical Framework

Alberto Momigliano Department of Philosophy Carnegie Mellon University

July 28, 2000

Thesis Defense

Thesis Committee: Frank Pfenning, Chair Dana Scott Dale Miller, Pennsylvania State University

Outline

1. Logical Frameworks

2. Adding Negation

3. Elimination of Negation vs. Negation-as-Failure 4. Elimination of Negation in a Logical Framework

(a) Clause Complement

(b) Term Complement

5. Conclusions and Future Work [landscape]slides latexsym amsfonts fslide-com

Alberto Momigliano Department of Philosophy Carnegie Mellon University

July 28, 2000

Thesis Defense

Thesis Committee: Frank Pfenning, Chair Dana Scott Dale Miller, Pennsylvania State University

Outline

1. Logical Frameworks

2. Adding Negation

3. Negation-as-Failure vs. Elimination of Negation 4. Elimination of Negation in a Logical Framework

(a) Clause Complement

(b) Term Complement

5. Contributions and Future Work

1. Logical frameworks:

A brief summary of their features and use.

Deductive Systems

• Deductive System: Calculus of axioms and inference rules which define derivable judgments. Used in the presentation of logics and aspects of programming languages such as:

– Type systems.

– Operational semantics.

– Abstract machines and compilation.

– Algorithms (e.g. type inference, unification, theorem proving).

Logical Frameworks

• Logical Framework: Meta-language for the specification, implementation and verification of (the meta-theory of) deductive systems.

– Reasoning within a specified system (operational semantics of Mini-ML).

– Reasoning about a deductive system (proof of type preservation).

• Formalism: hereditary Harrop formulae (HHF), dependently typed λ-calculi (LF), labeled deductive systems, inductive definitions, rewrite logics…

• We work in a fragment of HHF, but our design decisions are influenced by LF.

Logical Framework Design

• Logical frameworks are intentionally weak by design to facilitate:

– Informal proofs of adequacy of representation.

– Effective checking of the validity of derivations.

– Proof-search and unification.

• Extending a logical framework: need tools to make specifications concise, but balance benefits against complications in its meta-theory.

• (Conservative) extensions: sub-typing, modularity, equational reasoning, linearity… What about having negation?

2. Adding Negation:

Why negation is a useful notion in specifications.

Negation in Specification: Examples  1/2

• Formal definition of a programming language in the style of natural semantics: Progress lemma (well-typed expressions cannot go wrong):

if e : τ and e is not a value, there exists e′ such that e ↦ e′

• Process algebra: safety in an algorithm for mutual exclusion: for any transition, if the initial state is safe, so is the final one.

– A state is safe if processes are not in their critical section at the same time.

Negation in Specification: Examples  2/2

• Type inference: an expression is not well-typed.

• Functional program analysis: a function is not linear.

• Operational semantics: an expression is not in normal form.

• Algorithmic sub-typing: a sort is not a subsort (of another).

• Prolog style: two elements are different, an element is not a member of a list.

Negation in Logical Frameworks

• Logical frameworks with logic programming interpretation have no (declarative) negation operator, to preserve goal-oriented proof search.

• Need to explicitly program the negative code: for example, define non-value(e). Tedious and error-prone.

• Need to prove that this code implements the negation of the intended predicate.

• Our contribution: automation of this synthesis of negative information, proven correct once and for all.

3. Negation-as-Failure vs. Elimination of Negation:

• Problems with NF

• Elimination of Negation in the Horn case • Benefits of Elimination of Negation

Negation-as-Failure: Horn case  1/2

• NF (Clark [1978]) is the usual answer in LP:

P infers ¬A if A finitely fails from P

• Not declarative, but easy to implement (no change to the interpreter).

• Possibly unsound and generally incomplete: semantics?

• Closed World Assumption: Horn Logic ∼ inductive definitions: what is not provable is assumed to be false.

• Allowing negation in clauses may spoil their (monotone) inductive nature.

Negation-as-Failure: Logical Frameworks  2/2

• Even in a well-behaved fragment, NF in a logical framework makes the meta-theory much harder (provability and unprovability).

• Logical frameworks such as HHF cannot in general be seen as (monotone) inductive definitions, because they allow hypothetical and parametric judgments:

Q ← (D → G) Q ← ∀x:A. G

• Open World Assumption: programs and signature are open-ended.

• NF and embedded implication is particularly problematic (Gabbay [1985]): failure of cut-elimination.

Related Work

• Strict distinction between CWA and OWA predicates; NF for the former, minimal negation for the latter (Harland [1991]).

• A modal approach to account arbitrary extensions of the program as possible worlds (Olivetti & Giordano [1998] for N-Prolog, Bonner [1994] for Hypothetical Datalog).

• Embrace partiality of inductive definitions and use definitional reflection to obtain closure (Schroeder-Heister [1994], McDowell & Miller [1997]).

• Unsatisfactory (for our needs): need to negate OWA predicates, while not extending the language; PID’s technically inadequate for logical frameworks.

Eliminating Negation  1/2

• Our approach is transformational (Sato & Tamaki [1984] Barbuti et al. [1990] for first-order Horn logic and CLP’s):

– Given a clause Q ← G ∧ ¬p(t_{n}) ∧ G′

– a definition of p(x_{n})

⇒ synthesize a positive definition of non p, such that for all ground terms s_{n}:

⊬ p(s_{n}) iff ⊢ non p(s_{n})

• By replacing ¬p with non p, obtain the negation-less clause:

Q ← G ∧ non p(t_{n}) ∧ G′

Eliminating Negation  2/2

• Use classical transformation, such as contraposition, to bring the (completion of the) program to a sort of negation normal form.

• Use an algorithm to complement first-order terms to negate atoms.

• Sketch: the negating the definition of even:

Not_{D}(even(0) ∧ ∀Y :nat. even(s(s(Y))) ← even(Y))

requires the use of term complement Not (0):

Not_{D}(even(0)) = _{M∈Not (0)}^{⋀} ¬even(M) = ∀X:nat. ¬even(s(X))

Eliminating Negation: Benefits  1/2

• Compile-time source-to-source transformation: no run-time overhead.

• No need to extend the language; meta-theory unaltered, since negative information are ‘positivized’.

• No new semantics problems, no incompleteness.

• Proof terms provide evidence for (positivized) negative information.

• User level: adequacy theorem(s) unaltered.

Eliminating Negation: Problems  2/2

• Unfortunately, elimination of negation does not scale immediately to a logical framework such as HHF:

– Intrinsic friction between Closed and Open World Assumption.

– Negation normal forms (and completion-based approaches) are incompatible with the (constructive) operational semantics associated to HHF.

– HHF terms language based on the simply-typed λ-calculus, which is not closed under term complement.

4. Elimination of Negation in a Logical Framework: Part (a) Clause Complement.

• An Example

• The Regular World Assumption • HHF Clause Complement

Example: Encoding the (untyped) λ-calculus

• The language of expressions:

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

• The signature:

exp : type
lam : (exp → exp) → exp
app : exp → exp → exp

• The representation function:

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

Example: (object-level) linear terms

• A lambda term is linear if every functional subterm uses

each of its arguments exactly once:

linapp : linear(app E_{1} E_{2})

← linear(E_{1}) ← linear(E_{2}).

linlam : linear(lam(λx . E x))

← linx(λx . E x) ← (∀x:exp. linear(x) → linear(E x)).

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)).

Complementable Clauses

• Observation: in logical frameworks embedded implications represent scoping constructs, such as abstractions, quantifiers and rules with hypothetical premises.

• Implications paired with intensional universal quantifier to express the parametricity of the assumption.

• Here dynamic assumptions extend the current database in a regular way, so that static and dynamic clauses never overlap (eigenvariable condition).

• Idea: Restrict to programs (called complementable) where every assumption is parametric.

Regular World Assumption  1/2

• A manifestation of the Regular World Assumption: we establish in advance the class of “possible worlds” which programs can end up into.

• A middle ground between programs that cannot make any extension (CWA) and those whose extensions are completely unpredictable (OWA).

• Not covered: for example, the encoding of implication introduction in natural deduction:

nd(A imp B) ← (nd(A) → nd(B)).

• We have shown that this restriction is both elegant and pragmatically adequate (and conservative w.r.t. Horn logic).

Synthesis of the negation of linear  1/3

• An expression is not linear if there is some function which either does not use its argument or uses it more than once.

• An application is not linear if either the first element or the second is not linear: no new problems.

¬linapp : ¬linear(app E_{1} E_{2})

← ¬linear(E_{1}) ∨ ¬linear(E_{2}).

• A lambda expression is not linear if it is not linear in its first argument or if its body is not linear: how to negate a hypothetical and parametric goal?

Synthesis of the negation of linear  2/3

• We mimic a failure derivation to provide a derivation from the negative definition; it needs to mirror failure from assumptions.

• Assumption complementation more complicate than static clause complementation: not all information is available at compile-time.

• Restriction to parametric assumptions allows to complement around parameters, delaying dynamic instantiations as constraints.

• We synchronize clause, assumption and goal complementation (augmentation).

Synthesis of the negation of linear  3/3
linxlm : linx(λx . lam(λy . E x y))

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

• Compute y:exp ⊢ Not α(⊤_{linx}) = ¬linx(λx . y).

• Augment the clause linxlm with y:exp ⊢ Not α(⊤_{linx}):

aug_{D}(linxlm) : linx(λx . lam(λy . E x y))

← (∀y:exp. ¬linx(λx . y) → linx(λx . E x y)).

• Negate the body:

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

4. Elimination of Negation in a Logical Framework: Part (b) Term Complement.

• Higher-Order Term Complement • Strict Types

• Algebra of Simple Terms

Term Complement

• Recall: complement of the head of a clause requires term complement.

• A term M with free variables as the intensional representation of its ground instances, denoted ∥M∥.

• Unification of two terms ‘N = M’ as intersection of their ground instances: ∥N∥ ∩ ∥M∥.

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

• ’Relative Complement’: all the ground instances of a given (finite) set of terms which are not instances of another given one:

{M_{1}, …, M_{n}} − {N_{1}, …, N_{m}}

Higher-Order Term Complement

• Need to extend term complement to the simply-typed λ-calculus, to compute, for example:

1. Not_{D}(linx(λx . x )): not problematic.

2. Not_{D}(linx(λx . app (E_{1} x) E_{2} ) ← linx(λx . E_{1} x))

• Note that the bound variable x does not occur in the (pattern variable) argument E_{2}.

• Common technique: encoding a η-redex, where x ∉ F V (e):

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

Fully vs. Partially Applied Patterns  1/2

• Problem: a pattern (λx.E x) matches any term of appropriate type; (λx.E) matches only ground terms (λx.M) where M does not depend on x.

• The crux of the matter is whether a pattern is fully applied: all bound variables appearing in the binder are mentioned in the scope of a logic variable.

• In (λx . app (E_{1} x) E_{2}), the first argument (E_{1} x) is fully applied, while the second one E_{2} is not.

• Complement of fully applied terms is a simple extension of the first-order case, by keeping track of bound variables.

Fully vs. Partially Applied Patterns  2/2

• The complement of (λx . app (E_{1} x) E_{2}) contains every ground terms (λx.app (M_{1} x) (M_{2} x)), such that M_{2} must use x.

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

• Lugiez [1995] modifies the language of terms to promote constraints to first-class objects. The technical handling of those objects is awkward.

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

Strict Types  1/2

• We internalize strictness as a type system, generalizing the language of simple types 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

• Under the Howard-Curry isomorphism, this yields a relative of the implicational fragment of relevance logic R.

Strict Types  2/2

Labels k ::= 1 | 0 | u
Types A ::= a | 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.

• Typing judgment: Γ; Ω; Δ ⊢ M : A.

• Calculus is well-behaved.

Simple Terms

• We give a complement algorithm that is sound and complete for the natural embedding of the simply-typed λ-calculus:

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

• Partially applied terms are made fully applied with vacuous variables:

(λx . app (E x^{u})( F x^{0} ))

• Complement requires complementing the labels.

Not (λx . app (E x^{u})( F x^{0} )) =

{λx . x, λx . lam(λy . (E′ x^{u} y^{u}))),

λx . app (H x^{u}) ( G x^{1} )}

The Algebra of Simple Terms

• We extend higher-order pattern unification to simple terms in the form of intersection.

• Finite sets of most general unifiers exist.

• From complement and intersection we can define any boolean operations: in particular, the relative complement operation, for M and N finite sets of terms of the same type:

M − N = M ∩ (Not (N))

• The set of finite sets of simple terms (over a signature) as a boolean algebra under set union, pattern intersection and complementation and extensional identity (on sets of ground terms).

Complete definition of ¬linear

¬linapp1 : ¬linear(app F G) ← ¬linear(F).
¬linapp2 : ¬linear(app F G) ← ¬linear(G).
¬linlam1 : ¬linear(lam λx . E x) ← ¬linx(λx . E x).
¬linlam2 : ¬linear(lam λx . E x)
← (∀y:exp. (¬linx(λx . y) ∧ linear(y))
→ ¬linear(E y)).
¬linxap1 : ¬linx(λx . app (F x^{1}) (G x^{1})).
¬linxap2 : ¬linx(λx . app (F x^{0}) (G x^{0})).
¬linxap3 : ¬linx(λx . app (F x^{1}) (G x^{0})) ← ¬linx(λx . F x^{1}).
¬linxap4 : ¬linx(λx . app (F x^{0}) (G x^{1})) ← ¬linx(λx . G x^{1}).
¬linxlm : ¬linx(λx . lam(λy . E x y)) ←

(∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

5. Contributions and Future Work

• A complement algorithm for a useful class of third-order hereditary Harrop formulae

• A relative complement algorithm for higher-order patterns internalized into a strict type theory

Conclusions

• Negation is useful in logical frameworks such as Hereditary Harrop Formulae, but it is difficult to allow.

• We have approached the problem of adding negation by a source-to-source transformation.

• We have found a middle ground between CWA and OWA in the Regular World Assumption.

• We have isolated a significant fragment of HHF, where clause complementation is possible.

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

Future work

• Lift some of the current restrictions (no local variables).

• Extend to dependently typed λ-calculi.

• Implement this pre-compiler to languages as L_{λ}, and possibly to general purpose systems such as Isabelle.

• Investigate the transformational approach to negation in sub-structural calculi and languages (Lolli, Forum, Linear LF).