%% %% \documentclass[a4paper,11pt]{llncs} %\usepackage{makeidx} %\usepackage{acmnew-xref} \usepackage{latexsym} \usepackage{amssymb} %\usepackage{exptrees} \renewcommand{\today}{\number\day\ \ifcase\month\or January\or February\or March\or April\or May\or June\or July\or August\or September\or October\or November\or December\fi \ \number\year} %\setlength \parskip {1.0ex} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Preamble \title{Embedding Display Calculi into Logical Frameworks} \author{Jeremy E. Dawson \thanks{Supported by an Australian Research Council Small Research Grant.} \and Rajeev Gor\'e \thanks{Supported by an Australian Research Council Queen Elizabeth II Fellowship.}} % \institute{Department of Computer Science and % Automated Reasoning Group, % Computer Sciences Laboratory, \\ % Australian National University, % Canberra ACT 0200, Australia \\ % \texttt{jeremy@csl.anu.edu.au} \ \ % \texttt{rpg@csl.anu.edu.au} %\\[1ex] %Tel: +61-2-6249-5138 \ \ Fax: +61-2-6249-0010 % } \institute{ \begin{tabular*}{0.8\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 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.\ \\ \end{tabular*}\\ Australian National University \\ \begin{tabular*}{0.8\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} \texttt{jeremy@csl.anu.edu.au} & \texttt{rpg@csl.anu.edu.au} \end{tabular*} } \date{\today} \newcommand\cfile{} %\renewcommand{\thepage}{\roman{page}} \newcommand\shrinklist[1]{ \setlength\parskip{#1\parskip} \setlength\itemsep{#1\itemsep} \setlength\itemindent{#1\itemindent} \setlength\topsep{#1\topsep} } \newcommand\comment[1]{} \newcommand\invrule[2]{ % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline \hline $ #2 $ \end{tabular}} \newcommand\slrule[2]{ % similar to \frac, except % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline $ #2 $ \end{tabular}} %\newcommand\proof{\noindent\textbf{Proof.}} \newcommand\src[1]{source file \texttt{#1}} \newcommand\apsrc[1]{Appendix \ref{app:code}} %\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})} \newcommand\seesrc[1]{(see source file \texttt{#1})} %\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})} \newcommand\insrc[1]{in source file \texttt{#1}} \newcommand\page[1]{page~\pageref{#1}} \newcommand\fig[1]{Fig.~\ref{fig:#1}} \newcommand\ch[1]{Chapter~\ref{ch:#1}} \newcommand\tbl[1]{Table~\ref{tbl:#1}} \newcommand\thrm[1]{Theorem~\ref{thrm:#1}} \newcommand\lem[1]{Lemma~\ref{lem:#1}} \newcommand\ttl[1]{\tti{#1}\label{#1}} \newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}} \newcommand\ttdef[1]{\texttt{#1}\tti{#1}} \newcommand\tti[1]{\index{#1@\texttt{#1}}} \newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}} \newcommand\dRA{{\boldmath $\delta$}\textbf{RA}} \newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}} \newcommand\NRA{\textbf{NRA}} \newcommand\RA{\textbf{RA}} %\newcommand\M{$\mathcal M$} \newcommand\M{\ensuremath{\mathcal M}} \newcommand\Mp{$\mathcal M'$} \newcommand\up[1]{\vspace{-#1ex}} \newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree \newcommand\1{\textbf 1} \newcommand\0{\textbf 0} % automatically defined in LLNCS style %\newtheorem{thm}{Theorem}%[chapter] %\newtheorem{lemma}[thm]{Lemma} %\newtheorem{defn}[thm]{Definition} %\newtheorem{cor}{Corollary}[thm] %\renewcommand\thecor{\thethm(\arabic{cor})} \pagestyle{plain} \raggedbottom \begin{document} %% Title \maketitle \begin{abstract} We compare several methods of implementing the display (sequent) calculus \dRA\ 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 \dRA\, and any associated increase in proof length. We discuss issues arising from this requirement. % %We then show how the implementation can be used to prove results comparing %alternative formalisations of relation algebra %from a proof-theoretic perspective. \\[1ex] \textbf{Keywords:} logical frameworks, higher-order logics, proof systems for relation algebra, non-classical logics, automated deduction, display logic. \end{abstract} \sloppy %\newpage %% Here begins the main text \section{Introduction} Relation algebras \cite{maddux-introductory} 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 \cite{elmasri-navathe-database} and of the specification and proof of correctness of programs. Display Logic \cite{belnap-display} is a generalised sequent framework for non-classical logics, based on the Gentzen sequent calculus \cite{gallier-logic}. %It can be applied to give syntactic proof systems for various logics. 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 \cite{gore-sld-igpl}, \cite{wansing-displaying-modal-logic}. 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 proofs is then widely applicable and worth pursuing. In this paper we discuss the implementation of \dRA, a display calculus for relation algebras, as a case study for exploring various methods for such a mechanical formalisation of display calculi in general. \comment{ Display calculi resemble the Gentzen sequent calculus \textbf{LK}, but with significant differences. For example, the rules for introducing the connective `$\lor$' (on the right) in \textbf{LK} and some display calculi are \label{|-v} $$\frac {\Gamma \vdash \Delta, P, Q} {\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor ) \qquad \textrm{ and } \qquad \frac {X \vdash P , Q} { X \vdash P \lor Q}(\mbox{DC-}\vdash \lor ) $$ Whereas, in \textbf{LK}, $\Gamma$ and $\Delta$ denote comma-separated lists of formulae, in a display calculus, $X$ denotes a \emph{structure}, which can involve several \emph{structural} connectives (one of which is `,'). A structure can be either a \emph{formula} (such as $P$ or $P \lor Q$) or the result of a structure operator acting on smaller structure(s) (such as $P , Q$). Display calculi extend the Gentzen calculus with extra structural connectives, such as `*' (meaning negation) and, for \dRA, operators with relational meanings. } 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''. \comment{ Whereas Gentzen assumed the comma to be associative, commutative and inherently poly-valent, display calculi make no such implicit assumptions. Properties such as these are explicitly stated as structural rules. For example, \dRA-sequents are built using a binary comma, a binary semicolon, and unary $*$ and $\bullet$ structural connectives. Thus, whereas Gentzen's sequents $\Gamma \vdash \Delta$ assume that $\Gamma$ and $\Delta$ are comma-separated lists of formulae, \dRA-sequents $X \vdash Y$ assume that $X$ and $Y$ are complex tree-like structures built from formulae together with comma, semicolon, $*$ and $\bullet$. The defining feature of display calculi is that in all logical introduction rules, the principal formula is always ``displayed'' as the whole of the right-hand or left-hand side. For example, the rule $(\mbox{\textbf{LK}-}\vdash \lor )$, shown below left, is typical of Gentzen's sequent calculi like \textbf{LK}, while the rule $(\mbox{\dRA-}\vdash \lor )$ shown on the right is typical of display calculi: $$\frac {\Gamma \vdash \Delta, P, Q} {\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor ) \qquad \qquad \frac {X \vdash P , Q} { X \vdash P \lor Q}(\mbox{\dRA-}\vdash \lor ) $$ Intuitively, to use this display calculus rule downwards on a sequent $X' \vdash Y'$, everything other than $(P,Q)$ %that ``belongs on the right of $\vdash$'' must be moved into the complex structure $X$ on the left of $\vdash$, thereby displaying the structure $(P,Q)$ as the whole of the right-hand side. There are rules which always enable this to be done. After the rule application we can ``undisplay'' the moved material back to its original position, so that the sole purpose of this rule is to ``rewrite'' some $(P,Q)$ to $P \lor Q$ somewhere inside $Y'$. } 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 \cite{gore-relalg} for a full account. Isabelle is an automated proof assistant \cite{isabelle-ref}. Its meta-logic is an intuitionistic typed higher-order logic, % and typed $\lambda$-calculus, sufficient to support the built-in inference steps of higher-order unification and term rewriting. Isabelle accepts inference rules of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$'' where the $\alpha_i$ and $\beta$ are expressions of the Isabelle meta-logic, or are expressions using a new syntax, defined by the user, for some ``object logic'' $\mathcal F$. An Isabelle user can encode a particular calculus $\mathcal C _L$ for some object logic $\mathcal L$ using these rule templates by encoding the set of inference rules for $\mathcal C _L$. %This is supplemented with the user's choice of %object logic in which to perform proofs. For example, if $\mathcal C _L$ is a natural deduction calculus, then the $\alpha_i$ and $\beta$ will be formulae of $L$, whereas if $\mathcal C _L$ is a sequent calculus, then the $\alpha_i$ and $\beta$ will be sequents of $\mathcal C _L$. Such an encoding is called an ``object logic'', even though it is a (typically natural deduction or sequent) \emph{calculus} for some particular logic $L$. In practice most users would build on one of the comprehensive ``object logics'' already supplied \cite{isabelle-object}. Twelf \cite{pfennig-schurmann-twelf} is an implementation of the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}, which is based on a typed $\lambda$-calculus with dependent types. Logics are represented using a \emph{judgements as types} principle, where each judgement of the form $\Gamma, x : Q \vdash y : P$ is identified with the types of its proofs. Twelf also accepts inference rules of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$'', But now, the rule is expressed as the declaration of a $\lambda$-calculus term of type $\alpha_1 \to \alpha_2 \to \ldots \to \alpha_n \to \beta$. Once again, if the calculus we are trying to capture is a natural deduction calculus, then the $\alpha_i$ and $\beta$ will be formulae (types), but if the calculus is a sequent calculus, then the $\alpha_i$ and $\beta$ will be sequents (types). In an earlier paper \cite{dawson-gore-dra-jelia98}, we described the Isabelle implementation of \dRA, a display calculus for relation algebra \cite{gore-relalg}, 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 \emph{in} Isabelle. \comment{ in the sense we now explain. Suppose we have a logic $L$ (in the sense of %, a set of well-formed formulae, and a subset of these, the theorems), a set of formulae which we regard as valid with respect to some semantics) and two calculi $\mathcal P$ and $\mathcal Q$ for $L$ (each consisting of axioms and inference rules). Further suppose that we have mechanical implementations of $\mathcal P$ and $\mathcal Q$. Then one can use the implementation of $\mathcal P$ to derive in $\mathcal P$ every axiom and rule of $\mathcal Q$. One could then go outside the mechanical system and argue (by induction on the size, or on the structure, of a $\mathcal Q$-derivation) that therefore every $\mathcal Q$-derivable object (typically a formula or sequent) is also $\mathcal P$-derivable. The results referred to in \cite{dawson-gore-dra-jelia98} were proved in this manner. An alternative and, when one's aim is the mechanical proof of proof-theoretical results, better, approach would be one which enabled the inductive argument above to be carried out in the mechanical theorem-prover. This would require a different style of implementation of the calculi $\mathcal P$ and $\mathcal Q$ in the prover, so as to enable reasoning about the shape and form of $\mathcal P$-derivations and $\mathcal Q$-derivations. Typically this would require modelling, in the theorem prover, the ``tree'' of steps used in a derivation and the fact that each step is an instance of a rule of the calculus $\mathcal P$ or $\mathcal Q$; this in turn requires modelling the form of the statement of an inference rule of $\mathcal P$ or $\mathcal Q$, and a method of obtaining particular substitutional instances of such rules of inference. %and substitution of a term for a variable in it. The terms ``shallow embedding'' and ``deep embedding'' are often used to distinguish these styles of implementation \cite{boulton-et-al-hdl}. } % In this paper we describe work done so far towards such a ``deep embedding'' of \dRA. We explored the possibility of implementation in Twelf, Isabelle/CTT and Isabelle/HOL. In the subsequent sections we describe % the original Isabelle/Pure implementation and this further work. \section{The Isabelle/Pure implementation} \label{pure} \comment{ Isabelle is an interactive computer-based proof system, described in \cite{isabelle-ref}. Its capabilities include higher-order unification and term rewriting. It is written in Standard ML \cite{ML-definition}; when it is running, the user can interact with it by entering further ML commands, and can program complex proof sequences in ML. As stated previously, the basic Isabelle constructs available to a user include inference rule templates of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''. These can be used ``forwards'', to obtain $\beta$ from the $\alpha_i$, or ``backwards'', to reduce a given goal $\beta$ to subgoals $\alpha_1, \alpha_2, \ldots, \alpha_n$. Isabelle provides a number of basic operations for backwards proof and proof-search (\emph{tactics}\index{tactic|textbf}), as well as \emph{tacticals}\index{tactical|textbf} for combining these. %Isabelle automatically keeps track of the subgoals generated by this backward %search procedure and the user can choose to work on any subgoal. %The user can also write complex proof tactics in ML; %many complex tactics and tacticals are supplied with %Isabelle or its standard object logics. Isabelle also supports forward proof. The inference rules collectively form a simple meta-logic: an intuitionistic typed higher-order logic. %typed $\lambda$-calculus. There are three logical operators: \texttt{==>} (implication, or deducibility), \texttt{==} (equality, or substitutability), and \texttt{!!} (universal quantification). For example, \mbox{\texttt{[| A1; A2 |]~==>~B}}, which is an abbreviation for \texttt{A1 ==> (A2 ==> B)}, is the Isabelle representation for ``from $\alpha_1, \alpha_2, \mbox{ infer } \beta$''. These operators satisfy certain properties arising from their intended meanings. For example, since %the Isabelle proposition \mbox{\texttt{[| A1; A2 |]~==>~B}} means that $\beta$ can be deduced from $\alpha_1$ and $\alpha_2$, % and can be proved by deducing $\beta$ % from $\alpha_1$ and $\alpha_2$, % we have that % \mbox{\texttt{[|~(A~==>~B);~A~|] ==> B},} % and that it should also be possible to deduce $\beta$ from $\alpha_2$ and $\alpha_1$. Indeed, using Isabelle, we can prove a new rule, shown below, that states ``if (from $\alpha_1, \alpha_2, \mbox{ infer } \beta$) is a rule, then (from $\alpha_2, \alpha_1, \mbox{ infer } \beta$) is a rule''. {\par\noindent\centering \texttt{[| [| A1; A2 |] ==> B |] ==> ([| A2; A1 |] ==> B)}. \par\noindent} That is, \texttt{==>} can be seen as the analogue of the horizontal bar used to state rules in a natural deduction system, in which the order of premises is not significant. Likewise, since \texttt{A == B} means that \texttt{A} can be replaced by \texttt{B}, or vice versa, \texttt{==} is reflexive, symmetric and transitive. This meta-logic is known as Isabelle's \texttt{Pure} theory. Mostly the user would augment this by defining additional constants to capture the syntax of the object logic. For example, to capture set theory, we would add a constant \texttt{mem} (say) to stand for the $\in$ symbol, while sequents would require constants `\texttt{|-}' and `\texttt{,}'. % an object logic containing operators and inference rules; % these would usually include all the usual logical operators % and inference rules, % and often much more, such as operators and rules for set theory. Several such object logics are packaged with the Isabelle distribution \cite{isabelle-object}. Once these syntactic elements of the object logic are in place, we can build object-logic expressions into the $\alpha_i$ and $\beta$. For example, in \dRA, the $(\vdash \lor)$ rule uses the meta-logical operator \texttt{==>} discussed above, and could be entered as \texttt{"[| \$X |- P, Q |] ==> \$X |- P v Q"}. (The \texttt{\$} distinguishes \dRA-structures such as \texttt{X} from \dRA-formulae such as \texttt{P}.) This rule is an instance of the form ``from $\alpha \mbox{ infer } \beta$''. However \dRA\ was implemented in Isabelle directly on top of the \texttt{Pure} theory, so that the only inference rules available are those of \dRA. %(Thus you can't write $(P \vdash Q) \lor (R \vdash S)$, for example, %as you could if \dRA\ were built on top of Isabelle/HOL). As far as the Isabelle meta-logic is concerned, we can think of the atomic propositions as the formulae of the object-logic. In this case these are \dRA-sequents of the form $X \vdash Y$, built using object-logic ``connectives'' `$\vdash$', `,', `;', `*', `$\bullet$', `$\land$', `$\lor$', etc. These can be combined into more complex propositions using the Isabelle meta-logic connectives \texttt{==>}, \texttt{==} and \texttt{!!}. Thus each Isabelle proposition is either a \dRA\ sequent $X \vdash Y$, or is made up of sequents combined into inference rules using the three Isabelle/Pure logical operators. It follows that expressions such as \texttt{X |- (P ==> Q)} or \texttt{A v (B ==> C)} are not possible. Note that the $\alpha_i$ and $\beta$ as discussed above would most commonly simply be \dRA-sequents, but could be ``complex'' Isabelle propositions. We may declare axioms and inference rules of the \dRA\ calculus to Isabelle. For example, the sequent $p \vdash p$ is an initial sequent (axiom) in \dRA; thus it is declared in Isabelle as a ``rule'', \texttt{P |- P}. (For a rule with no premises, this notation is used rather than \texttt{[| |] ==> P |- P}.) Similarly, each rule of \dRA\ is declared as an Isabelle rule, as in the example of the $(\vdash \lor)$ rule above. These, and further derived sequents and rules, are called Isabelle ``theorems''. %Isabelle theorems may be object logic formulae or may %involve Isabelle's metalogical operators. Thus, in the Isabelle implementation of \dRA, an Isabelle theorem may be either a simple sequent of \dRA, or a sequent \emph{rule}. Whereas an initial sequent of \dRA\ becomes an Isabelle theorem of the form \texttt{X |- Y}, a sequent rule becomes an Isabelle theorem containing also the operators \texttt{==>} (implication) or \texttt{==} (equality). } In \cite{dawson-gore-dra-jelia98} we described an implementation of \dRA\ which used Isabelle's \texttt{Pure} theory, so that the only inference rules available were those of \dRA. Thus, in the Isabelle implementation of \dRA, an Isabelle theorem may be either a simple sequent of \dRA, or a sequent \emph{rule}. Whereas a sequent derivable in \dRA\ becomes an Isabelle theorem of the form \texttt{X |- Y}, a sequent rule becomes an Isabelle theorem containing also the meta-logical operators \texttt{==>} (implication) or \texttt{==} (equality). That this is a shallow embedding is reflected in the fact that the horizontal bar of sequent rules becomes the Isabelle \texttt{==>} operator. In a deep embedding, as in Section \ref{hol}, the horizontal bar also becomes an object-level constant. \comment{ % For example, the (cut) rule (shown on \page{id}) appears as % {\par\noindent\centering % \texttt{"[| \$?X |- ?A; ?A |- \$?Y |] ==> \$?X |- \$?Y"} % \par\noindent} For example, the ($\vdash \lor $) rule (shown in \S\ref{|-v}) appears as $$\texttt{"\$?X |- ?A, ?B ==> \$?X |- ?A v ?B"}$$ in Isabelle. (The `\verb:?:' denotes a variable which can be instantiated, and the `\verb:$:' denotes a structural variable or constant.) The variant $A \vdash A$ of the (id) rule (see \S\ref{otm}) appears as \texttt{"?A |- ?A"}. The bi-directional \texttt{dcp} rule, shown in \fig{sdr}, appears as \texttt{"\$?X |- \$?Y == * \$?Y |- * \$?X"}. } In this shallow embedding, access to and manipulation of the shape of \dRA\ constructs (ie, sequents, structures, formulae) and derivations was provided only at the ML level. For example, in \cite{dawson-gore-dra-jelia98} we described having programmed a procedure to perform cut-elimination for \dRA. The input to this was a \dRA\ 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 \dRA\ 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. \comment{ a derivation step is represented as a function; a complex derivation is the composition of functions representing the elementary derivation steps. Therefore, to look at the shape of a derivation (for example, to ask what rule was used in the final \dRA\ inference step) involved changing the Isabelle code somewhat, so as to record the elementary \dRA\ rules used and to construct a derivation-tree while a derivation was being performed. } What we aim to do (as described later) is to perform the cut-elimination {\em proof} entirely within a theorem prover, rather than writing a cut-elimination {\em 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. \comment{ In \cite{dawson-gore-dra-jelia98} we also described using the Isabelle \dRA\ implementation to show the soundness of certain other calculi for relation algebra. In these cases, we in fact showed that all the axioms and rules of the other calculi were derivable in \dRA. The argument that followed, namely that therefore an entire derivation in one of those other calculi could have been performed in \dRA, was outside the scope of the mechanical theorem prover. Again, doing this within the theorem prover requires modelling the shape of sequents or formulae of the calculus in question, of derivations, and of the rules used in them. Similar work has been done by Mikhajlova and von Wright for classical first-order logic proof systems in \cite{mikhajlova-vonwright-isomorphism}. But note that their work assumes that the second and third clauses of the definitions given at \cite[p.~302]{mikhajlova-vonwright-isomorphism} are sound, and we suspect one is not. We are currently trying to show whether their definitions are derivable using their previous definitions. } \section{Dependent Type Theory implementations} \subsection{Introduction} In a dependent type theory, a type may be parametrised over a type variable {\em and} a term variable. This, coupled with the \emph{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. \comment{ A simpler situation where the Curry-Howard isomorphism can be seen is in the simply-typed $\lambda$-calculus and a natural deduction calculus \textsf{NDInt} for intuitionistic propositional logic. Let $A$ and $B$ be formulae, and $\pi$ be a derivation of $A$ in \textsf{NDInt}. Suppose also that $A \to B$ is derivable in \textsf{NDInt}, and consider an \textsf{NDInt}-derivation of $A \to B$ %in the Natural Deduction style, where one assumes $A$ and derives $B$. That is, it is a derivation of $B$ in which $A$ is regarded as true; at the points where $A$ is used, it would contain some notation $\xi$ meaning ``true by assumption''. Let $\rho(\xi)$ be this derivation of $B$. %where $x$ is a place-holder for some %notation meaning ``true by assumption'', %as will appear in the derivation of $B$ wherever $A$ is used. So if we substitute $\pi$ (the derivation of $A$) for $\xi$ in $\rho(\xi)$, we get a derivation $\rho(\pi)$ of $B$ which does not rely on $A$ as an assumption. Then, using $\pi : A$ to mean ``$\pi$ is a derivation of $A$'', we can write the rule \begin{center} \slrule { \pi : A \qquad \rho(\xi) : A \to B } { \rho(\pi) : B } \end{center} Erasing the annotations $\pi$ $\rho$ and `:' gives the well-known $(\to E)$ natural deduction rule for intuitionistic logic; the rule as it stands also shows how to derive $B$. As indicated above, we can equally think of $\rho(.)$ as a derivation of $A \to B$ or as a function which takes, as argument, a derivation of $A$ such as $\pi$, and returns a derivation of $B$. If we also think of $A$ as the type ``derivations of proposition $A$'' (and similarly for $B$) we get the functional type-theory interpretation, under which $A \to B$ means the type of functions which take an argument of type $A$ and return a result of type $B$. (Conveniently, the same symbol `$\to$' is conventionally used for both purposes.) } The Curry-Howard isomorphism, in the simply-typed $\lambda$-calculus, identifies terms with proofs and types with propositions. So if $A$ is a type (proposition), and $\pi$ is a term, then $\pi : A$ means ``$\pi$ is a derivation of $A$''. Dependent types extend what can be done in the simply-typed $\lambda$-calculus in two distinct ways. Firstly, consider a type $I$ of individuals, and a parametrised type $A(i)$. That is, for each individual $i \in I$, there is a type $A(i)$. Consider a function $\rho$ whose domain is $I$, such that for each $i \in I$, $\rho(i) \in A(i)$. The type of such a function is written $\prod i : I . A(i)$ denoting how the type of $\rho(i)$ \emph{depends} on the \emph{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 $\rho(i)$ be a derivation of $A(i)$. That is, $\rho$ is a function which, for each individual $i$, gives a derivation of $A(i)$; we can think of such a $\rho$ as a derivation of $\forall i A(i)$. At the same time, if we think of each type $A(i)$ as the type ``derivations of proposition $A(i)$'', then the functions $\rho$ of type $\prod i : I . A(i)$ are the derivations of $\forall i A(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 $\lambda$-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 \dRA\ where instead of $P(t)$, we used $X \vdash 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 \to Z$, $U \to V \to W$ and $S \to S \to T$ we can construct functions of type $X \to Y \to Z$, $V \to U \to W$ and $S \to T$, we unavoidably have weakening, exchange and contraction. However, in our formulation of \dRA, these are at the meta-logic level, not in the object logic. Two theories based on dependent types are the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework} and Constructive Type Theory (CTT) \cite{martin-lof-CTT}. \subsection{The Twelf implementation} Twelf \cite{pfennig-schurmann-twelf} is an implementation of the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}. This is based on a typed $\lambda$-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. \begin{tabular}{c@{\quad}l} 1 & \texttt{str : type. } \\ 2 & \texttt{|- : str -> str -> type. \%infix none 10 |-.} \\ 3 & \texttt{* : str -> str. \%prefix 200 *.} \\ & \\ 4 & \texttt{\% Display postulates } \\ 5 & \texttt{sA : (* X |- Y) -> (* Y |- X).} \\ 6 & \texttt{sS : (X |- * Y) -> (Y |- * X).} \\ & \\ 7 & \texttt{\% Derived structural rules} \\ 8 & \texttt{ssASl = [D] sA (sS D). \% (X |- * * Y) -> (* * X |- Y)} \end{tabular} Line~1 declares \texttt{str} as a new type to represent the \dRA\ structures. Line~2 declares \texttt{|-} as a binary type constructor, taking two \emph{term} arguments of type \texttt{str} and returning a \emph{type}. Thus, for structures \texttt{X} and \texttt{Y}, the construct \texttt{X |- Y} represents derivations of the sequent $X \vdash Y$. Line~3 declares \texttt{*} as a unary structure operator. Lines 4 and 7 are comments. In lines 5 and 6 the terms \texttt{sA} and \texttt{sS} (which stand for ``star in the antecedent'' and ``star in the succedent'') are declared with the types %showing that they denote that represent derivations of the \dRA\ rules \begin{center} \slrule { *X \vdash Y } { *Y \vdash X } (\ttdef{sA}) \qquad \hspace{20mm} \slrule { X \vdash *Y } { Y \vdash *X } (\ttdef{sS}) \qquad \end{center} We can think of these declarations as assertions that there are derivations called \texttt{sA} and \texttt{sS}) of these rules, or as defining these as new ``primitive'' one-step rules. Now, by treating \texttt{sA} and \texttt{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 \vdash * * V$ as below: $$ \stackrel {\mbox{derivation of}}{U \vdash * * V} \quad \stackrel{\texttt{sS}} \longrightarrow \quad \stackrel {\mbox{derivation of}}{* V \vdash * U} \quad \stackrel{\texttt{sA}} \longrightarrow \quad \stackrel {\mbox{derivation of}}{* * U \vdash V} $$ The definition of \texttt{ssSAl} does this; the notation means $\lambda D. \textit{sA} (\textit{sS} \ D)$. Twelf computes the type of the function \texttt{ssSAl}, giving $(S1 \vdash * * S2) \to (* * S1 \vdash S2)$. Note that $X, Y, S1$ and $S2$ are variables. Twelf offers Prolog-like \cite{prolog-standard} queries such as \texttt{ \_ssASl : (X1 |- * * Y1) -> (* * X1 |- Y1).} \noindent which searches for a term of the specified type (ie, searches for a derivation of the stated rule) and instantiates \texttt{\_ssASl} with that term. In this example, because Twelf allows substituting for \texttt{X1} and \texttt{Y1} in the query as well as for the variables \texttt{X} and \texttt{Y} in the declarations of \texttt{sA} and \texttt{sS}, the search proceeds along an infinite branch in the wrong direction. On the other hand, the code \begin{verbatim} % Using the theorem prover %theorem ssASl\_th : exists {D:{S1:str} {S2:str} (S1 |- * * S2) -> (* * S1 |- S2)} true. %prove 2 {} (ssASl\_th D). \end{verbatim} \noindent successfully uses Twelf's theorem prover to find the derivation, returning \noindent \texttt{ /ssASl\_th/: ssASl\_th ([S1:str] [S2:str] [X1:S1 |- * * S2] sA (sS X1)).} \noindent (Here the variables \texttt{S1} and \texttt{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. \comment{ At this point we should refer to the proof of a cut-elimination theorem, using Twelf, described in \cite{pfennig-structural-cut-elimination}. This uses a rather ingenious representation of sequents; a cut-free proof of a traditional Gentzen sequent $A \vdash B$ is represented as the type \texttt{neg A -> pos B -> @}, and a cut-free proof of it as \texttt{neg A -> pos B -> \#}. The two rules shown below left are represented as the type shown on the right: \begin{center} \slrule {\Gamma, A \vdash \Delta} {\Gamma, A \& B \vdash \Delta} \quad \slrule { A \vdash } { A \& B \vdash } \quad \texttt{(neg A -> \#) -> (neg (A and B) -> \#)} \end{center} In fact, the second rule shown would be directly represented by the type shown, but the first rule shown would be directly represented by \begin{center} \texttt{(neg $\Gamma$ -> pos $\Delta$ -> neg A -> \#) -> \qquad \mbox{}\\ (neg $\Gamma$ -> pos $\Delta$ -> neg (A and B) -> \#)} \end{center} However the existence of a term (function) of the type shown first trivially implies the existence of a term (function) of the type shown second. Further constructed types represent stages of the transformation of a proof into a cut-free proof, and a termination checker checks that the function performing the entire transformation from a proof to a cut-free proof terminates. However, this termination checker only checks that the function would not run forever. It does not check that it terminates with a cut-free derivation -- it does not complain if the code is run with some cases deleted. This work on the cut-elimination theorem is based on an ingenious way of representing the problem in a way that fits into Twelf; even so, getting a proof of the cut-elimination theorem from it relies on the heuristically-based termination checker and upon a manual check that all possible cases for the rules used just above the ``cut'' have been covered. On the other hand, the Twelf type-checker proves that each individual step is correct, in that the changed derivation in fact does derive the sequent which it purports to derive. Thus this proof of cut-elimination lies between our previous work (where we just programmed a cut-elimination function in ML) and a fully formal proof. } \subsection{The Isabelle/CTT implementation} We then turned to the \texttt{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 \dRA\ similarly to its implementation in Twelf, so that we had, for example, (omitting premises of the from \texttt{?X : str}, which were fairly ubiquitous) \texttt{ "sA : * ?X |- ?Y --> * ?Y |- ?X" : thm \\ \indent "sA oo sS : ?X |- * * ?Y --> * * ?X |- ?Y" : thm } \noindent where \texttt{oo} denotes function composition. We wrote tactics to determine the type of a term variable \texttt{?t} by solving a goal such as \texttt{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 \texttt{?P}. \texttt{"?P : ( X |- * * Y) --> ( * * X |- Y)"}. The \texttt{CTT} theory of Isabelle is not extensively developed so we found it necessary to prove some fairly elementary though general theorems. %\subsection{Dependent type theory -- conclusions} \subsection{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, \emph{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. %We have referred to a proof in Twelf of the sequent calculus %cut-elimination theorem, noting that it was based on %an ingenious way of representing the problem in a way that fits into %Twelf, and that it was not a fully formal proof. %Since we are aiming for a fully formal proof, using techniques which %would be applicable equally to other proof-theoretic results, %we felt that this cut-elimination proof does not indicate that %dependent type theory would be powerful enough for our needs. \section{The Isabelle/HOL implementation} \label{hol} \texttt{HOL} is an Isabelle theory based on the higher-order logic of Church \cite{church-types} and the HOL system of Gordon \cite{HOL-introduction}. Thus it includes quantification and abstraction over higher-order functions and predicates. The \texttt{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 \texttt{datatype} and \texttt{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 \dRA\ in Isabelle/HOL is still underway. However it is clear at this stage that the facility for \texttt{datatype} type declarations and associated primitive recursive function definitions is of enormous help. For example, we model \dRA\ structure expressions (see \cite{gore-relalg}) as below: \begin{verbatim} datatype structr = Comma structr structr | SemiC structr structr | Star structr | Blob structr | I | E | Structform formula | SV string \end{verbatim} The first six lines correspond to the structure operators of \dRA\ and the next line is for ``casting'' a \dRA\ formula into a \dRA\ structure. The last line had no analogue in the shallow embedding, where an Isabelle variable such as \texttt{?S} referred to any \dRA-structure. In the deep embedding, \texttt{SV ``X''} will refer to the variable named \texttt{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 \ref{pure}, 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) \texttt{(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 \begin{verbatim} datatype pftree = Pr rule (pftree list) | Unf sequent \end{verbatim} where \texttt{Pr r pts} is a derivation whose last step uses a \dRA\ rule whose instantiation is \texttt{r}, and the premises of that last step are the conclusions of the derivations in the list \texttt{pts}. \texttt{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, \begin{verbatim} primrec "premsPT (Unf seq) = [seq]" "premsPT (Pr rule pts) = premsPTs pts" "premsPTs [] = []" "premsPTs (pt # pts) = premsPT pt @ premsPTs pts" \end{verbatim} 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 \texttt{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 \dRA\ rule {\em instance} of a \dRA\ 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. \section{Conclusion} We have reviewed earlier work in which a shallow embedding of the \dRA\ 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 \dRA, 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. % \vspace{2ex} % \textbf{Acknowledgement}. % The second author is supported by the Australian Research Council % via a Queen Elizabeth II Fellowship. \comment{ } %endcomment %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Here begins the end matter %\bibliography{./awcl,/home/arp/disk1/rpg/bib/fm,/home/arp/disk1/rpg/bib/modal,/home/arp/disk1/rpg/bib/mtl,/home/arp/disk1/rpg/bib/logic,/home/arp/disk1/rpg/bib/tl,/home/arp/disk1/rpg/bib/paracon,/home/arp/disk1/rpg/bib/linear,/home/arp/disk1/rpg/bib/algebra,/home/arp/disk1/rpg/bib/relevant,/home/arp/disk1/rpg/bib/dl} %\bibliographystyle{plain} \begin{thebibliography}{10} \bibitem{belnap-display} N~D {Belnap}. \newblock Display logic. \newblock {\em Journal of Philosophical Logic}, 11:375--417, 1982. \bibitem{boulton-et-al-hdl} Boulton, Gordon, Gordon, Harrison, Herbert, and van Tassel. \newblock Experience with embedding hardware description languages in hol. \newblock In {\em 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. \bibitem{church-types} Alonzo Church. \newblock A formulation of the simple theory of types. \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. \bibitem{dawson-gore-dra-jelia98} J~Dawson and R~Gor{\'{e}}. \newblock A mechanised proof system for relation algebra using display logic. \newblock In {\em JELIA98:}, LNAI 1489:264--278. Springer, 1998. \bibitem{prolog-standard} P~Deransart, A~Ed-Dbali, and L~Cervoni. \newblock {\em Prolog: The Standard}. \newblock Springer-Verlag, 1996. \bibitem{elmasri-navathe-database} Ramez~A Elmasri and Shamkant~B Navathe. \newblock {\em Fundamentals of Database Systems}. \newblock Benjamin/Cummings, Redwood City, 2 edition, 1994. \bibitem{gallier-logic} J.~H. Gallier. \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem Proving}. \newblock John Wiley and Sons, 1987. \bibitem{HOL-introduction} M~J~C Gordon and T~F Melham. \newblock {\em Introduction to HOL: a Theorem Proving Environment for Higher Order Logic}. \newblock Cambridge University Press, 1993. \bibitem{gore-relalg} R~Gor{\'{e}}. \newblock Cut-free display calculi for relation algebras. \newblock In CSL96: LNCS 1258:198--210. Springer, 1997. \bibitem{gore-sld-igpl} R~Gor{\'{e}}. \newblock Substructural logics on display. \newblock {\em Logic Journal of the Interest Group in Pure and Applied Logic}, 6(3):451--504, 1998. \bibitem{harper-honsell-plotkin-framework} Robert Harper, Furio Honsell, and Gordon Plotkin. \newblock A framework for defining logics. \newblock {\em Journal of the ACM}, 40:143--184, 1993. \bibitem{maddux-introductory} R~D Maddux. \newblock Introductory course on relation algebras, finite-dimensional cylindric algebras, and their interconnections. \newblock In H.~Andreka, J.~D. Monk, and I.~Nemeti, editors, {\em Algebraic Logic}, volume~54 of {\em Colloquia Mathematica Societatis Janos Bolyai}, pages 361--392. North-Holland, Amsterdam, 1991. \bibitem{martin-lof-CTT} Per Martin-L\"{o}f. \newblock {\em Intuitionistic Type Theory}. \newblock Bibliopolis, 1984. \bibitem{mikhajlova-vonwright-isomorphism} Anna Mikhajlova and Joakim von Wright. \newblock Proving isomorphism of first-order proof systems in hol. \newblock In TPHOLS98, LNCS 1479:295--314. Springer, 1998. \bibitem{ML-definition} Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. \newblock {\em The Definition of Standard ML (Revised)}. \newblock The MIT Press, 1997. \bibitem{isabelle-ref} Lawrence~C Paulson. \newblock {\em The Isabelle Reference Manual}. \newblock Computer Laboratory, University of Cambridge, 1995. \bibitem{isabelle-object} Lawrence~C Paulson. \newblock {\em Isabelle's Object-Logics}. \newblock Computer Laboratory, University of Cambridge, 1995. \bibitem{pfennig-structural-cut-elimination} Frank Pfennig. \newblock Structural cut elimination. \newblock In Proc.\ LICS95, pages 156--166. IEEE Computer Society Press, 1995. \bibitem{pfennig-schurmann-twelf} Frank Pfennig and Carsten Sch\"{u}rmann. \newblock System description: Twelf - a meta-logical framework for deductive systems. \newblock In CADE-16, LNAI 1632:202--206. Springer, 1999. \bibitem{wansing-displaying-modal-logic} Heinrich Wansing. \newblock {\em Displaying Modal Logic}, volume~3 of {\em TRENDS IN LOGIC}. \newblock Kluwer Academic Publishers, Dordrecht, August 1998. \end{thebibliography} \end{document}