% FILL_exponentials.tex

\documentclass[11pt,a4paper]{article}

% Fonts and glyphs
%\usepackage[T1]{fontenc}
\usepackage{times}
%\usepackage{cmll}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{stmaryrd,bussproofs,relsize}
\usepackage[all]{xy} 
\SelectTips{cm}{}                 % - Looks pretty
\usepackage{proof}
%\usepackage{lscape}
\usepackage{pdflscape}

% Macros
\usepackage{graphicx}
\usepackage{mathpartir}
\input{macros}% local macros

\def\parr{\mathbin{\rotatebox[origin=c]{180}{$\&$}}}
\def\parrs{\mathbin{\rotatebox[origin=c]{180}{\tiny{$\&$}}}}
\def\merge{\star}

\renewcommand{\labelenumi}{(\roman{enumi})}

\def\turn{\vdash}

% Title
\title{Exponentials in FILL}
\author{Ranald Clouston and Alwen Tiu}
\date{\texttt{[Version of \today]}}

\listfiles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\maketitle

The \emph{categorical semantics} of $!$ and $?$ within non-classical linear
logic were given by Blute et al 1996, and are equivalent to the existence of
the arrows (given any objects $A,A',B$ and an arrow $f:A\to A'$):
\begin{description}
\item[Functorial:] 
  $\xymatrix{!A \ar[r] & !A'}
  \qquad
  \xymatrix{?A \ar[r] & ?A'}$
\item[(Co)monad:]
  $\xymatrix{A & !A \ar[l] \ar[r] & !!A}
  \qquad
  \xymatrix{A \ar[r] & ?A & ??A \ar[l]}
  $
\item[Weak/Contr:]
  $\xymatrix{I & !A \ar[l] \ar[r] & !A\otimes !A}
  \qquad
  \xymatrix{\bot \ar[r] & ?A & ?A\parr ?A \ar[l]}
  $
\item[Strengths:]
  $\xymatrix{!A\otimes !B \ar[r] & !(A\otimes B)}
  \qquad
  \xymatrix{?(A\parr B) \ar[r] & ?A\parr ?B}
  $
\item[\hphantom{Strengths:}]
  $\xymatrix{I \ar[r] & !I}
  \qquad
  \xymatrix{?\bot \ar[r] & \bot}
  $
\item[\hphantom{Strengths:}]
  $\xymatrix{!(A\parr ?B) \ar[r] & !A \parr ?B}
  \qquad
  \xymatrix{?A\otimes !B \ar[r] & ?(A\otimes !B)}
  $
\end{description}

In order to give display rules for these exponentials it is necessary to define
$!$- and $?$- restricted structures, which are restrictions of antecedent and
succedent structure respectively:
$$
X^! \quad::=\quad !A \mid \Phi \mid X^!,X^! \mid X^! < Y^?
$$
$$
Y^? \quad::=\quad ?B \mid \Phi \mid Y^?,Y^? \mid X^! > Y^?
$$

\begin{tabular}[c]{l@{\extracolsep{3cm}}l}
\multicolumn{2}{l}{Logical rules:}
\\[0px]
\qquad\qquad
  \AxiomC{$A\turn Y$}
  \LeftLabel{($!\turn$)\,}
  \UnaryInfC{$!A\turn Y$}
  \DisplayProof
  &
  \AxiomC{$X^!\turn B$}
  \LeftLabel{($\turn !$)\,}
  \UnaryInfC{$X^!\turn !B$}
  \DisplayProof
\\[10px]
\qquad\qquad
  \AxiomC{$A\turn Y^?$}
  \LeftLabel{($?\turn$)\,}
  \UnaryInfC{$?A\turn Y^?$}
  \DisplayProof
  &
  \AxiomC{$X\turn B$}
  \LeftLabel{($\turn ?$)\,}
  \UnaryInfC{$X\turn ?B$}
  \DisplayProof
\\%[5px]
\multicolumn{2}{l}{Structural rules:}
\\[0px]
  \qquad\qquad
  \AxiomC{$\Phi\turn Y$}
  \LeftLabel{(Wk $\turn$)\,}
  \UnaryInfC{$X^!\turn Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn \Phi$}
  \LeftLabel{($\turn$ Wk)\,}
  \UnaryInfC{$X\turn Y^?$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$X^!,X^!\turn Y$}
  \LeftLabel{(Ctr $\turn$)\,}
  \UnaryInfC{$X^!\turn Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn Y^?,Y^?$}
  \LeftLabel{($\turn$ Ctr)\,}
  \UnaryInfC{$X\turn Y^?$}
  \DisplayProof
\end{tabular}

\section{Soundness and Completeness}

Soundness can be proved for BiILL plus exponentials; this result does not
immediately extend to FILL plus exponentials because the definition of
$!$-restricted involves the structural connective $<$, which has no FILL
translation. We will show the soundness of the $!$ rules only, as the soundness
of the $?$ rules follows by exactly dual reasoning. In the proofs below we abuse
notation by omitting explicit references to $\tau$-translations.

\begin{lemma}\label{lem:!iso}
For any $!$-restricted structure $X$ there exists an arrow $\tau^a(X)\to
!\tau^a(X)$, and for any $?$-restricted structure $Y$ there exists an arrow
$?\tau^s(Y)\to\tau^s(Y)$
\end{lemma}
\begin{proof}
By mutual induction on the size of $X,Y$; we give the $!$ cases only, as the $?$
cases follow similarly.

$X=!A$: this is the comonad arrow $!A\to !!A$.

$X=\Phi$: this is the arrow $I\to !I$.

$X=X_1,X_2$: by induction there exist arrows $X_i\to !X_i$, so by the
functoriality of $\otimes$ we have $X_1\otimes X_2\to !X_1\otimes !X_2$. This
composes with $!X_1\otimes !X_2\to !(X_1\otimes X_2)$.

$X=W<Y$: we proceed by composing the following arrows: $W\to !W$ (induction);
$\to !(Y\parr(W\excl Y))$ (applying the functoriality of $!$ to the unit of
the coclosure); $\to !(?Y\parr(W\excl Y))$ (the monad arrow $Y\to ?Y$ along with
the functoriality of $\parr,!$); $\to ?Y\parr !(W\excl Y)$ (strength); $\to Y
\parr !(W\excl Y)$ (by the arrow $?Y\to Y$ existing by induction,
along with the functoriality of $\parr$). The arrow $W\to Y\parr !(W\excl Y)$
is equivalent to $W\excl Y\to!(W\excl Y)$ by the adjunction.
\end{proof}

\begin{theorem}[Soundness]
The proof rules are sound for BiILL-categories with exponentials.
\end{theorem}
\begin{proof}
($!\turn$): given an arrow $A\to Y$, we can compose it with the comonad
arrow $!A\to A$ to get $!A\to Y$ as required.

($\turn !$): given $X^!\to B$ we have $!X^!\to !B$ by the functoriality of $!$;
this composes with the arrow $X^!\to !X^!$ of Lem. \ref{lem:!iso}.

(Wk $\turn$): we have $X^!\to !X^!\to I$ by Lem. \ref{lem:!iso} and the
weakening arrow; this composes with $I\to Y$.

(Ctr $\turn$): compose $X^!\to !X^!$ (Lem. \ref{lem:!iso}), $!X^!\to
!X^!\otimes !X^!$ (contraction arrow), and $!X^!\otimes !X^!\to Y$ (premise).
\end{proof}

\begin{theorem}[Completeness]
All arrows existing for the categorical semantics of $!$ and $?$ are provable by
the proof rules given.
\end{theorem}
\begin{proof}
This is routine; again we skip the dual cases.

Functoriality: given a proof of $A\turn A'$ we derive $!A\turn A'$ by ($!\turn$)
and then $!A\turn !A'$ by ($\turn !$).

Comonad: $!A\turn A$ by ($!\turn$); $!A\turn !!A$ by ($\turn !$).

Weak/Contr: by (Wk $\turn$) and (Ctr $\turn$).

Strengths: $!A\otimes !B\turn !(A\otimes B)$ and $I\to !I$ both involve
($\turn !$) and are then easy; $!(A\parr ?B)\turn !A\parr ?B$ involves first
using (drp) to display $!A$, then ($\turn !$), and then is easy.
\end{proof}

\section{Disjunction and False}

We know that we cannot put (additive) conjunction and true into the display logic
for BiILL and retain soundness for the exclusion-free fragment. However, I do not
know whether this result holds for sums, i.e. disjunction $\lor$ and false $0$, also.
Note that I use $\lor$ rather $\oplus$, following [Avron 1988] because I find
Girard's alterations to the notation of completely standard notions like disjunction
irritating.

The categorical semantics are to equip the category with finite coproducts --
given $f:A\to A'$ and $g:B\to B'$:
\begin{description}
\item[Functorial:] 
  $\xymatrix{A\lor B\to A'\lor B'}$
\item[Coproducts:]
  $\xymatrix{A\to A\lor B}
  \qquad
  \xymatrix{B\to A\lor B}
  \qquad
  \xymatrix{A\lor A\to A}
  \qquad
  \xymatrix{0\to A}
  $
\end{description}

Proof rules are given in a structure-free style:

\begin{tabular}[c]{l@{\extracolsep{3cm}}l}
\multicolumn{2}{l}{ \ }
\\[0px]
\qquad\qquad
  \AxiomC{$X\turn A$}
  \LeftLabel{($\turn \lor_1$)\,}
  \UnaryInfC{$X\turn A\lor B$}
  \DisplayProof
  &
  \AxiomC{$X\turn B$}
  \LeftLabel{($\turn \lor_2$)\,}
  \UnaryInfC{$X\turn A\lor B$}
  \DisplayProof
\\[10px]
\qquad\qquad
  \AxiomC{$A\turn X$}
  \AxiomC{$B\turn X$}
  \LeftLabel{($\lor\turn$)\,}
  \BinaryInfC{$A\lor B\turn X$}
  \DisplayProof
  &
  \AxiomC{ \ }
  \LeftLabel{($0\turn$)\,}
  \UnaryInfC{$0\turn X$}
  \DisplayProof
\end{tabular}

\ \\

Soundness and completeness proofs are routine.

\input{shallow}

\input{deep}

\section{TO DO}

\begin{description}
  \item[Raj:] Confirm that the display calculi are cut-free.
  \item[Alwen:] Refine these rules to deep nested sequent calculi.
  \item[Ranald:] Confirm the soundness of the deep nested sequent calculi with
  respect to the FILL fragment only.
  \item[Jeremy:] Fold all this into the mechanisation eventually.
\end{description}

\end{document}
