A New Machine-checked Proof of Strong Normalisation for Display Logic

Jeremy E. Dawson and Rajeev Goré

Automated Reasoning Group  Formal Methods Group
Computer Sciences Laboratory  Dept. of Computer Science
Res. Sch. of Inf. Sci. and Eng.  Fac. of Eng. and Inf. Tech.
Institute of Advanced Studies  The Faculties

Australian National University

jeremy@csl.anu.edu.au                       rpg@csl.anu.edu.au
csl.anu.edu/∼jeremy                         csl.anu.edu.au/∼rpg

Goré supported by an Australian Research Council Queen Elizabeth II Fellowship. Dawson supported by an Australian Research Council Large Research Grant.

2003 1

Overview and Motivation

RA: Algebra of binary relations (sets of ordered pairs) over underlying set U

Foundation of relational databases Display Calculi: Generalised sequent framework due to Nuel Belnap

Single cut-elimination proof if rules satisfy 8 easily checked conditions dRA: Display Calculus for the logic of relation algebras Isabelle/HOL: Logical framework that allows us to formalise mathematics Goal: Use Isabelle/HOL to check the strong normalisation proof of Wansing Actual outcome: problem with proof, found and checked a new proof

2003 2

Display Calculus δRA for Relation Algebra

RA: Algebra of binary relations (sets of ordered pairs) over underlying set U Extends classical propositional logic (algebra of sets), we only show classical connectives and rules.

Atomic constants: c ::= ⊥ | ⊤ | …

Atomic formulae: p ::= p_{0} | p_{1} | p_{2} | ⋯ (relation symbols)

Formulae: A B ::= c | p | ¬A | A ∧ B | A ∨ B | …

Structure: X Y ::= A | I | ∗X | X , Y | …

Sequent:  X ⊢ Y  where X is the antecedent and Y is the succedent
Sequent rule:  (name) \frac{X_{1} ⊢ Y_{1} ⋯ X_{n} ⊢ X_{n}}{X ⊢ Y}  \frac{premisses}{conclusion}

2003 3

Display Calculus δRA: Display Postulates

\begin{matrix}∗X ⊢ Y \\ ∗Y ⊢ X \end{matrix} \begin{matrix}X ⊢ ∗Y \\ Y ⊢ ∗X \end{matrix} \begin{matrix}∗ ∗ X ⊢ Y \\ X ⊢ Y \end{matrix}  \begin{matrix}X ⊢ Z , ∗ Y \\ X , Y ⊢ Z \\ Y ⊢ ∗X , Z \end{matrix} \begin{matrix}Z , ∗ Y ⊢ X \\ Z ⊢ X , Y \\ ∗X , Z ⊢ Y \end{matrix}

Theorem (Belnap82): For every sequent X ⊢ Y and every substructure Z of X ⊢ Y, there is a structurally equivalent sequent Z ⊢ Y′ or X′ ⊢ Z that has Z displayed as the whole of its antecedent or succedent.

e.g. \frac{∗p_{3} ⊢ p_{0} , (p_{0} ∧ p_{1})}{∗(p_{0} , (p_{0} ∧ p_{1})) ⊢ p_{3}}  \frac{∗p_{3} , ∗ (p_{0} ∧ p_{1}) ⊢ p_{0}}{∗p_{3} ⊢ p_{0} , (p_{0} ∧ p_{1})}

2003 4

Display Calculus δRA: Logical Rules

Left and right introduction rules for every logical connective

(id) p ⊢ p  (cut) \frac{X ⊢ A A ⊢ Y}{X ⊢ Y}
(∨ ⊢) \frac{A ⊢ X B ⊢ Y}{A ∨ B ⊢ X , Y}  decoding/rewrite  (⊢ ∨) \frac{Z ⊢ A , B}{Z ⊢ A ∨ B}

(∧ ⊢) \frac{A , B ⊢ Z}{A ∧ B ⊢ Z} rewrite/decoding (⊢ ∧) \frac{X ⊢ A Y ⊢ B}{X , Y ⊢ A ∧ B}

Introduced formula is always displayed Gentzen overloading: Antecedent Part ⊤ ¬ ∧ Connective I ∗ , Succedent Part ⊥ ¬ ∨

Example: ∗(p_{0} , p_{1}) ⊢ ∗(p_{1} , p_{3}) means ¬(p_{0} ∨ p_{1}) ⊢ ¬(p_{1} ∧ p_{3}) 2003 5

Display Logic δRA: Structural Rules

A structural rule contains no logical connectives and no formula variables.

