\begin{figure}[t]
{\small
Cut and identity:
$
\qquad
\vcenter{
\infer[id]
{p \seq p}{}
}
\qquad
\vcenter{
\infer[cut]
{\Sc,\Vc \seq \Uc, \Tc}
{\Sc \seq \Uc, A & A, \Vc \seq \Tc}
}
$
Structural rules:
$$
\begin{array}{ccc}
\mbox{$
\infer[\drp_1]
{(\Sc \seq \Tc) \seq \Tc'}
{\Sc \seq \Tc, \Tc'}
$}
&
\mbox{$
\infer[\rp_1]
{\Sc \seq (\Tc \seq \Tc')}
{
\Sc, \Tc \seq \Tc'
}
$}
&
\mbox{$\infer[gl]
{(\Sc, \Tc \seq \Sc') \seq \Tc'}
{(\Sc \seq \Sc'), \Tc \seq \Tc'}
$} \\ \\
\mbox{$
\infer[drp_2]
{\Sc \seq \Tc, \Tc'}
{(\Sc \seq \Tc) \seq \Tc'}
$}
&
\mbox{$
\infer[rp_2]
{\Sc, \Tc \seq \Tc'}
{\Sc \seq (\Tc \seq \Tc')}
$}
&
\mbox{$
\infer[gr]
{\Sc \seq (\Sc' \seq \Tc', \Tc)}
{
\Sc \seq (\Sc' \seq \Tc'), \Tc
}
$}
\end{array}
$$
Logical rules:
$
\raisebox{-1em}{
\infer[\punit_l]
{\punit \seq \sunit}
{}
\qquad
\infer[\punit_r]
{\Sc \seq \Tc, \punit}
{\Sc \seq \Tc}
\qquad
\infer[\tunit_l]
{\Sc, \tunit \seq \Tc}
{\Sc \seq \Tc}
\qquad
\infer[\tunit_r]
{\sunit \seq \tunit}{}
}
$
$$
\infer[\ltens_l]
{\Sc, A \ltens B \seq \Tc}
{\Sc, A, B \seq \Tc}
\qquad
\infer[\ltens_r]
{\Sc, \Sc' \seq A \ltens B, \Tc, \Tc'}
{\Sc \seq A, \Tc & \Sc' \seq B, \Tc'}
$$
$$
\infer[\parr_l]
{\Sc, \Sc', A \parr B \seq \Tc, \Tc'}
{\Sc, A \seq \Tc & \Sc', B \seq \Tc'}
\qquad
\infer[\parr_r]
{\Sc \seq A \parr B, \Tc}
{\Sc \seq A, B, \Tc}
$$
$$
\infer[\limp_l]
{\Sc, \Sc', A \limp B \seq \Tc, \Tc'}
{
\Sc \seq A, \Tc
&
\Sc', B \seq \Tc'
}
\qquad
\infer[\limp_r]
{\Sc \seq \Tc, A \limp B}
{\Sc \seq \Tc, (A \seq B)}
$$
$$
\infer[\excl_l]
{\Sc, A \excl B \seq \Tc}
{
\Sc, (A \seq B) \seq \Tc
}
\qquad
\infer[\excl_r]
{\Sc, \Sc' \seq A \excl B, \Tc, \Tc'}
{
\Sc \seq A, \Tc &
\Sc', B \seq \Tc'
}
$$
}
\caption{The shallow inference system $\biillsn$.}
\label{fig:fbills}
\end{figure}
\section{Shallow Nested Sequent Calculi}
\label{sec:eqdlshallow}
In \cite{Clouston13CSL} nested sequents are defined as below,
where $A_i$ and $B_j$ are formulae:
$$
S~~T ::= S_1,\dots,S_k,A_1,\dots,A_m \seq B_1,\dots, B_n, T_1, \dots,T_l
$$
We use $\Gamma$ and $\Delta$ for multisets of formulae and use
$P$, $Q$, $S$, $T$, $X$, $Y$, etc., for nested
sequents, and $\Sc$, $\Xc$, etc., for
multisets of nested sequents and formulae. The empty multiset is
$\sunit$ (`dot'). A nested sequent is essentially a display structure,
but with the associativity and commutativity of the comma structural
connective implicit in the use of multisets. The sequent arrow $\seq$
overloads both $>$ and $<$, depending on whether it occurs in an antecedent
or a succeedent position in the sequent. This overloading simplifies
the presentation of the nested sequent rules~\cite{Clouston13CSL}.
%% is intentional,
%% as it allows us to simplify the presentation of the
%% nested sequent rules.
The shallow inference system $\biillsn$ for $\biill$ is given
in Fig.~\ref{fig:fbills}.
The most faithful encoding of a nested sequent would be one that
uses multisets as a datatype, which is supported by recent versions
of Isabelle~\cite{DBLP:conf/lics/TraytelPB12}.
%% Thanks to recent developments, the recent versions of Isabelle have
%% some capabilities to use a multiset as a
%% datatype~\cite{DBLP:conf/lics/TraytelPB12}.
However due to incompatibilities between versions of Isabelle we have been
constrained to use an older version of Isabelle to allow us to reuse
proofs for display calculi developed in that version~\cite{DBLP:conf/tphol/DawsonG02}.
Our definition of nested sequents is thus as below:
{\small
\begin{verbatim}
datatype nested = NComma nested nested | Nseq nested nested
| NPhi | NStructform formula | NSV string
\end{verbatim}
}
In our definition, \verb!NSeq! is the nested sequent turnstile
$\seq$, \verb!NComma! is the comma of nested sequent
calculi and \verb!NPhi! is its unit.
%% As for display calculi, we allow pretty-printing and parsing of
%% variables which stand for nested sequents by encoding them as
%% \verb!$"S"! while variables which stand for formulae are encoded as
%% \verb!"A"!.
As for display calculi, we allow \verb!=>! instead of \verb!Nseq! and
\verb!,,,! instead of \verb!NComma!.
%% The previous distinction between display structure and formulae
%% variables now becomes the distinction between nested sequent variables
%% like \verb!$"S"! and formula variables \verb!"A"!. We now need a
%% new turnstile \verb!=>! which can be treated much the same as a nested
%% sequent connective since it can be nested. We also need a nested
%% sequent ``comma'' for which we use \verb!,,,!.
%% For example, the cut
%% rule from Figure~\ref{fig:fbills} is encoded as:
%% \begin{verbatim}
%% sn_cut "sn_cutr == (
%% [($''S'' => $''U'',,, ''A''), (''A'',,, $''V'' => $''T'')],
%% ($''S'',,, $''V'' => $''U'',,, $''T''))"
%% \end{verbatim}
In our Isabelle formalisation, $\biillsn$ rules are prefixed
by \texttt{sn}, e.g., the $rp$ rule is named \texttt{sn\_rp}.
%% For the nested sequent calculus we have rules named (for example)
%% \texttt{sn\_rp},
%% \texttt{sn\_drp},
%% \texttt{sn\_pA} (permutation of the antecedent),
%% \texttt{sn\_aS} (associativity of the succedent),
%% \texttt{sn\_anda} and \texttt{sn\_ands}.
%These rules correspond to equivalent rules for the display calculus.
%
The entire set of rules is called \texttt{biillsn} and its cut-free
subset is \texttt{biillsn\_cf} (see file \texttt{N\_Rls.thy}).
As with the display calculus, we define a function \texttt{nrulefs}
to generate the (infinite) set of all substitution instances of a given rule.
%% we are interested in the (infinite) set of
%% substitution instances of these rules, that is,
%% \texttt{nrulefs biillsn} and \texttt{nrulefs biillsn\_cf}.
%% \subsection{The nested sequent datatype cannot involve multisets}
%% \label{s-msde}
%% The most faithful encoding of a nested sequent would be as below:
%% \begin{verbatim}
%% datatype nseq = NSeqTs "(nseq multiset) * (formula multiset)"
%% "(formula multiset) * (nseq multiset)"
%% ("_ => _" [61,61] 60)
%% | NSV string
%% \end{verbatim}
%% Here, the nested sequent turnstile $\seq$ is explicitly represented by
%% the datatype constructor \verb!NSeqTs!, taking two multisets on each
%% side corresponding respectively to the multiset of nested sequents and
%% multiset of formulae that appear on both sides. The second part is to
%% allow us to represent explicitly variables standing for nested
%% sequents, and substitutions on such variables.
%% Isabelle permits nested datatypes. For example, our derivation tree
%% \verb!dertree! is made up of an end-sequent and a list of
%% \verb!dertree!s whose end-sequents are the premises of the final rule
%% of the whole \verb!dertree!. Thus the datatype is nested because the
%% derivation tree contains a list of derivation trees. But this is
%% possible only because ``list'' is also a datatype. Since the multiset
%% type is not an Isabelle datatype, we cannot define dertree with
%% ``list'' replaced by ``multiset''. Similarly, we cannot just use the
%% definition of \verb!nseq! above.
% We first tried to define a nested sequent $\Sc \seq \Tc$ using a
% recursive structure where a nested sequent consists of two multisets
% of nested sequents joined by the \verb!=>! where the ``,'' is used to
% form multisets. However, in the paper a nested sequent is constructed
% using the operator ``$\Rightarrow$'', with a multiset of nested
% sequents on either side of the ``$\Rightarrow$''.
%% Note that our encoding \verb!nested! does not capture
%% the notion of nested sequent exactly since it allows
%% structures which may not contain a top-level \texttt{=>}.
%% %% For example, each of the following are allowed by \verb!nested! but
%% %% are not nested sequents as such:
%% %% a single formula $A$ encoded as
%% %% \verb!''A''!;
%% %% two comma-separated multisets of nested sequents
%% %% $\Sc, \Tc$ encoded as
%% %% \verb!$''S'' ,,, $''T''!.
%% Since our rules always have a \texttt{=>} as the top-level operator, all
%% uses of \verb!nested! in our formalisation do capture nested sequents
%% as defined.
%% Note also that associativity and commutativity of \verb!NComma! and the fact
%% that \verb!NPhi! is its unit is not enforced in the datatype. Rather, we
%% need to define additional structural rules to account for these. These
%% rules are straightforward and are omitted here.
%% The \verb!NComma! is not associative or commutative in the above
%% definition, and it does not have an identity. Our datatype therefore
%% creates an identity constructor \verb!NPhi! for \verb!NComma! and
%% requires the extra structural rules, such as one shown below, to enforce
%% associativity, commutativity and the fact that \verb!NPhi! is the
%% identity for \verb!NComma!.
%% That is, we had to extend the nested sequent calculus by extra
%% explicit structural rules to handle the commutativity, associativity
%% for its comma \verb!,,,! and add an extra structural connective $\Phi$
%% to represent its identity, as shown below for commutativity for
%% antecedents:
%% \\[15px]
%% \begin{minipage}[c]{0.4\linewidth}
%% \AxiomC{$S, T \seq U$}
%% \RightLabel{Ca}
%% \UnaryInfC{$T, S \seq U$}
%% \DisplayProof
%% \end{minipage}
%% \begin{minipage}[c]{0.4\linewidth}
%% \begin{verbatim}
%% sn_pA == (
%% [($''S'',,, $''T'' => $''U'')],
%% ($''T'',,, $''S'' => $''U'')")
%% \end{verbatim}
%% \end{minipage}
%% \\[15px]
%% The encoded shallow nested sequent calculus is \textit{not} merely a
%% notational variant of our display calculus since its logical rules and
%% cut-rule now allow contexts and also builds the explicit Grishin rules from
%% $\biilldc$ into the
%% logical rules, as in the original definition of the shallow nested
%% sequent calculus~\cite{csl-fill-paper}.
We defined a relation \texttt{ms\_deep\_equiv} of
\emph{multiset-equivalence}, under which any two Isabelle nested
sequents are equivalent if they would be the same if a collection of
Isabelle nested sequents, separated by commas, were considered as a multiset.
This includes where the difference between two Isabelle nested
sequents occurs at any depth. Its definition relies on a function
\texttt{ms\_of\_ns} for ``multiset of Isabelle nested sequent''
which turns (eg)
the Isabelle nested sequent
$(S, T), U$ into the multiset
%$\{#S, T, U\#\}$
\verb!{# S, T, U #}!, and a relation \texttt{ms\_ms\_deep\_equiv}, which expresses
equivalence of multisets of Isabelle nested sequents.
% While we used the relation \texttt{ms\_deep\_equiv} to describe the situation
% where two nested sequents are equivalent, we defined the shallow and deep
% nested sequent calculi $\biillsn$ and $\biilldn$ to contain rules expressing
% the monoid (commutativity, associativity and $\Phi$) rules
% (\texttt{sn\_ac0} and \texttt{dn\_ac0}), in addition to the rules shown in the
% paper.
%% An alternative in the deep nested sequent formalisation would allow us to
%% build associativity, commutativity and identity into the act of
%% instantiating a rule as guaranteed by the theorems below:
%% \begin{verbatim}
%% (["Msde.ctxt_dn_ac0_msde"],
%% "([?a], ?b) : ctxt (nrulefs dn_ac0) ==> (?a, ?b) : ms_deep_equiv"),
%% (["Msde.msde_derl"],
%% "(?a, ?b) : ms_deep_equiv
%% ==> ([?a], ?b) : derl (ctxt (nrulefs dn_ac0))"),
%% \end{verbatim}
%% A {\em context} is either a `hole' $[~]$, called the {\em empty
%% context}, or a sequent where exactly one node has been replaced by a
%% hole $[~]$. We write contexts as $X[~]$ and write $X[S]$ for the
%% sequent resulting from replacing the hole $[~]$ in $X[~]$ with the
%% sequent $S$. A non-empty context $X[~]$ is {\em positive} if the hole
%% $[~]$ occurs immediately\marginpar{Positive negative not needed by JED.}
%% to the right of a sequent arrow $\seq$, and
%% {\em negative} otherwise. Thus by overloading $\seq$ to denote the
%% structural counterparts of $\limp$ and $\excl$, we can present deep
%% inference rules that ignore context polarity.\marginpar{Should we give
%% the $\tau$-translation?}
%% \begin{proposition}[Display property]
%% \label{prop:display}
%% Let $X[~]$ be a positive (negative) context. For every
%% $\Sc$,\marginpar{Not yet proved by JED}
%% there exists $\Tc$ such that $\Tc \seq \Sc$ (respectively $\Sc \seq \Tc$)
%% is derivable from $X[\Sc]$
%% using only the structural rules from $\{ \drp_1, drp_2, \rp_1,
%% rp_2\}.$
%% Thus $\Sc$ is ``displayed'' in $\Tc\seq\Sc$ ($\Sc\seq\Tc$).
%% \end{proposition}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: