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@arp.anu.edu.au                       rpg@arp.anu.edu.au
arp.anu.edu/∼jeremy                         arp.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.

2001 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

2001 2

Display Calculus δRA for Relation Algebra

RA: Algebra of binary relations (sets of ordered pairs) over underlying set U Atomic constants: c ::= ⊥ | ⊤ | 1 | 0 (∅ | U × U | identity | diversity) Atomic formulae: p ::= p_{0} | p_{1} | p_{2} | ⋯ (relation symbols) Formulae: A B ::= c | p | ¬A | A ∧ B | A ∨ B | ⌣ A | A ∘ B | A + B

U × U − A ∩ ∪ converse composition

Structure: X Y ::= A | I | ∗X | X , Y | E | •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}

2001 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 ⊢ Y \\ X ⊢ •Y \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}  \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})}

2001 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 ⊤ ¬ ∧ 1 ∼ ∘ Connective I ∗ , E • ; Succedent Part ⊥ ¬ ∨ 0 ∼ +

Example: ∗(p_{0} ; p_{1}) ⊢ ∗ • (p_{1} , p_{3}) ; is + and , is ∧ 2001 5

Display Logic δRA: Structural Rules

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

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

Note: no (M) (P) or (C) rules for ; since ∘/+ are not classical connectives

2001 6

Logical Variation Via Structural Rules (modularity)

An equation A ≤ B is primitive iff A and B are built from relational variables and the constants ⊤ and 1 with the help of ⌣, ∧, ∨ and ∘ only, and if no relational variable appears in A more than once (Kracht96).

reflexivity  seriality  symmetry  transitivity (T) 1 ≤ A  (D) A ∘ ⊤ = ⊤ (B) A = ⌣A  (4) A ∘ B ≤ A ∨ B (T) \frac{X ⊢ Z}{E ⊢ Z}  (D) \begin{matrix}I ⊢ Z \\ X ; I ⊢ Z \end{matrix} (B) \begin{matrix}•X ⊢ Z \\ X ⊢ Z \end{matrix} (4) \frac{X_{1} ⊢ Z X_{2} ⊢ Z}{X_{1} ; X_{2} ⊢ Z}

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.

Theorem: Using results of Kracht 96 we can construct a cut-free display calculus which is sound and complete for any primitive extension of RA.

2001 7

Formalising δRA in Logical Frameworks

Isabelle: Encode the rules directly using the syntax of Isabelle So horizontal line in sequents becomes Isabelle’s ==> Can construct derivations but no term to represent a derivation Cannot reason about derivations

ELF and Isabelle/CTT: Use dependent type theory Have terms to represent derivations But reasoning about derivations is still naive Written up in an ENTCS paper which appeared in 2001

Conclusion: require a deep(er) embedding

2001 8

Formalising δRA in Isabelle/HOL

Formulae: A B ::= c | p | ¬A | A ∧ B | A ∨ B | ⌣ A | A ∘ B | A + B

datatype formula = Btimes formula formula ("_&& _" [68,68] 67)
| Rtimes formula formula ("_oo _" [68,68] 67)
| Bplus formula formula ("_v _" [64,64] 63)
| Rplus formula formula ("_++ _" [64,64] 63)
| Bneg formula ("--_" [70] 70)
| Rneg formula ("_^" [75] 75)
| Btrue ("T")
| Bfalse("F")
| Rtrue ("r1")
| Rfalse("r0")
| PP string
| FV string

2001 9

Formalising δRA in Isabelle/HOL

Structure: X Y ::= A | I | ∗X | X , Y | E | •X | X ; Y

datatype structr = Comma structr structr                  '
| SemiC structr structr                  ;
| Star structr                             *
| Blob structr                             @
| I                                         $I
| E                                         $E
| 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''))

2001 10

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

ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'')
                      ( *@$''Y''; $''X'' |- $''Z'')"

Deep embedding because of the ''X''. Shallow embedding would use ?X.

This means we must handle substitutions explicitly.

2001 11

Formalising Derivations

datatype pftree = Pr sequent rule (pftree list)
                  | Unf sequent

Leaves of successful derivation have form Pr (''A'' |- ''A'') id [] A derived rule will have some Unfinished leaf sequents Now write functions to reason about derivations

IsProvableR :: "rule set => [sequent set, sequent] => bool"
idf_der = "IsProvableR rls {} (?p |- ?p)"
 "IsProvableR rules prems concl == (? pftr.
     allPT (frb rules) pftr & allPT wfb pftr &
     conclPT pftr = concl & set (premsPT pftr) <= prems)"

2001 12

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 ⊤, 1, ⊥, 0

2001 13

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

2001 14

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

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

an ancestor of A is principal if introduced by logical rule (⊢ A) all other ancestors of A are parametric ancestors (including those

“introduced” by weakening there must be at least one introduction of A in every branch not all occurrences of A need be ancestors of this occurrence of A

2001 15

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 parametric ancestors of A with Y ” Suppose Π_{L} does not branch at all for simplicity

\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 2001 16

Putting It All Together

  canElim       :: "(pftree => bool) => bool"
  canElimAll   :: "(pftree => 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”

2001 17

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)"
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)"

If we can eliminate one left-and-right-principal/left-principal/arbitrary cut then we can eliminate any number, one at a time, top down.

Chain of implications canElim (cutIsLRP ?A) ==> canElimAll
(cutIsLRP ?A) ==> canElim (cutIsLP ?A) ==> canElimAll
(cutIsLP ?A) ==> canElim (cutOnFmls ?A)
"canElimAll (cutOnFmls {?A, ?B}) ==> canElim (cutIsLRP (?A v ?B))"
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
     ==> canElim (cutOnFmls {?A v ?B})"

2001 18

Finally ...

"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
     ==> canElim (cutOnFmls {?A v ?B})"

A proof by induction on the structure of a formula 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"

2001 19

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 Have formalised strong-normalisation and have found a bug in (someone else’s) proof Currently writing this up

2001 20

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.

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

Equivalently, no two constituents of the conclusion are congruent to each other.

(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. Such a formula is 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 φ.

2001 22