(I_{−}^{+} ⊢) \begin{matrix}X , I ⊢ Y \\ X ⊢ Y \\ I , X ⊢ Y \end{matrix}  ^{(⊢ A) \begin{matrix}W ⊢ X , (Y , Z) \\ W ⊢ (X , Y) , Z \end{matrix}}  (⊢ P) \frac{Z ⊢ Y , X}{Z ⊢ X , Y} (M ⊢) \frac{X ⊢ Z}{X , Y ⊢ Z}  (⊢ C) \frac{Z ⊢ X , X}{Z ⊢ X}

Cut Elimination

Theorem [Belnap 82]: Any display calculus whose rules obey eight conditions given by Belnap enjoys cut-elimination. If X ⊢ Y is derivable, then it is derivable without the cut rule.

2003 6

Formalising δRA in Isabelle/HOL

Formulae: A B ::= c | p | ¬A | A ∧ B | A ∨ B | …

datatype formula = Btimes formula formula ("_&& _" [68,68] 67)
| Bplus formula formula ("_v _" [64,64] 63)
| Bneg formula ("--_" [70] 70)
| Btrue ("T")
| Bfalse("F")
| ...
| PP string
| FV string

2003 7

Formalising δRA in Isabelle/HOL

Structure: X Y ::= A | I | ∗X | X , Y | …

datatype structr = Comma structr structr                  '
                   | Star structr                             *
                   | I                                         $I
                   | ...
                   | Structform formula
                   | SV string                                $''X''
datatype sequent = Sequent structr structr                |-
$''X'' |- ''A'' via print-translation and parse-translation
becomes Sequent (SV ''X'') (Structform (FV ''A''))

2003 8

A Deep Embedding of Rules

(name) \frac{X_{1} ⊢ Y_{1} ⋯ X_{n} ⊢ X_{n}}{X ⊢ Y}  \begin{matrix}X ⊢ Y , Z \\ ∗Y , X ⊢ Z \end{matrix}

     datatype rule = Rule (sequent list) sequent
                     | Bidi sequent sequent
                     | InvBidi sequent sequent

     cs1   "cs1 == Bidi ($''X'' |- $''Y'',, $''Z'')
                          (*$''Y'',, $''X'' |- $''Z'')"

Deep embedding of variables – ''X'', not ?X – needed to describe properties of rules (eg Belnap’s eight conditions).

This means we must define substitution explicitly.

A shallow(er) embedding might not model rules at all.

2003 9

Formalising Derivations

datatype dertree = Der sequent rule (dertree list)
                   | Unf sequent

Leaves of successful derivation have form Der (''A'' |- ''A'') id [] A derived rule will have some Unfinished leaf sequents wfb :: "dertree => bool" returns true if the end-sequent of dertree and the end-sequents of its immediate children in dertree list are a well-formed instance of rule

allDT ::  "(dertree => bool) => dertree => bool" returns true if

every node of dertree satisfies the given boolean valued function allDT wfb returns true if every rule application in dertree is well formed allDT (frb rules) returns true if every rule application in dertree is a member of set rules

2003 10

Reducing a Left-and-Right Principal Cut

A cut on A is left- [right-] principal if the left [right] inference immediately above the cut introduces A via a logical rule, written (⊢ A) [(A ⊢)]

Π_{L} (⊢ A) X ⊢ A ^{Π_{R} (A ⊢) A ⊢ Y} X ⊢ Y

C8: All left-and-right principal cuts can be replaced by cuts on strictly smaller subformulae of A

Base Case: (cut) \frac{p ⊢ p p ⊢ p}{p ⊢ p}reduced to just p ⊢ p

Similar cases for ⊤, ⊥

2003 11

Example of a Principal reduction (C8 condition)

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (⊢ ∨) Z ⊢ A ∨ B ^{\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (∨ ⊢) A ∨ B ⊢ X, Y} (cut) Z ⊢ X, Y

Principal cut on formula A ∨ B

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (dp) ∗A, Z ⊢ B \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (cut) ∗A, Z ⊢ Y

(dp) Z ⊢ A, Y

(dp) Z, ∗Y ⊢ A

\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix}

(cut)
Z, ∗Y ⊢ X

(dp) Z ⊢ X, Y

Transformed derivation uses cuts only on A and B

Must exhibit and hard-wire such transformations for every logical connective

So if cut is not left-and-right principal then we try to make it so ...

2003 12

A Parametric Reduction — making a cut left-right-principal

