The Transformational Approach to Negation

in a Logical Framework Alberto Momigliano Carnegie Mellon University

• Logical Frameworks

• Negation in a Logical Framework • Modified Closed World Assumption • Term Complement

• Future Work

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:

– Type systems.

– Operational semantics.

– 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. Applications as a teaching and research tool include:

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

– Implementation of algorithms (evaluation, type inference).

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

Systems

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

• Environments: interactive theorem proving vs. logic programming and proof-checkers.

• Implementations: Isabelle, λProlog, Elf, Maude, Pi…

• Applications: Mobile Code Security (Proof-Carrying Code) and Certifying Compilation (Necula), Protocol Security Verification (Paulson)…

Logical Framework’s Design

• Logical frameworks are weak by design to facilitate: – Informal proofs of adequacy of representation.

– Effective checking of the validity of derivations.

– Proof-search and unification.

– Efficient implementations.

• Extending a logical framework: balance benefits against complications in its meta-theory.

• Extensions: subtyping, modularity, equational reasoning, linearity… What about having negation?

Our Contribution: Adding Negation  1/2

In specifications, negation is often used.

• In Prolog, obtain odd(n) from ¬even(n).

• Two elements are different, an element is not a member of a list.

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

• Functional program analysis: a function is not linear.

• Operational semantics: an expression is not a value.

• Algorithmic subtyping: a sort is not a subsort (of another).

Our Contribution: Adding Negation  2/2

• Lf’s with logic programming interpretation have no negation operator.

• Need to explicitly program the negative code (tedious and error-prone).

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

• Our result: automation of this synthesis of negative information.

• Benefits: a sound negation operator allows us to implement topics too unwieldy to deal with otherwise.

Negation-as-Failure: Horn case  1/3

• NF is the usual answer in logical programming:

P infers ¬A if A finitely fails from P

• Not declarative, but easy to implement.

• Possibly unsound and generally incomplete: semantics?

• Closed World Assumption: Horn Logic ∼ inductive definitions: everything which is not provable from a program is assumed to be false.

• Allowing negation in clauses spoils their inductive nature.

Negation-as-Failure: Lf’s case  2/3

• Even in a well-behaved fragment, NF in the meta-language makes adequacy theorems too complicated (provability and unprovability).

• Lf’s not inductive definitions, because of embedded implication and universal quantifiers:

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.

Between CWA and OWA

• Intrinsic tension between CWA and OWA.

• Both assumptions represent too extreme poles.

• Is there is a middle ground where negation is meaningful?

• We need to identify a class of “possible worlds” which are stable under extensions of the program and signature.

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: need to negate OWA predicates, while not extending the language; PID’s technically inadequate for Lf’s.

Transforming Negation  1/3

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

Given a clause Q ← G, ¬p, G′ a definition of p synthesize a positive definition of non p, such that

⊬ p iff ⊢ non p

Replace non p in p: Q ← G, non p, G′

• Technically:

– Bring the program in negation normal form.

– Need an algorithm to complement terms (Lassez [1987]) to negate atoms.

Transforming Negation: Benefits  2/3

• Compile-rime source-to-source transformation.

• No need to extend the language; negative information are ‘positivized’.

• No new semantics problems, no floundering, no incompleteness.

• Proof terms provide evidence for negative information.

• Adequacy theorem(s) unalterated.

Transforming Negation: Problems  3/3

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

– Same friction between Closed and Open World Assumption.

– Negation normal forms 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.

Our Solution: Modified CWA  1/2

• Modified CWA: restrict to programs whose dynamic assumptions extend the current database in a regular way, so that static and dynamic clauses never overlap.

• Observation: in Lf’s 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.

• The eigenvariable condition ensures no overlap.

• A program is deniable if every assumption is parametric.

Modified CWA  2/2

• Example: checking whether a λ-term is closed:

\begin{matrix}ΠE:exp. closed(lam E) ← Πx:exp. closed(x) → closed(E x). \\ ΠE_{1} :exp. ΠE_{2} :exp. closed(app E_{1} E_{2}) ← closed(E_{1}) ∧ closed(E_{2}). \end{matrix}

• Not allowed: encoding of implication introduction in natural deduction:

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

• If implication is not parametric, need to explicitly manage assumptions as lists (see McDowell& Miller [1997]).

• Our restriction has shown to be both elegant and pragmatically adequate (and conservative w.r.t. Horn logic).

Negation Normal Forms

• Operational semantics of embedded implication is intuitionistic.

• No negation normal forms available in intuitionistic logic.

• Strong negation normal form (Nelson [1949]) incompatible with semantic of failure:

¬(D → G) = D → ¬G

• Valid for deniable programs.

Term Complement  1/2

• λx.x is an instance of λx.E x

• λx.y in an instance of λx.E, where E does not depend on x.

• The complement of λx.E is the set of all terms that does depend on x.

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

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

Term Complement  2/2

• We internalize strictness as a type system, generalizing the language of simple types to include:

– strict functions of type A →^{1} B, guaranteed to depend on their argument

– invariant functions of type A →^{0} B, guaranteed not to depend on their argument

– the uncommitted function space A →^{u} B.

• We embed the simply-typed calculus.

• In this system we can perform any boolean operation on finite sets of patterns (unification as intersection).

Conclusions

• Negation is useful in Lf’s, but it is difficult to allow.

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

• We have found a middle ground between CWA and OWA.

• We have isolated a significant fragment of HHF, where program negation 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), related to question of extensionality in Lf’s.

• Extend to dependently typed λ-calculi.

• Implement this pre-compiler to languages as λProlog, Elf, and possibly to general purpose systems such as Isabelle.

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