Embedding Display Calculi into Logical Frameworks

Jeremy E. Dawson ^{⋆} and Rajeev Goré ^{⋆⋆}

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

Australian National University

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

Abstract. We compare several methods of implementing the display (sequent) calculus δRA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for δRA and any associated increase in proof length. We discuss issues arising from this requirement. Keywords: logical frameworks, higher-order logics, proof systems for relation algebra, non-classical logics, automated deduction, display logic.

1 Introduction

Relation algebras [12] are extensions of Boolean algebras; whereas Boolean algebras model subsets of a given set, relation algebras model binary relations on a given set. Thus relation algebras have operations such as relational composition and relational converse. As each relation is itself a set (of ordered pairs), relation algebras also have the Boolean operations such as intersection (conjunction) and complement (negation). Relation algebras form the basis of relational databases [6] and of the specification and proof of correctness of programs.

Display Logic [1] is a generalised sequent framework for non-classical logics, based on the Gentzen sequent calculus [7]. Its advantages include a generic cut-elimination theorem, which applies whenever the rules for the display calculus satisfy certain, easily checked, conditions. It is an extremely general logical formalism, applicable to many (classical and non-classical) logics in a uniform way [10], [20]. The generality of the display framework means that essentially the same meta-level proofs work for many different logics. A rigorous mechanical formalisation of such

⋆ Supported by an Australian Research Council Small Research Grant. ⋆⋆ Supported by an Australian Research Council Queen Elizabeth II Fellowship.

proofs is then widely applicable and worth pursuing. In this paper we discuss the implementation of δRA, a display calculus for relation algebras, as a case study for exploring various methods for such a mechanical formalisation of display calculi in general.

Display calculi extend Gentzen’s language of sequents with extra, complex, n-ary structural connectives, in addition to Gentzen’s sole structural connective, the “comma”. Their defining feature is that in all logical introduction rules, the principal formula is always “displayed” as the whole of the right-hand or left-hand side. There are rules (the “display postulates”) which always enable a given structures to be displayed, as required for using the logical introduction rules. See [9] for a full account.

Isabelle is an automated proof assistant [16]. Its meta-logic is an intuitionistic typed higher-order logic, sufficient to support the built-in inference steps of higher-order unification and term rewriting. Isabelle accepts inference rules of the form “from α_{1}, α_{2}, …, α_{n}, infer β” where the α_{i} and β are expressions of the Isabelle meta-logic, or are expressions using a new syntax, defined by the user, for some “object logic” F. An Isabelle user can encode a particular calculus C_{L} for some object logic L using these rule templates by encoding the set of inference rules for C_{L}. For example, if C_{L} is a natural deduction calculus, then the α_{i} and β will be formulae of L, whereas if C_{L} is a sequent calculus, then the α_{i} and β will be sequents of C_{L}. Such an encoding is called an “object logic”, even though it is a (typically natural deduction or sequent) calculus for some particular logic L. In practice most users would build on one of the comprehensive “object logics” already supplied [17].

Twelf [19] is an implementation of the Edinburgh Logical Framework (LF) [11], which is based on a typed λ-calculus with dependent types. Logics are represented using a judgements as types principle, where each judgement of the form Γ, x : Q ⊢ y : P is identified with the types of its proofs. Twelf also accepts inference rules of the form “from α_{1}, α_{2}, …, α_{n}, infer β”, But now, the rule is expressed as the declaration of a λ-calculus term of type α_{1} → α_{2} → … → α_{n} → β. Once again, if the calculus we are trying to capture is a natural deduction calculus, then the α_{i} and β will be formulae (types), but if the calculus is a sequent calculus, then the α_{i} and β will be sequents (types).

In an earlier paper [4], we described the Isabelle implementation of δRA, a display calculus for relation algebra [9], as an object logic for Isabelle. In that paper we described how we had used the implementation to prove results comparing alternative formalisations of relation algebra from a proof-theoretic perspective. However we had not proved those results themselves in Isabelle. In this paper we describe work done so far towards such a “deep embedding” of δRA. We explored the possibility of implementation in Twelf, Isabelle/CTT and Isabelle/HOL. In the subsequent sections we describe this further work.