Given a derivation ending in a non left-and-right principal cut on formula A,

we trace the ancestor occurrences of this A up Π_{L}: Let Π[A := Y] mean “replace all (non-principal) ancestors of A with Y ”

\begin{aligned}Π_{L}^{1} & (⊢ A) & V ⊢ A \\ & (π) \\ Π_{L}^{2} \end{aligned} ; (ρ) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{1} (⊢ A) V ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V ⊢ Y \\ & (π) \\ Π_{L}^{2}[A := Y] \end{aligned} ; (ρ) ; X ⊢ Y

New cut is left-principal (similarly make it also right principal) If Π_{L} branches (A introduced at multiple places), more complex (!)

If Π_{L}^{1} is empty, A introduced by A ⊢ A, no new cuts needed. 2003 13

Strong Normalisation

Cut-admissibility proceeds by eliminating the top-most cut Strong normalisation: define reduction steps, eliminate any cut that can be reduced, and prove that this cut-elimination procedure terminates: Π_{n} < Π_{n−1} < ⋯ < Π_{2} < Π_{0} Π_{n} is cut-free n is finite weak-normalisation (attacking top most cut) is an instance of this method Usually define reductions as either a parametric or principal move, with proviso that we must not cross a cut in a parametric move

2003 14

Why Formalise (in Isabelle) ?

Strong-normalisation proofs are notoriously difficult involving many cases We tried to formalise Heinrich Wansing’s proof of strong-normalisation for display logic, but got stuck at one particular case Found a problem ... Wansing assumes that Π_{L}^{1} is unchanged!

V_{A} is (∗A , X) V_{Y} is (∗Y , X)

\begin{matrix}Π_{L}^{1} & (⊢ A) & V_{A} ⊢ A \\ (dp) \\ X ⊢ A, A \end{matrix} ; (ctr) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{′1} (⊢ A) V_{Y} ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V_{Y} ⊢ Y \\ & (dp) \\ X ⊢ Y, Y \end{aligned} ; (ctr) ; X ⊢ Y

2003 15

Branch in left subtree — before and after

Π′ (intro-A) X′ ⊢ A ^{Π′′ (intro-A) X′′ ⊢ A} (π) Π_{L}

(ρ) X ⊢ A

\begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix}

(cut)
X ⊢ Y

\begin{matrix}Π′ \\ X′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′ ⊢ Y ^{\begin{matrix}Π′′ \\ X′′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′′ ⊢ Y} (π) Π_{L}[A?= Y]

(ρ) X ⊢ Y

2003 16

Two successive introductions – before

Π  (ρ) X, B ⊢ ∗B

(⊢ ¬) X, B ⊢ ¬B

(dp) ∗¬B, X ⊢ ∗B

(⊢ ¬) ∗¬B, X ⊢ ¬B

(dp) X ⊢ ¬B, ¬B

(⊢ cont) X ⊢ ¬B

\begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix}

(cut)

X ⊢ Y 2003 17

Two successive introductions – after

\begin{aligned}\begin{aligned}Π & (ρ) & X, B ⊢ ∗B \\ & (⊢ ¬) \\ X, B ⊢ ¬B \end{aligned} & \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} & (cut) & X, B ⊢ Y \\ & (dp) \\ ∗Y, X ⊢ ∗B \end{aligned} ; (⊢ ¬) ; ∗Y, X ⊢ ¬B\begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} (cut) ∗Y, X ⊢ Y

(dp) X ⊢ Y, Y

(⊢ cont) X ⊢ Y

2003 18

Various Binary Orderings

1. Π_{1} <_{LRP} Π_{0} if the bottom inferences of derivations Π_{1} and Π_{0} are both cut, and either

a. the cut in Π_{1} is left-principal or right-principal, and the cut in Π_{0} is neither, or

b. the cut in Π_{1} is (left- and right-)principal, and the cut in Π_{0} is not (leftand right-)principal.

2. Π_{1} <_{cut} Π_{0} if the bottom inferences of derivations Π_{1} and Π_{0} are both cut, and if either

a. the size of the cut-formula of Π_{1} is smaller than that of Π_{0}, or

b. each derivation has the same cut-formula, and Π_{1} <_{LRP} Π_{0}.

2003 19

Various Binary Orderings

1. Π_{1} <_{sn1} Π_{0} if Π_{0} and Π_{1} are the same except that one of the immediate subtrees of Π_{0} is strongly normalisable and reduces to the corresponding immediate subtree of Π_{1}.

2. Π_{1} <_{dt} Π_{0} iff any of the following hold:

