\section{Deep Inference and Proof Search}
\label{sec:nested-sequent}

We now present a refinement of the display calculus $\biilldc$,
in the form of a nested sequent calculus, that is more suitable
for proof search. A nested sequent
%can be seen as a tree of traditional two-sided sequents. 
%It
is essentially just a structure in display calculus, but presented in a more sequent-like notation. 
This change of notation allows us to present the proof systems much more concisely. 
The proof system we are interested in is the deep inference
system in Sec.~\ref{sec:deep}, but we shall first present an intermediate system, 
$\biillsn$, which is closer to display calculus, and which eases the proof of
correspondence between the deep inference calculus and the display calculus for $\biill.$

%% that we have just presented satisfies cut-elimination, it does not
%% behave nicely with respect to proof search. This is essentially because
%% it lacks a true subformula property; although one never needs to introduce
%% new formula connectives going upwards in proof construction, the display postulates
%% and other structural rules allow one to create new structural connectives.
%% So in this sense, subformula property in display calculus does not give us
%% immediately a bound on the size of the structures created during proof search,
%% even when contraction is absent. 

\subsection{The Shallow Inference Calculus}
\label{sec:shallow}


%% Consider the full intuitionistic linear logic extended with the exclusion
%% operator $\excl$. Formulas are ranged over by lower-case Greek letters;
%% atomic formulae are ranged over by $a$,$b$,$c$, etc. 
The syntax of nested sequents is given by the grammar 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 sequents, and $\Sc$, $\Xc$, etc., for
multisets of sequents and formulae. The empty multiset is 
$\sunit$ (`dot'). 
% We use $\Gamma$ and $\Delta$ to denote multisets of formulae and 
% $P$, $Q$, $S$, $T$, $X$, $Y$, etc., to denote sequents, and $\Sc$, $\Xc$, etc., to
% denote multisets of sequents and formulae. The empty multiset is denoted by 
% $\sunit$ (`dot'). 

%% The empty multiset corresponds to the
%% structural unit $\Phi.$ To reduce clutter of symbols, we shall use $\sunit$ (`dot') to 
%% represent the empty multiset. 


A nested sequent can naturally be represented as a tree structure as follows.
The nodes of the tree are traditional two-sided sequents (i.e., pairs of multisets). The edges
between nodes are labelled with either a $-$, denoting nesting to the left of the sequent
arrow, or a $+$, denoting nesting to the right of the sequent arrow. For example,
the nested sequent below
can be visualised as the tree in Fig.~\ref{fig:partition} (i):
\begin{equation}
  \label{eq:1}
(e,f \seq g), (p, (u,v \seq x,y) \seq q,r), a, b \seq c, d, (\cdot \seq s)
\end{equation}
A display sequent can be seen as a nested sequent, where $\turn$,
$>$ and $<$ are all replaced by $\seq$ and the unit $\Phi$ is represented by the empty multiset.
%, and interpreting the structural
%connective `,' (comma) as multiset union, and $\Phi$ as the empty multiset. 
The definition of a nested sequent incorporates implicitly the associativity and
commutativity of comma, and the effects of its unit, via the multiset structure.

\begin{definition}\label{def:tau_nested}
Following Def.~\ref{def:tau}, we can translate nested sequents into equivalence
classes of BiILL-formulae (modulo associativity, commutativity, and unit laws)
via
%antecedent and succedent
\emph{$\tau$-translations}:
$$
\begin{array}{l}
\tau^a(S_1,\dots,S_k, A_1,\dots,A_m \seq B_1,\dots,B_n, T_1,\dots,T_l) \\
= 
(\tau^a(S_1) \ltens \cdots \ltens \tau^a(S_k) \ltens A_1 \ltens \cdots \ltens A_m) 
\excl
(B_1 \parr \cdots \parr B_n \parr \tau^s(T_1) \parr \cdots \parr \tau^s(T_l))
\\[1em]
\tau^s(S_1,\dots,S_k, A_1,\dots,A_m \seq B_1,\dots,B_n, T_1,\dots,T_l) \\
= 
(\tau^a(S_1) \ltens \cdots \ltens \tau^a(S_k) \ltens A_1 \ltens \cdots \ltens A_m) 
\limp
(B_1 \parr \cdots \parr B_n \parr \tau^s(T_1) \parr \cdots \parr \tau^s(T_l)).
\end{array}
$$
The translations
$\tau^a$ and $\tau^s$ differ only in their translation of the sequent symbol
$\seq$ to $\limp$ and $\excl$ respectively. Where $m = 0$, $A_1\ltens\cdots
\ltens A_m$ translates to $I$, and similarly $B_1\parr\cdots\parr B_n$
translates to
$\bot$ when $n =0$. These translations each extend to a map from multisets of nested
sequents and formulae to formulae: $\tau^a$ (resp. $\tau^s$) acts on each
sequent as above, leaves formulae unchanged, and connects the resulting formulae
with $\otimes$ (resp. $\parr$). Empty multisets are mapped to $I$ (resp.
$\bot$).
\end{definition}

%% Conversely, a
%% nested sequent can be translated to an equivalence class of structures (modulo 
%% the associativity, commutativity and unit laws for `,') 
%% by replacing sequent arrows in negative positions with $<$, and those in positive positions with $>$. 

%% the nested sequent $(\Gamma_1, (\Gamma_2 \seq \Delta_2), (\Gamma_3 \seq \Delta_3)
%% \seq \Delta_1, (\Gamma_4 \seq \Delta_4) )$ can be visualised as the following tree: 
%% $$
%% \xymatrix{
%%  & {\Gamma_1 \seq \Delta_1} \ar[dl]_{-} \ar[d]_{-} \ar[dr]^{+} \\
%% {\Gamma_2 \seq \Delta_2} & {\Gamma_3 \seq \Delta_3} & \Gamma_4 \seq \Delta_4
%% }
%% $$

A {\em context} is either a `hole' $[~]$, called the {\em empty context}, 
%or a sequent containing exactly one occurrence of $[~]$. 
or a sequent where exactly one node has been replaced by a hole $[~]$. 
Contexts are denoted by $X[~]$.
We write $X[S]$ to denote a 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
to the right of a sequent arrow $\seq$, and {\em negative} otherwise.
%\footnote{
This simple definition of polarities of a context is made possible by the use of the same symbol $\seq$
to denote the structural counterparts of $\limp$ and $\excl$. 
As we shall see in Sec.~\ref{sec:deep}, this overloading of $\seq$ allows a
presentation of deep inference rules that ignores context polarity. 
%A formula $A$ occurs negatively (positively) in a nested sequent $X$ iff 
%there exists a negative (resp. positive) context $Y[~]$ such that $X = Y[A].$

%% It is not difficult to see that this definition of contexts coincides with
%% the similar definition in display calculus presented earlier. 
%% The reader is invited to check that
%% this simpler definition of context polarity coincides with the definition in display calculus presented earlier.
%% %}

%% Since a nested sequent is just a notational variance of a display structure, the definition
%% of a context can be defined similarly as in the display case. However, because we
%% overload the symbol $\seq$ to denote both $<$ and $>$, we obtain a simpler characterisation
%% of context polarities: a {\em positive} ({\em negative}) 
%% context is a context where the hole appears immediately to the right (resp. left) of a
%% sequent arrow. As we shall see in Sec.~\ref{sec:deep}, this overloading of $\seq$ allows a
%% presentation of deep inference rules that ignores context polarity. 


The shallow inference system $\biillsn$ for $\biill$ is given
in Fig.~\ref{fig:fbills}.
%Notice that we split each of the (invertible) display postulates into 
%two rules, e.g., $drp$ is split into $drp_1$ and $drp_2$, to ease the transition
%into the deep inference system. 
%We split the display postulates $rp$ (resp. $drp$) into two rules,
%and add a dual version of the Grishin(b) rule ($gl$). These rules make the transition to the
%deep inference system easier. Other than these, the
The main difference from $\biilldc$ is that
we allow multiple-conclusion logical rules. This implicitly builds the Grishin (b) rules into 
the logical rules (see \cite{ARXIV}). 
%We state the equivalence of $\biilldc$ and $\biillsn$ below; the proof can be
%found in the appendix. 

\begin{theorem}
\label{thm:biill-sn-eq-dc}
A formula is cut-free $\biillsn$-provable iff it is cut-free $\biilldc$-provable. 
\end{theorem}
% \begin{theorem}
% \label{thm:biill-sn-eq-dc}
% A formula $A$ is cut-free provable in $\biillsn$ iff it is cut-free provable in $\biilldc$. 
% \end{theorem}

\begin{corollary}
\label{cor:cut-elim-biillsn}
The cut rule is admissible in $\biillsn.$
\end{corollary}

Just as in display calculus (Thm. \ref{thm:display}), the display property holds
for $\biillsn$. 

\begin{proposition}[Display property]
\label{prop:display}
Let $X[~]$ be a positive (negative) context. For every $\Sc$,
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}

\begin{figure}[t]
{\footnotesize
$$
\begin{array}{ccc}
\mbox{$
\xymatrix@C=0pt@R=12pt{
 & {a, b \seq c,d} \ar[dl]_{-} \ar[d]^{-} \ar[dr]^{+}\\
{e,f \seq g} & {p \seq q,r} \ar[d]^{-} & {\cdot \seq s} \\
 & {u, v \seq x,y }
}
$}
&
\mbox{
$
\xymatrix@C=0pt@R=12pt{
 & {a \seq c} \ar[dl]_{-} \ar[d]^{-} \ar[dr]^{+}\\
{e \seq g} & {p \seq } \ar[d]^{-} & {\cdot \seq \cdot} \\
 & { u \seq x }
}
$}
&
\mbox{
$
\xymatrix@C=0pt@R=12pt{
 & {b \seq d} \ar[dl]_{-} \ar[d]^{-} \ar[dr]^{+}\\
{f \seq \cdot} & {\cdot \seq q,r} \ar[d]^{-} & {\cdot \seq s} \\
 & {v \seq y }
}
$} \\
(i) & (ii) & (iii)
\end{array}
$$
}
\caption{A tree representation of a nested sequent (i), and its partitions (ii and iii). }
\label{fig:partition}
\end{figure}

\begin{figure}[t]
{\small
Cut and identity: 
$
\qquad
\vcenter{
\infer[id]
{p \seq p}{}
}
\qquad
\vcenter{
\infer[cut]
{\Sc,\Tc \seq \Sc', \Tc'}
{\Sc \seq \Sc', A & A, \Tc \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}
$$

%% $$
%% \infer[\drp_1]
%% {(\Sc \seq \Tc) \seq \Tc'}
%% {\Sc \seq \Tc, \Tc'}
%% \qquad
%% \infer[drp_2]
%% {\Sc \seq \Tc, \Tc'}
%% {(\Sc \seq \Tc) \seq \Tc'}
%% $$
%% $$
%% \infer[\rp_1]
%% {\Sc \seq (\Tc \seq \Tc')}
%% {
%% \Sc, \Tc \seq \Tc'
%% }
%% \qquad
%% \infer[rp_2]
%% {\Sc, \Tc \seq \Tc'}
%% {\Sc \seq (\Tc \seq \Tc')}
%% $$
%% $$
%% \infer[gl]
%% {(\Sc, \Tc \seq \Sc') \seq \Tc'}
%% {(\Sc \seq \Sc'), \Tc \seq \Tc'}
%% \qquad
%% \infer[gr]
%% {\Sc \seq (\Sc' \seq \Tc', \Tc)}
%% {
%%  \Sc \seq (\Sc' \seq \Tc'), \Tc
%% }
%% $$

Logical rules:
$$
\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$, where $gl$ and $gr$
  capture Grishin (b).}
\label{fig:fbills}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: ccc dl dr multiset Grishin iff Thm drp rp gl BiILL

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