2 The Isabelle/Pure implementation

In [4] we described an implementation of δRA which used Isabelle’s Pure theory, so that the only inference rules available were those of δRA. Thus, in the Isabelle implementation of δRA, an Isabelle theorem may be either a simple sequent of δRA, or a sequent rule. Whereas a sequent derivable in δRA becomes an Isabelle theorem of the form X |- Y, a sequent rule becomes an Isabelle theorem containing also the meta-logical operators ==> (implication) or == (equality).

That this is a shallow embedding is reflected in the fact that the horizontal bar of sequent rules becomes the Isabelle ==> operator. In a deep embedding, as in Section 4, the horizontal bar also becomes an object-level constant.

In this shallow embedding, access to and manipulation of the shape of δRA constructs (ie, sequents, structures, formulae) and derivations was provided only at the ML level. For example, in [4] we described having programmed a procedure to perform cut-elimination for δRA. The input to this was a δRA derivation (represented as a tree of sequent rule instances), and the output was a derivation not containing an instance of the cut rule. This required examining the shape of a derivation (represented as a tree of δRA rule instances) and of the Isabelle terms representing sequents. While the shape of an Isabelle term is easily accessible (by ML code), we wrote additional ML code to record a proof in the form of a derivation tree, so that our procedure could examine its shape.

What we aim to do (as described later) is to perform the cutelimination proof entirely within a theorem prover, rather than writing a cut-elimination program in ML. We will therefore need to model derivation trees within the object language of the theorem prover. We would also need to model the set of elementary inference rules of the calculus, so as to be able to say that every rule in a given derivation tree is an instance of one of the inference rules in that calculus.

3 Dependent Type Theory implementations

3.1 Introduction

In a dependent type theory, a type may be parametrised over a type variable and a term variable. This, coupled with the judgements as types principle, where a judgement is identified with the types of its proofs, enables us to express the derivation of a display calculus derived rule.

The Curry-Howard isomorphism, in the simply-typed λ-calculus, identifies terms with proofs and types with propositions. So if A is a type (proposition), and π is a term, then π : A means “π is a derivation of A”.

Dependent types extend what can be done in the simply-typed λcalculus in two distinct ways. Firstly, consider a type I of individuals, and a parametrised type A(i). That is, for each individual i ∈ I, there is a type A(i). Consider a function ρ whose domain is I, such that for each i ∈ I, ρ(i) ∈ A(i). The type of such a function is written ∏ i : I.A(i) denoting how the type of ρ(i) depends on the value of i.

Let A be a predicate, and therefore each A(i) be a proposition taking the value true or false, and let each ρ(i) be a derivation of A(i). That is, ρ is a function which, for each individual i, gives a derivation of A(i); we can think of such a ρ as a derivation of ∀iA(i). At the same time, if we think of each type A(i) as the type “derivations of proposition A(i)”, then the functions ρ of type ∏ i : I.A(i) are the derivations of ∀iA(i).

Secondly, we install an object-logic at the level of terms so that formulae of the object-logic become terms of the dependently-typed λ-calculus. That is, we install a syntax for terms using the connectives of the chosen object logic, and declare a type constructor P (.), so that for each term t, P (t) will mean “derivation of formula t”. This was our approach for modelling δRA where instead of P (t), we used X ⊢ Y, with X and Y being the left and right-hand sides of a sequent.

Regarding a formula t as derivable when we have a term of type P (t) has certain consequences. For example, since from functions of type X → Z, U → V → W and S → S → T we can construct functions of type X → Y → Z, V → U → W and S → T, we unavoidably have weakening, exchange and contraction. However, in our formulation of δRA, these are at the meta-logic level, not in the object logic.

Two theories based on dependent types are the Edinburgh Logical Framework (LF) [11] and Constructive Type Theory (CTT) [13].

3.2 The Twelf implementation

Twelf [19] is an implementation of the Edinburgh Logical Framework (LF) [11]. This is based on a typed λ-calculus with dependent types. Twelf is written in Standard ML, and the user can interact with the system using its “ML Interface”, but only a very limited range of functions is available.

Here is an extract of our Twelf source file.

   1 str : type.
   2 |- : str -> str -> type. %infix none 10 |-.
   3 * : str -> str. %prefix 200 *.
   4 % Display postulates
   5 sA : (* X |- Y) -> (* Y |- X).
   6 sS : (X |- * Y) -> (Y |- * X).
   7 % Derived structural rules
   8 ssASl = [D] sA (sS D). % (X |- * * Y) -> (* * X |- Y)

Line 1 declares str as a new type to represent the δRA structures. Line 2 declares |- as a binary type constructor, taking two term arguments of type str and returning a type. Thus, for structures X and Y, the construct X |- Y represents derivations of the sequent X ⊢ Y. Line 3 declares * as a unary structure operator. Lines 4 and 7 are comments.

In lines 5 and 6 the terms sA and sS (which stand for “star in the antecedent” and “star in the succedent”) are declared with the types that represent derivations of the δRA rules

\frac{∗X ⊢ Y}{∗Y ⊢ X} (sA) \frac{X ⊢ ∗Y}{Y ⊢ ∗X} (sS)

We can think of these declarations as assertions that there are derivations called sA and sS) of these rules, or as defining these as new “primitive” one-step rules.

Now, by treating sA and sS as functions that take a derivation of a sequent to a derivation of another sequent, we can form their composition for some given sequent U ⊢ ∗ ∗ V as below:

derivation of U ⊢ ∗ ∗ V

                    \underrightarrow{sS}

derivation of ∗V ⊢ ∗U

                                     \underrightarrow{sA}

derivation of ∗ ∗ U ⊢ V

The definition of ssSAl does this; the notation means λD.sA(sS D). Twelf computes the type of the function ssSAl, giving (S1 ⊢ ∗∗S2) → (∗∗S1 ⊢ S2). Note that X, Y, S1 and S2 are variables.

Twelf offers Prolog-like [5] queries such as

     ssASl : (X1 |- * * Y1) -> (* * X1 |- Y1).

which searches for a term of the specified type (ie, searches for a derivation of the stated rule) and instantiates ssASl with that term. In this example, because Twelf allows substituting for X1 and Y1 in the query as well as for the variables X and Y in the declarations of sA and sS, the search proceeds along an infinite branch in the wrong direction.

On the other hand, the code

% Using the theorem prover
%theorem
ssASl\_th : exists
  {D:{S1:str} {S2:str} (S1 |- * * S2) -> (* * S1 |- S2)} true.
%prove 2 {} (ssASl\_th D).

successfully uses Twelf’s theorem prover to find the derivation, returning

 /ssASl th/: ssASl th ([S1:str] [S2:str] [X1:S1 |- * * S2]
sA (sS X1)).

(Here the variables S1 and S2 need to be explicitly abstracted over – in the earlier code they were free variables.) Twelf’s theorem prover is not extensively documented.

We found that certain extremely useful aspects of Isabelle are absent from Twelf. Isabelle offers a substantial number of user “commands”, in the form of well-documented ML functions, which enable the user to programme proof procedures, or to examine the shape of a term or type expression. Twelf appears to offer no comparable capabilities to the user. Thus, although the theorem prover did successfully find the derivation above, we felt uncertain that it would be capable of finding all required derivations, particularly as it is stated to be under extensive development.

3.3 The Isabelle/CTT implementation

We then turned to the CTT theory of Isabelle, since it is based on a logic which is very similar to that of Twelf, in that it includes dependent types.

We implemented δRA similarly to its implementation in Twelf, so that we had, for example, (omitting premises of the from ?X : str, which were fairly ubiquitous)

    "sA : * ?X |- ?Y --> * ?Y |- ?X" : thm
   "sA oo sS : ?X |- * * ?Y --> * * ?X |- ?Y" : thm