a. the bottom inference of Π_{1} is not cut, but that of Π_{0} is

b. Π_{1} <_{cut} Π_{0}

c. Π_{1} <_{sn1} Π_{0}.

Theorem 1 The relations LRPorder, cutorder, sn1order, and dtorder

are well-founded

Despite notation, these relations are not reflexive, and some are not transitive.

Intuitively, (Π_{1}, Π_{0}) ∈ dtorder means that Π_{1} is closer to being cut-free (in some sense) than is Π_{0}.

2003 20

Inheriting Strong Normalisation

We next define snHered, a property of derivation trees which indicates that a tree inherits strong normalisation from its immediate subtrees. Definition 1 Π satisfies snHered iff: if all the immediate subtrees of Π are strongly normalisable then Π is strongly normalisable.

   snHered_def = "snHered ?dt ==
      set (nextUp ?dt) <= sn_set --> ?dt : sn_set"

Lemma 1 A derivation tree Π is strongly normalisable iff every subtree of Π has the property snHered.

2003 21

Key Properties of Reductions

When we apply a reduction to a cut at the bottom of a tree Π_{0}, obtaining Π_{1}, then every subtree Π_{1}^{s} of Π_{1} which has cut at the bottom satisfies one of

Π_{1}^{s} is a proper subtree of Π_{0}, or

Π_{1}^{s} <_{cut} Π_{0}, because

(principal reduction) the cut-formula of Π_{1}^{s} is smaller than that of Π_{0}

(parametric reduction) Π_{1}^{s} and Π_{0} have the same cut-formula and Π_{1}^{s} <_{LRP} Π_{0}.

2003 22

Strong-Normalisation

Lemma 2 For a given derivation Π_{0}, if all derivation trees Π′ <_{dt} Π_{0} have the property snHered, then so does Π_{0}.

dth = "ALL dt'. (dt', ?dt) : dtorder --> snHered dt'
        ==> snHered ?dt" : thm

Proof: The machine-proof is quite complicated, and a careful examination of it highlights why the definition of dtorder needs to be so complex. Theorem 2 Every derivation tree is strongly normalisable.

   all_snH = "snHered ?dt"     : thm
   all_sn  = "strongNorm ?dt" : thm

Proof: By well-founded induction, it follows from Lemma 2 that every derivation tree satisfies snHered; the result follows from Lemma 1.

2003 23

Where are we?

We have actually shown using Isabelle that a class of reductions which we

have defined is (small enough to be) strongly normalising. We would like to show that this class of reductions is correctly defined, ie, it

(is large enough that it) contains the reductions used by Wansing. We can show that it is large enough to ensure cut-elimination. This guards

against the worst definition errors. We do this by showing that any tree containing a cut admits at least one

reduction in this class. Strong normalization then gives cut-elimination.

2003 24

Belnap’s Conditions and New C8

Appendix: Belnap’s Conditions.

For every sequent rule Belnap82, page 388 first defines the following notions: in an application Inf of a sequent rule (ρ), “constituents occurring as part of occurrences of structures assigned to structure-variables are defined to be parameters of Inf ; all other constituents are defined as nonparametric, including those assigned to formula-variables. Constituents occupying similar positions in occurrences of structures assigned to the same structure-variable are defined as congruent in Inf ”. The eight (actually seven) conditions shown below are from [Kracht96]:

(C1) Each formula which is a constituent of some premiss of a rule ρ is a subformula of some formula in the conclusion of ρ.

(C2) Congruent parameters are occurrences of the same structure.

2003 25 (C3) Each parameter is congruent to at most one constituent in the conclusion.

Equivalently, no two constituents of the conclusion are congruent.

(C4) Congruent parameters are either all antecedent parts or all succedent parts of their respective sequent.

(C5) If a formula is non-parametric in the conclusion of a rule ρ, it is either the entire antecedent, or the entire succedent (called a principal formula).

(C6/7) Each rule is closed under simultaneous substitution of arbitrary structures for congruent parameters.

(C8) If there are inference rules ρ_{1} and ρ_{2} with respective conclusions X ⊢ φ and φ ⊢ Y with φ principal in both inferences (in the sense of C5), and if (cut) is applied to yield X ⊢ Y then, either X ⊢ Y is identical to X ⊢ φ or to φ ⊢ Y; or it is possible to pass from the premisses of ρ_{1} and ρ_{2} to X ⊢ Y by means of inferences falling under (cut) where the cut-formula is always a proper subformula of φ.

2003 26