Formalising Cut-elimination for the Display Calculus of Relation Algebras

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.

2002 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 cut-elimination proof of Belnap Case study: Check it for dRA and then generalise

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

2002 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})} \frac{∗p_{0} , p_{3} ⊢ p_{0} ∧ p_{1}}{∗p_{3} ⊢ p_{0} , (p_{0} ∧ p_{1})}

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

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

2002 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

2002 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''))

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

2002 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

2002 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 ⊤, ⊥

2002 11

Example of 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 ...

2002 12

Making a cut left-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 If Π_{L} branches (A introduced at multiple places), more complex

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

Making a cut (left-and-right-)principal

Similarly to make a left-principal cut also right principal But note, one cut ⇝ several cuts (in general) Summing up:

single non-principal cut ⇝ several left-principal cuts
single left-principal cut ⇝ several principal cuts
single principal cut ⇝ several cuts on sub-formulae

To deal with several left-and-right-principal/left-principal/arbitrary cuts, deal

with a top-most one first (sub-tree containing single cut) Procedurally, this is a deeply nested recursion. Is an equally deeply nested inductive proof necessary?

2002 14

Cut-Admissibility By Structural Induction

elim eliminates a single arbitrary top-most cut, by turning it into several

left-principal cuts and using elimAllLP to eliminate them … elimAllLP eliminates several left-principal cuts, by repeatedly using elimLP

to eliminate the top-most remaining one … elimLP eliminates a top-most left-principal cut, by turning it into several

principal cuts and using elimAllLRP to eliminate them … elimAllLRP eliminates several principal cuts, by repeatedly using elimLRP

to eliminate the top-most remaining one … elimLRP eliminates a top-most principal cut, by turning it into several cuts on

smaller cut-formulae, and using elimAll to eliminate them … elimAll eliminates several arbitrary cuts, by repeatedly using elim to

eliminate the top-most remaining one … termination 2002 15

Putting It All Together

  canElim       :: "(dertree => bool) => bool"
  canElimAll   :: "(dertree => bool) => bool"

canElim f means that if a derivation tree pt has no cuts other than at the bottom, and satisfies f, then there is an equivalent cut-free derivation tree.

canElimAll f means that if every subtree of a given tree pt satisfies f, then there is a cut-free derivation tree pt' equivalent to pt (we also require that if the bottom rule of pt is not (cut), then the bottom rule of pt' is the same).

allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})"

Here f is (cutIsLP ?A) [(cutOnFmls {?A})] which means that if the lowest rule application is cut then it is a left-principal cut with cut formula ?A [if the lowest rule application is cut then the cut formula is from set {?A}]

allLP' means “if you can eliminate several cuts, all left-principal on A, then you can eliminate a single cut, at the bottom, on A” (its backwards!)

2002 16

Putting It All Together ...

allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})"
allLRP' = "canElimAll (cutIsLRP ?A) ==> canElim (cutIsLP ?A)"
elimLRP = "canElim (cutIsLRP ?A) ==> canElimAll (cutIsLRP ?A)"
elimLP = "canElim (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)"

Chaining these implications gives

canElim (cutIsLRP ?A) ==> canElim (cutOnFmls ?A)

Dealing with left-right-principal cuts gives

canElimAll (cutOnFmls {?A, ?B}) ==>
    canElim (cutIsLRP (?A v ?B))
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)"
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
     ==> canElim (cutOnFmls {?A v ?B})"

2002 17

Finally ...

A proof by induction on the structure of a formula then gives

canElimFml = "canElim (cutOnFmls {?fml})"

(“you can eliminate one cut on any given formula fml”),

canElimAny = "canElim (cutOnFmls UNIV)",

(“you can eliminate one cut whatever the cut-formula”), and, using elimFmls,

canElimAll = "canElimAll (cutOnFmls UNIV)"

Finally we convert canElimAll into

cutElim = "IsProvableR rls {} ?concl  ==>
             IsProvableR (rls - {cut}) {} ?concl"

2002 18

Further Work

Our cut elimination theorem is quite naive: eliminate top-most cut. Strong normalisation: define reduction steps, eliminate any cut that can be reduced, and prove that this cut-elimination procedure terminates: Π_{0} > Π_{1} > Π_{2} > ⋯ > Π_{n} Π_{n} is cut-free n is finite (i.e. > is well-founded) top most cut method is an instance of this method Found a bug in Wansing’s proof Found new proof and formalised it

2002 19

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.

2002 20 (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 φ.

2002 21