where oo denotes function composition. We wrote tactics to determine the type of a term variable ?t by solving a goal such as sA oo sS : ?t, corresponding to the derived rule obtained by the given combination of these rules. We explored tactics to search for a term (i.e. proof) of a given type (i.e. sequent), by solving a goal such as the one below, which contains the term variable ?P.

   "?P : ( X |- * * Y) --> ( * * X |- Y)".

The CTT theory of Isabelle is not extensively developed so we found it necessary to prove some fairly elementary though general theorems.

3.4 Conclusions

We experimented with Twelf because we thought we could get our hands on the proofs “for free”. That is, in the course of deriving a sequent or sequent rule, we produce a term which embodies the derivation performed. Given our intention to do a fully mechanised proof of the cut-elimination theorem (in which we manipulate derivations extensively) it had seemed that this feature of Twelf would be useful. Our work with Isabelle/CTT seemed to indicate that the same things could be done in it as in Twelf (with some effort to produce appropriate derived rules and tactics).

However we realised that although we could produce a term which represented the derivation and showed the elementary steps from which it is composed, we could not analyse derivations, in the logic of the theorem prover, in the required ways: for example, to ask which rule was used in the final step of the derivation. In the light of this, there seemed to be no benefit in pursuing an implementation using dependent type theory.

4 The Isabelle/HOL implementation

HOL is an Isabelle theory based on the higher-order logic of Church [3] and the HOL system of Gordon [8]. Thus it includes quantification and abstraction over higher-order functions and predicates. The HOL theory uses Isabelle’s own type system and function application and abstraction: that is, object-level types and functions are identified with meta-level types and functions. Isabelle/HOL contains constructs found in functional programming languages (such as datatype and let) which greatly facilitates re-implementing a program in Isabelle/HOL, and then reasoning about it. However limitations (not found in, say, Standard ML itself) prevent defining types which are empty or which are not sets, or functions which may not terminate.

The work of embedding δRA in Isabelle/HOL is still underway. However it is clear at this stage that the facility for datatype type declarations and associated primitive recursive function definitions is of enormous help. For example, we model δRA structure expressions (see [9]) as below:

datatype structr = Comma structr structr
                 | SemiC structr structr
                 | Star structr
                 | Blob structr
                 | I
                 | E
                 | Structform formula
                 | SV string

The first six lines correspond to the structure operators of δRA and the next line is for “casting” a δRA formula into a δRA structure. The last line had no analogue in the shallow embedding, where an Isabelle variable such as ?S referred to any δRA-structure. In the deep embedding, SV ``X'' will refer to the variable named X appearing in (say) the statement of a rule. We therefore need to define Isabelle/HOL functions which (for example) find all the variables in a structure expression, or substitute a given structure for such a variable. (We wrote such functions for the work described in Section 2, but in Standard ML, not in Isabelle.)

On the other hand, when writing Isabelle tactics which involve analysing the shape of a rule, we can write (for example) (SV Comma ?V ?S) to match any structure expression consisting of two substructures joined by the comma operator of which the first must be a variable. This matching and any related substitution is performed by Isabelle.

For describing the structure of a derivation we have

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

where Pr r pts is a derivation whose last step uses a δRA rule whose instantiation is r, and the premises of that last step are the conclusions of the derivations in the list pts. Unf (“unfinished”) means that a leaf is a sequent which is not an axiom, so is an assumption (or a “premise” of the derivation tree as a whole). We define functions which check that such a structure is a valid derivation (for example, that the premises of a rule really are the conclusions of the trees above, and that each step uses a valid rule and instantiates it correctly). For example, to list the “premises” of the whole derivation tree,

primrec
  "premsPT (Unf seq) = [seq]"
  "premsPT (Pr rule pts) = premsPTs pts"

  "premsPTs [] = []"
  "premsPTs (pt # pts) = premsPT pt @ premsPTs pts"

