\section{Formulae, sequents and derivations} %{Reasoning About Derivations and Derivability}
\label{s-deriv}

We explain briefly the data structures we use to encode formulae, structures, 
sequents and derivations. 

%% Proof-theorists typically work with sequents  $\Gamma
%% \vdash \Delta$ where $\Gamma$ and $\Delta$ are ``collections'' of
%% formulae. The ``collections'' found in the literature increase in
%% complexity from simple sets for classical logic, to multisets for
%% linear logic, to ordered lists for substructural logics, to complex
%% tree structures for display logics.
%% A sequent rule typically has a rule name, a (finite) number of premises,
%% a side-condition and a conclusion.
%% Rules are read top-down as ``if all the premises hold then the
%% conclusion holds''.  A derivation of the judgement $\Gamma \vdash
%% \Delta$ is typically a finite tree of judgements with root $\Gamma
%% \vdash \Delta$ where parents are obtained from children by ``applying
%% a rule''. We use ``derivation''  to refer to a
%% proof \emph{within} a calculus, reserving ``proof'' for a
%% meta-theoretic proof of a theorem \emph{about} the calculus.  

%\subsection{Formulae and Subformulae}\label{subsec:formulae}

%We define a language of formulae. 
The language of formula for BiILL is defined using the grammar below:
$$
  A ::= p \mid I \mid \bot \mid A\otimes A \mid A\parr A \mid A\limp A \mid A\excl A
$$
where $p$ denotes a propositional variable. A FILL formula is just a BiLL formula
without any occurrences of $\excl.$