Each datatype declaration generates a number of theorems which are made available for proofs, and of which some are installed in rule sets used by the more automated proof tactics. These theorems include ones expressing that a datatype type is a disjoint union and that the constructors are 1-1 functions, and one expressing a structural induction principle.

As noted above, this work is still in progress. We still need to specify and reason about derivability and derivation trees; for example, we need to express the requirement that each step of a derivation uses a δRA rule instance of a δRA rule found in a given set. It appears at this stage that the Isabelle/HOL logic is well-equipped for writing specifications which imitate a program written in functional programming style, and for reasoning about the behaviour of that program; Isabelle/HOL seems to offer the capabilities we will require.

5 Conclusion

We have reviewed earlier work in which a shallow embedding of the δRA calculus into the Isabelle/Pure logic, and noted its drawbacks for proving proof-theoretic results in Isabelle itself. Attracted by the notion that the tools based on dependent type theory would give expressiveness about proofs “for free”, we then looked at the Twelf tool. While the Twelf tool is still under active development, we noted how a similar logic is available in Isabelle/CTT, which offers the advantages of Isabelle, such as access to a wide range of documented ML functions for programming proof tactics. However we also found that, while Twelf and Isabelle/CTT facilitate identifying the derivation of a sequent or derived rule, they do not facilitate reasoning about the shape of that derivation, or of the sequents found in it. Thus we turned to Isabelle/HOL, which appears to offer the best facility for deep embedding of a logic such as δRA, and reasoning about derivability, derivation trees and the associated concepts we will need. Needless to say, this was the advice we received from Larry Paulson from the start.

References

1. N D Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982.

2. Boulton, Gordon, Gordon, Harrison, Herbert, and van Tassel. Experience with embedding hardware description languages in hol. In Proceedings of IFIP TC10/WG 10.2, International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129–156. North-Holland/Elsevier, 1992.

3. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

4. J Dawson and R Goré. A mechanised proof system for relation algebra using display logic. In JELIA98:, LNAI 1489:264–278. Springer, 1998.

5. P Deransart, A Ed-Dbali, and L Cervoni. Prolog: The Standard. Springer-Verlag, 1996.

6. Ramez A Elmasri and Shamkant B Navathe. Fundamentals of Database Systems. Benjamin/Cummings, Redwood City, 2 edition, 1994.

7. J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. John Wiley and Sons, 1987.

8. M J C Gordon and T F Melham. Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

9. R Goré. Cut-free display calculi for relation algebras. In CSL96: LNCS 1258:198– 210. Springer, 1997.

10. R Goré. Substructural logics on display. Logic Journal of the Interest Group in Pure and Applied Logic, 6(3):451–504, 1998.

11. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40:143–184, 1993.

12. R D Maddux. Introductory course on relation algebras, finite-dimensional cylindric algebras, and their interconnections. In H. Andreka, J. D. Monk, and I. Nemeti, editors, Algebraic Logic, volume 54 of Colloquia Mathematica Societatis Janos Bolyai, pages 361–392. North-Holland, Amsterdam, 1991.

13. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

14. Anna Mikhajlova and Joakim von Wright. Proving isomorphism of first-order proof systems in hol. In TPHOLS98, LNCS 1479:295–314. Springer, 1998.

15. Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.

16. Lawrence C Paulson. The Isabelle Reference Manual. Computer Laboratory, University of Cambridge, 1995.

17. Lawrence C Paulson. Isabelle’s Object-Logics. Computer Laboratory, University of Cambridge, 1995.

18. Frank Pfennig. Structural cut elimination. In Proc. LICS95, pages 156–166. IEEE Computer Society Press, 1995.

19. Frank Pfennig and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In CADE-16, LNAI 1632:202–206. Springer, 1999.

20. Heinrich Wansing. Displaying Modal Logic, volume 3 of TRENDS IN LOGIC. Kluwer Academic Publishers, Dordrecht, August 1998.