BiLL formulae are defined formally in Isabelle as follows. We let the type variable
\texttt{'s} be (Isabelle) strings. 
\begin{verbatim}
datatype 's pformula =
    Btimes pformula pformula ("_ &&& _" [68,68] 67)
  | Bplus pformula  pformula ("_ +++ _" [66,66] 65)
  | Blolli pformula pformula ("_ --o _" [64,64] 63)
  | Bexcl pformula pformula ("_ --< _" [64,64] 63)
  | Btrue ("T") | Bfalse("F") | FV string | PP string
\end{verbatim}
Here the binary constructors correspond to, respectively, 
$\ltens$, $\parr$, $\limp$ and $\excl$. The unary constructors 
\texttt{Btrue} and \texttt{Bfalse} encode the units $\tunit$ and $\punit$, 
respectively. The constructor \texttt{PP} is used to encode propositional
variables, whereas \texttt{FV} is used to encode ``scheme variables''; we shall
come back to this shortly. 


%
We define the immediate (proper) subformula
relation, \texttt{ipsubfml}, which will not need to be changed when new
connectives are added.
\begin{verbatim}
ipsubfml     :: "('a pformula * 'a pformula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
  intrs ips_and1 "(P, P &&& Q) : ipsubfml" (etc)
\end{verbatim}

%\subsection{Structures, Sequents and Rules}\label{subsec:structures}

%% Sequents in display calculus are more general than the traditional notion
%% of sequents in Gentzen's system, where the only structural connective allowed
%% is the `comma'. 

A sequent is made up of {\em antecedent}
and {\em succedent} structures, defined, respectively, as follows: 
$$
  X_a ::= A \mid \Phi \mid X_a,X_a \mid X_a<X_s
\qquad
\qquad
\qquad
  X_s ::= A \mid \Phi \mid X_s,X_s \mid X_a>X_s
$$
where $\Phi$ is a structural constant. The symbols $<$ and $>$ are
the structural counterparts of the connectives $\excl$ and $\limp$, respectively.

Structures are 
%of our calculus $\biilldc$ are 
represented by the datatype below:
\begin{verbatim}
datatype 's pstructr = Comma ('s pstructr) ('s pstructr)
  | Gt ('s pstructr) ('s pstructr) | Lt ('s pstructr) ('s pstructr)
  | I | Structform ('s pformula) | SV 's
\end{verbatim}
where \texttt{Comma}, \texttt{Gt}, \texttt{Lt} and \texttt{I} correspond
to the structural connectives `,', $>$, $<$ and $\Phi$.
The operator \texttt{Structform} ``casts '' a formula into
a structure. %, since a formula is a special case of a structure.
% (as in the premises of the cut rule given above). 
The constructor \texttt{SV}
represents scheme variables for structures.
%% structure variables which appear in the statement of a rule
%% or theorem, and which are instantiated to actual structures of the calculus 
%% when constructing derivations. 
Since we must reason about arbitrary
derivations, we have to allow derivations to contain structure
variables and reason about their instantiations.
%% We therefore cannot use Isabelle's built-in unification facility for
%% instantiating its scheme variables as explained in more detail in
%% \cite{Dawson01}. 
We do not encode explicitly the notion of antecedent/succeedent
structures in the data type; these notions are enforced via
separate predicates when needed (see e.g.,
Section~\ref{sec:eqdlshallow}).

%% Likewise, formulae of the calculus 
%% are represented by a datatype which include a constructor \texttt{FV}
%% for formula variables which can be instantiated to actual formulae of
%% the calculus, and a constructor \texttt{PP} for a primitive proposition
%% variable $p$.

%% The notation in parentheses in the definition of datatype
%% \texttt{pformula}
%% %Figure~\ref{fig:isabelle-formulae}
%% describe an alternative infix syntax, closer to the actual
%% syntax of the calculus.  Some complex manipulation of the syntax, available
%% through Isabelle's ``parse translations'' and ``print translations'',
%% allows structure variables and constants to be prefixed by the symbol
%% \texttt{\$}, and the notations \texttt{FV}, \texttt{SV} and
%% \texttt{Structform} to be omitted.  For technical reasons related to
%% this, a different method is used to specify the alternative infix
%% syntax for structures and sequents: details omitted.

Sequents and rules of the calculus are represented by 
%the Isabelle/HOL datatypes:
\begin{verbatim}
datatype 'a sequent = Sequent 'a 'a
types 'a psc = "'a list * 'a" (* single step inference *) 
types 'a rule = 'a sequent psc
\end{verbatim}
The premises of a rule are represented using a list of sequents while
the conclusion is a single sequent. Thus \texttt{(prems, concl)}
means a rule with premises \texttt{prems} and conclusion \texttt{concl}. 
A sequent \texttt{(Sequent X Y)} can also be represented as
\texttt{\$X |- \$Y}. 
%% Thus \texttt{(\$"X" |- "A")} is equivalent
%% to the term \texttt{Sequent (SV "X") (Structform (FV "A"))}.
%% % is printed, and may be entered, as

% This doesn't seem to be used anywhere.
%% Functions \texttt{premsRule} and
%% \texttt{conclRule} return the premise list and the conclusion of a
%% rule respectively. 
%% A structure expression is \emph{formula-free} if it
%% does not contain any formula as a sub-structure: that is, if it does
%% not contain any occurrence of the operator \texttt{Structform}.  A
%% formula-free sequent is defined similarly. 

% The constant \texttt{rls}
% represents the set of rules of \dRA, encoded using the datatypes just
% described: we omit the details of this code.

% Our definition of nested sequents is very similar, except that we do not have
% separate datatypes corresponding to sequents and structures.  
% Rather we have a single datatype 
% \begin{verbatim}
% datatype 's pnested = NComma ('s pnested) ('s pnested)
% 		    | Nseq ('s pnested) ('s pnested)
% 		    | NI
% 		    | NStructform ('s pformula)
% 		    | NSV 's
% \end{verbatim}
% The pretty-printing/parsing (\texttt{\$} for a nested sequent, its absence for
% a formula, omission of ``\texttt{NStructform}'' and ``\texttt{NSV}'') is
% similar to that for display logic.

%% Note that our formalisation defines variant sets of rules 
%% both including and excluding the cut rule shown below.
%% \[
%%   \AxiomC{$\Gamma \vdash A, \Delta$}
%%   \AxiomC{$\Gamma, A \vdash \Delta$}
%%   \LeftLabel{(cut)}
%%   \BinaryInfC{$\Gamma \vdash \Delta$}
%%   \DisplayProof
%% \]
%% Thus our cut-admissibility result will be of the form:
%% if $\Gamma \vdash A, \Delta$ is (cut-free) derivable
%% and $\Gamma, A \vdash \Delta$ is (cut-free) derivable
%% then $\Gamma \vdash \Delta$ is (cut-free) derivable.

%% In previous work~\cite{dawson-gore-embedding-comparing}, we describe
%% our initial attempts to formalise display calculi in various logical
%% frameworks and describe why we selected Isabelle/HOL.  When we model a
%% derivation tree, explicitly, we do so using the capability in HOL of
%% defining types like the datatypes of SML, see \S\ref{s-dse}.  
%% %Here we return to simpler sequents and seek generality.

%% In~\cite{dawson-gore-cut-admissibility}, we modelled a derivation tree
%% in HOL as a recursive structure which consists of a
%% root sequent (which should be the conclusion of some rule), and an
%% associated list of (sub)trees (each of which should derive a premise of
%% that rule). The type of explicit derivation trees is a recursive
%% datatype, such as:
%% \begin{verbatim}
%%    datatype 'a dertree = Der 'a ('a dertree list)
%%        | Unf 'a (* unfinished leaf which remains unproved *)
%% \end{verbatim}
%% %
%% We then had to define a predicate on such a tree, saying whether it
%% was in fact correctly based on the given rules, and so represented a
%% valid derivation.
%% %
%% We modelled a sequent rule as an object in HOL consisting of a list of
%% premises and a conclusion, each of which was a sequent in the language
%% of the logic. Notably, our language of formulae
%% included ``variables'' which could be instantiated with formulae, 
%% so we defined functions for such substitutions.
%% %
%% Thus it is more accurate to say in
%% ~\cite{dawson-gore-cut-admissibility}, we used a deep embedding for
%% \emph{derivations}, \emph{rules} and \emph{variables}, since we
%% modelled each of these features of the proof-theory explicitly rather
%% than identifying them with the same features of Isabelle.

%% In alternative approaches to work of this type, the set of derivable
%% sequents can be modelled as an inductively defined set \texttt{ders}
%% (say),
%% % (as we describe in \S\ref{s-dp}). 
%% where the derivation tree does not exist, but it ``happens'' in the
%% course of proving that a specific sequent is derivable.  That is,
%% derivability in the sequent calculus studied equates to derivability
%% in Isabelle, giving a shallow embedding of {\em derivations}.

%% In such alternative approaches, the rules of the sequent calculus can
%% either be encoded explicitly 
%% %(as assumed in the treatment in \S\ref{s-dp}), 
%% or they can be encoded in the clauses for the inductive definition of
%% \texttt{ders}.  In the latter case, the rules of the
%% sequent calculus under study are encoded as theorems of Isabelle.
%% Thus, even with a shallow embedding of derivations, we have a choice
%% of either a deep or a shallow embedding of {\em rules}:
%% %where \textit{ders} means the set of derivable sequents:
%% % \begin{gather}
%% %  (\{P,  Q\},  {P \land Q}) \in \mathit{rules} \tag{deep}
%% % \qquad
%% % \frac{ (ps, c) \in \mathit{rules} \quad ps \subseteq \mathtt{ders}}
%% % {  c \in \mathtt{ders}}
%% % \\[1ex]
%% % \frac {P \in \mathtt{ders} \qquad Q \in \mathtt{ders}}
%% % {P \land Q \in \mathtt{ders}} \tag{shallow}
%% % \end{gather}
%% %
%% \begin{description}
%% \item[\rm Deep Rules and Shallow Derivation:] \ \\[0.5em]
%%   \begin{tabular}[c]{l}
%%    $\mathtt{(\{\Gamma \vdash P, ~~\Gamma \vdash Q\},  
%%      \;\; \Gamma \vdash P \land Q) \in rules}$
%%   \\[0.5em]
%%    $\mathtt{ [|~(ps, c) \in rules ~;~ ps \subseteq \mathtt{ders}~|]
%%          ==> c \in \mathtt{ders}}$
%%   \\[0.5em]
%%   \end{tabular}
%% \item[\rm Shallow Rules and Shallow Derivations:] \ \\[0.5em]
%%   \begin{tabular}[c]{l}
%%    $\mathtt{[|~\Gamma \vdash P \in \mathtt{ders} ~;~ 
%%           \Gamma \vdash Q \in \mathtt{ders}~|]
%%         ==> \Gamma \vdash P \land Q \in \mathtt{ders}}$.
%%   \end{tabular}
%% \end{description}

%% Finally, compared to \cite{dawson-gore-cut-admissibility}, it is much
%% more common to let the variables in a rule be the variables of the
%% theorem prover, and for the theorem prover to do the substitution. In
%% general, however, a deep embedding of one feature can be combined with
%% a shallow embedding of another.

%% Our experience is that shallow embeddings generally permit easier
%% proofs, but sometimes they are inadequate to express a desired
%% concept. For example, with a deep embedding of rules it is easy to
%% express that one set of rules is a subset of another set.  With a deep
%% embedding of derivation trees it is easy to express that one property
%% of derivation trees is the conjunction of two other properties, or
%% that a derivation tree has a particular height, whereas to express
%% such things using \derl, \derrec, etc (see \S\ref{s-dp}), one would
%% have to redefine these predicates incorporating the particular
%% properties of interest.  Indeed, in this work \cite{our-GLR-paper} we
%% discuss how we found a shallow embedding of derivability inadequate.

%% We have developed the code on which
%% \cite{dawson-gore-cut-admissibility} was based to reflect the fact
%% that Belnap's original proof applied generally to display calculi
%% satisfying certain conditions.  Some of these conditions required a
%% deep embedding of variables (and, therefore, of the rules), for
%% example, that no structure variable appears twice in the conclusion of
%% the statement of a rule.  For others, a shallow embedding of variables
%% was adequate, since the condition applied equally to the statement of
%% the rule and to all its substitution instances, for example that a
%% premise of a rule contains no variable not contained in the
%% conclusion.

%% \subsection{Our General Derivability Predicates} \label{s-dp} 

We now briefly describe the functions we used to encode
derivability.  A fuller account is given in \cite{DBLP:conf/lpar/DawsonG10}.
This framework is general in that a rule merely consists of ``premises''
and a ``conclusion'', and is independent of whether the things derived
are formulae or sequents, but we will refer to them
as formulae.

\begin{verbatim}
types 'a psc = "'a list * 'a"       (* single step inference *)
consts
  derl, adm :: "'a psc set => 'a psc set"
  dersl     :: "'a psc set => ('a list * 'a list) set"
  dercsl    :: "'a psc set => ('a list list * 'a list) set"
  derrec    :: "'a psc set => 'a set => 'a set"
  dersrec   :: "'a psc set => 'a set => 'a list set"
\end{verbatim}

An inference rule \texttt{'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then, \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls}, and \texttt{derrec rls
  prems} is the set of formulae derivable using rules \texttt{rls}
from the set \texttt{prems} of premises.  These were defined as
inductive sets, using also the functions \texttt{dersl} and
\texttt{dersrec}. So $\mathtt{(ps, c) \in \derl\ \rls}$ reflects the
shape of a derivation tree: \texttt{ps} is a list of exactly the
premises used, in the correct order, whereas $\mathtt{c \in \derrec\
  \rls\ prems}$ holds even if the set of premises \texttt{prems}
contains extra formulae.

The auxiliary function \texttt{dersrec} represents several formulae,
all derivable from the premises.  The auxiliary function
\texttt{dersl} represents several derivation trees side by side;
$\mathtt{(ps, cs) \in dersl~rls}$ when \texttt{ps} is the
concatenation of their lists of premises, and \texttt{cs} is the list
of their conclusions.  The function \texttt{dercsl} is similar, but it
shows which premises are part of which tree.  That is, $\mathtt{(pss, cs) \in
\texttt{dercsl}\ rls}$ implies $\mathtt{(concat\ pss, cs) \in \texttt{dersl}\
rls}$.  
Some proofs about \derl\ are easier using 
\texttt{dercsl} rather than \texttt{dersl} as the auxiliary function.

%% The key clauses for these functions are shown below:
%% \begin{verbatim}
%%   dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |] 
%%               ==> (pss, concl) : derl pscrel"
%%   derI : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |] 
%%               ==>  concl : derrec pscrel prems"
%% \end{verbatim}

%% We obtained the expected results linking \texttt{derl} and \texttt{derrec},
%% and a number of results expressing transitivity of derivation and the
%% results of derivation using derived rules, for example:
%% \begin{verbatim}
%% derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
%%                  ==> (?x, ?c) : derl ?rls" 
%% derl_deriv_eq : "derl (derl ?rls) = derl ?rls" 
%% derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"
%% \end{verbatim}

Finally, $(ps, c)$ is an admissible rule iff: if all premises in $ps$
are derivable, then $c$ is derivable:\\
$(ps, c) \in \adm\ \rls \iff 
(set\ ps \subseteq \derrec\ \rls \ \ \Rightarrow \ \ c \in \derrec\
\rls)
$.

%% We obtained the following four results, which were surprisingly tricky
%% since \adm\ is not monotonic:
%% \begin{verbatim}
%% "derl ?rls <= adm ?rls"              "adm (adm ?rls) = adm ?rls"
%% "adm (derl ?rls) = adm ?rls"         "derl (adm ?rls) = adm ?rls"
%% \end{verbatim}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 





