\documentclass[11pt,twoside]{article}

\usepackage{latexsym}
\usepackage{code}
\usepackage{proof}
\usepackage{fancyhdr}
\usepackage{lecnotes}

\newcommand{\lecdate}{October 12, 2006}
\newcommand{\lecnum}{14}
\newcommand{\lectitle}{Cut Elimination}

\begin{document}

\maketitle

\noindent
In this lecture we consider how to prove that connectives are
asynchronous as goals and then consider cut elimination, one of
the most important and fundamental properties of logical systems.
We then revisit residuation to restore some of the connectives
not present in the asynchronous fragment of linear logic.  For
each synchronous assumption we find a corresponding synchronous
goal connective.

\setcounter{section}{\lecnum}
\subsection{Proving Connectives Asynchronous}

We have claimed in the last lecture that certain connectives
of linear logic are asynchronous as goals in order to justify
their inclusion in our linear logic programming language.
I know of essentially two ways to prove that such operators
are indeed asynchronous.  The first is by simple inductions,
one for each asynchronous connectives.  The
following theorem provides an example.  In todays lecture
we generally omit the judgment form for propositions such
as $\jtrue$ on the right-hand side, and $\jres$ or $\ures$
on the left-hand side, since this can be infered from
the placement of the proposition.

\begin{theorem}
If $\Delta \ldash A \lwith B$ then $\Delta \ldash A$
and $\Delta \ldash B$.
\end{theorem}
\begin{proof}
By induction on the structure of $\DD$, the deduction of $\Delta
\ldash A \lwith B$.  We show only two cases; others are similar.
\begin{description}
\item[Case:]
$\DD = \lowered{\infer[{\lwith}R.]{\Delta \ldash A \lwith B}
             {\deduce{\Delta \ldash A}{\DD_1} &
              \deduce{\Delta \ldash B}{\DD_2}}}$
\begin{tabbing}
$\Delta \ldash A$ \` Subderivation $\DD_1$ \\
$\Delta \ldash B$ \` Subderivation $\DD_2$
\end{tabbing}
\item[Case:]
$\DD = \lowered{\infer[{\lwith}L_1]{\Delta', C_1 \lwith C_2 \ldash A \lwith B}
             {\deduce{\Delta', C_1 \ldash A \lwith B}{\DD_1}}}$
where $\Delta = (\Delta', C_1\lwith C_2)$.
\begin{tabbing}
$\Delta', C_1 \ldash A$ and \\
$\Delta', C_1 \ldash B$ \` By i.h.\ on $\DD_1$ \\
$\Delta', C_1 \lwith C_2 \ldash A$ \` By rule ${\lwith}L_1$ \\
$\Delta', C_1 \lwith C_2 \ldash B$ \` By rule ${\lwith}L_1$ 
\end{tabbing}
\end{description}
\end{proof}

There is a second way to proceed, using the admissibility
of cut from the next section directly, without appeal to
induction.

\subsection{Admissibility of Cut}

So far we have not justified that the right and left rules
for the connectives actually match up in an expected way.
What we would like to show is that the judgment of a being resource
and the judgment of truth, when combined in a linear
hypothetical judgment, coincide.  There are two parts to
this.  First, we show that with the resource $A$ we
can achieve the goal $A$, for arbitrary $A$ (not just
atomic predicates).

\begin{theorem}[Identity Principle]
$A\,\jres \ldash A\;\jtrue$ for any proposition $A$.
\end{theorem}
\begin{proof}
See Exercise 12.1.
\end{proof}

Second, we show that if we can achieve $A$ as a goal, it is
legitimate to assume $A$ as a resource.  This completes the
theorems which show our sequent calculus is properly designed.

\begin{theorem}[Admissibility of Cut]\mbox{}\newline
If $\Delta_A \ldash A\;\jtrue$ and $\Delta_C, A\,\jres \ldash
C\;\jtrue$ then $\Delta_C, \Delta_A \ldash C\;\jtrue$.
\end{theorem}
\begin{proof}
We prove this here only for the purely linear fragment,
without the operators involving unrestricted
resources ($\lbang A$, $A \limplies B$).  The proof
proceeds by nested induction, first on the structure
of $A$, the so-called \emph{cut formula}, then
simultaneously on the structure of $\DD$, the derivation
of $\Delta_A \ldash A\;\jtrue$ and $\EE$, the derivation
of $\Delta_C, A\,\jres \ldash C\;\jtrue$.
This form of induction means we can appeal to the induction
hypothesis
\begin{enumerate}
\item either on a smaller cut formula with arbitrary derivations, or
\item on the same cut formula $A$ and same $\DD$, but a subderivation of $\EE$, or
\item on the same cut formula $A$ and same $\EE$, but a subderivation of $\DD$.
\end{enumerate}
There are many cases to distinguish; we show only three
which illustrate the reasons behind the form of the induction above.
\begin{description}
\item[Case:]
$\DD = \lowered{\infer[{\lwith}R]{\Delta_A \ldash A_1 \lwith A_2}
                      {\deduce{\Delta_A \ldash A_1}{\DD_1} &
                       \deduce{\Delta_A \ldash A_2}{\DD_2}}}$
and $\EE = \lowered{\infer[{\lwith}L_1]{\Delta_C, A_1 \lwith A_2 \ldash C}
                          {\deduce{\Delta_C, A_1 \ldash C}{\EE_1}}}$.
% where $A = A_1 \lwith A_2$.
\begin{tabbing}
$\Delta_C, \Delta_A \ldash C$ \` By i.h.\ on $A_1$, $\DD_1$ and $\EE_1$
\end{tabbing}

\item[Case:]
$\DD = \lowered{\infer[{\otimes}R]{\Delta_1, \Delta_2 \ldash A_1 \otimes A_2}
                      {\deduce{\Delta_1 \ldash A_1}{\DD_1} &
                       \deduce{\Delta_2 \ldash A_2}{\DD_2}}}$
and $\EE = \lowered{\infer[{\otimes}L]{\Delta_C, A_1 \otimes A_2 \ldash C}
                          {\deduce{\Delta_C, A_1, A_2 \ldash C}{\EE'}}}$.
% where $\Delta_A = (\Delta_1,\Delta_2)$ and $A = A_1 \otimes A_2$.
\begin{tabbing}
$\Delta_C, A_1, \Delta_2 \ldash C$ \` By i.h.\ on $A_2$, $\DD_2$, and $\EE'$ \\
$\Delta_C, \Delta_1, \Delta_2 \ldash C$ \` By i.h.\ on $A_1$, $\DD_1$
and the previous line \\
$\Delta_C, \Delta_A \ldash C$ \` Since $\Delta_A = (\Delta_1,\Delta_2)$
\end{tabbing}

\item[Case:]
$\lowered{\deduce{\Delta_A \ldash A}{\DD}}$ is arbitrary and
$\EE = \lowered{\infer[{\lwith}L_1]{\Delta', D_1\lwith D_2, A \ldash C}
                      {\deduce{\Delta', D_1, A \ldash C}{\EE_1}}}$.
% where $\Delta_C = (\Delta', D_1 \lwith D_2)$.
\begin{tabbing}
$\Delta', D_1, \Delta_A \ldash C$ \` By i.h.\ on $A$, $\DD$ and $\EE_1$ \\
$\Delta', D_1 \lwith D_2, \Delta_A \ldash C$ \` By rule ${\lwith}L_1$
\end{tabbing}
\end{description}
\end{proof}

The shown cases are typical in that if the cut formulas were just
introduced on both the right and the left, then we can appeal to
the induction hypothesis on its subformulas.  Otherwise, we can keep
the cut formula and either $\DD$ or $\EE$ the same and appeal to
the induction hypothesis on the subderivations on the other side.

The case for $\otimes$ above shows why we cannot simply use
an induction over the derivations $\DD$ and $\EE$, because
the second time we appeal to the induction hypothesis,
one of the derivations come from a previous appeal to the
induction hypothesis and could be much larger than $\EE$.

The proof is not too difficult to extend to the case with
unrestricted assumptions (see Exercise~\ref{exc:unres-cutelim}).

\subsection{Cut Elimination}

Cut elimination is the property that if we take cut as a new
inference rule, it can be eliminated from any proof.  Actually,
here we would have two cut rules.
\[ \begin{array}{c}
\infer[\mbox{cut}]{\Gamma; \Delta_C, \Delta_A \ldash C\;\jtrue}
      {\Gamma; \Delta_A \ldash A\;\jtrue &
       \Gamma; \Delta_C, A\,\jres \ldash C\;\jtrue}
\\[1em]
\infer[\mbox{cut!}]{\Gamma ; \Delta \ldash C\;\jtrue}
      {\Gamma ; \cdot \ldash A\;\jtrue &
       (\Gamma, A\,\ures) ; \Delta \ldash C\;\jtrue}
\end{array} \]
Showing that cut can be eliminated is an entirely straightforward
induction over the structure of the deduction with cuts.  In each
case we just appeal to the induction hypothesis on each premiss
and re-apply the rule to the get the same conclusion.  The only
exception are the cut rules, in which case we obtain cut-free
derivations of the premisses by induction hypothesis and then
appeal to the admissibility of cut to get a cut-free derivation
of the conclusion.

Cut as a new rule, however, is unfortunate from the perspective
of proof search.  When read bottom-up, we have to invent a new
proposition $A$, which we then prove.  When this proof succeeds
we would be allowed to assume it into our overall proof.  While
mathematically inventing such lemmas $A$ is critical, in a logic
programming language it destroys the goal-directed character of
search.

\subsection{Asynchronous Connectives, Revisited}

Using cut elimination we can give alternate proofs that
connectives are asynchronous.  We show only one example,
for conjunction.
\begin{theorem}
If $\Delta \ldash A \lwith B$ then $\Delta \ldash A$
and $\Delta \ldash B$.
\end{theorem}
\begin{proof}
(Alternate) Direct, using admissibility of cut.
\begin{tabbing}
$\Delta \ldash A \lwith B$ \` Given \\
$A \ldash A$ \` Identity principle \\
$A \lwith B \ldash A$ \` By rule ${\lwith}L_1$ \\
$\Delta \ldash A$ \` By admissibility of cut \\[1em]
$B \ldash B$ \` Identify principle \\
$A \lwith B \ldash B$ \` By rule ${\lwith}L_2$ \\
$\Delta \ldash B$ \` By admissibility of cut
\end{tabbing}
\end{proof}

\subsection{Residuation and Synchronous Goal Connectives}

In the focusing calculus from the previous lecture, all
connectives are asynchronous as goals and synchronous when in
focus as assumptions.  In our little programming example of peg
solitaire, we extensively used simultaneous conjunction
($\otimes$) and and also disjunction ($\oplus$).  One question is
how to extend our language to include these connectives.
So far, we have, for both programs and goals:
\[ \begin{array}{lcl}
A & ::= & P \mid A_1 \lolli A_2 \mid A_1 \lwith A_2
\mid \top \mid \forall x\ldot A \mid A_1 \limplies A_2
\end{array} \]

A principled way to approach this question is to return
to residuation.  Given a program clause this constructs
a goal whose search behavior is equivalent to the behavior
of the clause.  Since we have already seen residuation
in detail for the non-linear case, we just present the
rules here.
\[ \begin{array}{c}
\infer{P' \ldash P \resid P' \doteq P}{\mathstrut}
\hspace{3em}
\infer{G_2 \lolli D_1 \ldash P \resid G_1 \otimes G_2}
      {D_1 \ldash P \resid G_1}
\\[1em]
\infer{D_1 \lwith D_2 \ldash P \resid G_1 \oplus G_2}
      {D_1 \ldash P \resid G_1 &
       D_2 \ldash P \resid G_2}
\hspace{3em}
\infer{\top \ldash P \resid \lzero}{\mathstrut}
\\[1em]
\infer{\forall x\ldot D \ldash P \resid \exists x\ldot G}
      {D \ldash P \resid G & x \notin \FV(P)}
\hspace{3em}
\infer{G_2 \limplies D_1 \ldash P \resid G_1 \obang G_2}
      {D_1 \ldash P \resid G_1}
\end{array} \]

There are a few connectives we have not seen in their full
generality in linear logic, namely equality, existential
quantification, and a curious asymmetric connective $G_1 \obang
G_2$.  We concentrate here on their behavior as goals
(see Exercise~\ref{exc:new-goals}).
Because these connectives mirror the synchronous behavior
of the assumption in focus, proving one of these is now
a focusing judgment, except that we focus on a goal.
We write this as $\Gamma ; \Delta \rfocus G$.

First, in our proof search judgment we replace the
$\mbox{focus}$ and $\mbox{copy}$ rules by appeals
to residuation.  
\[ \begin{array}{c}
\infer[\mbox{resid!}]{\Gamma ; \Delta \ldash P}
      {D \in \Gamma &
       D \ldash P \resid G &
       \Gamma ; \Delta \rfocus G}
\\[1em]
\infer[\mbox{resid}]{\Gamma ; \Delta, D \ldash P}
      {D \ldash P \resid G &
       \Gamma ; \Delta \rfocus G}
\end{array} \]
Next the rules for focusing on the right.
\[ \begin{array}{c}
\infer[\mbox{id}]{\Delta \rfocus P \doteq P}
      {\Delta = (\cdot)}
\hspace{3em}
% \begin{array}{l}
% \mbox{no rule for $P' \doteq P$ if $P' \not= P$}
% \end{array}
% \\[1em]
\infer[{\otimes}R]{\Delta \rfocus G_1 \otimes G_2}
      {\Delta = (\Delta_1, \Delta_2) &
       \Delta_1 \rfocus G_1 &
       \Delta_2 \rfocus G_2}
\\[1em]
\infer[{\oplus}R_1]{\Delta \rfocus G_1 \oplus G_2}
      {\Delta \rfocus G_1}
\hspace{3em}
\infer[{\oplus}R_2]{\Delta \rfocus G_1 \oplus G_2}
      {\Delta \rfocus G_2}
\hspace{3em}
\deduce{\Delta \rfocus \lzero}
       {\mbox{no ${\lzero}R$ rule for}}
\\[1em]
\infer[{\exists}R]{\Delta \rfocus \exists x\ldot G}
      {\Delta \rfocus G(t/x)}
\hspace{3em}
\infer[{\obang}R]{\Gamma; \Delta \rfocus G_1 \obang G_2}
      {\Gamma; \Delta \rfocus G_1 &
       \Gamma; \cdot \rfocus G_2}
\end{array} \]
Furthermore, we transition back to asynchronous
decomposition when we encounter an asynchronous
connective.  We call this \emph{blurring} the
focus.  Conversely, we focus on the right when
encountering a synchronous connective.
\[ \infer[\mbox{blur}]{\Delta \rfocus G}
         {\Delta \ldash G &
	  \mbox{$G$ asynch.}}
\hspace{3em}
\infer[\mbox{rfocus}]{\Delta \ldash G}
         {\Delta \rfocus G &
          \mbox{$G$ synch.}}
\]
For completeness, we give the remaining rules for asynchronous goals
(the atomic case is above in the $\mbox{resid}$ and $\mbox{resid!}$
rules).
\[ \begin{array}{c}
\infer[{\lolli}R]{\Delta \ldash D_1 \lolli G_2}
         {\Delta, D_1 \ldash G_2}
\hspace{3em}
   \infer[{\lwith}R]{\Delta \ldash G_1 \lwith G_1}
         {\Delta \ldash G_1 &
          \Delta \ldash G_2}
\hspace{3em}
\infer[{\top}R]{\Delta \ldash \top}
         {\mathstrut}
\\[1em]
\infer[{\forall}R]{\Delta \ldash \forall x\ldot G}
      {\Delta \ldash G &
       x \not\in \FV(\Gamma; \Delta)}
\hspace{3em}
\infer[{\limplies}R]{\Gamma ; \Delta \ldash D_1 \limplies G_2}
      {(\Gamma, D_1); \Delta \ldash G_2}
\end{array} \]

This yields the following grammar of so-called \emph{linear
hereditary Harrop formulas} which form the basis of the Lolli
language.  The fragment without $\lolli$ and $\otimes$, replacing
$\land/\lwith, \lor/\oplus, \bot/\lzero, \land/\obang$, is called
\emph{hereditary Harrop formulas} and forms the basis for
$\lambda$Prolog.
\[ \begin{array}{llcc@{\;\mid\;}c@{\;\mid\;}c@{\;\mid\;}c@{\;\mid\;}c@{\;\mid\;}c}
\mbox{Goals} & G & ::= \\
\quad\mbox{Asynch.} & & & P & D_1 \lolli G_2 & G_1 \lwith G_2
& \top & \forall x\ldot G & D_1 \limplies G_2 \\
\quad\mbox{Synch.} & & \mid & P' \doteq P & G_1 \otimes G_2 &
G_1 \oplus G_2 & \lzero & \exists x\ldot A & G_1 \obang G_2 \\[1ex]
\mbox{Programs} & D & ::= & P & G_2 \lolli D_1 & D_1 \lwith D_2
& \top & \forall x\ldot D & G_2 \limplies D_1
\end{array} \]
We have lined up the synchronous goals with their counterparts
as synchronous programs just below, as explained via
residuation.

Strictly speaking, going back and forth between the $\Delta
\ldash G$ and $\Delta \rfocus G$ is unnecessary: we could
coalesce the two into one because programs are always fully
synchronous.  However, it highlights the difference between the
synchronous and asynchronous right rules: Asynchronous
decomposition in $\Delta \ldash G$ is automatic and involves no
choice, synchronous decomposition $\Delta \rfocus G$ involves a
significant choice and may fail.  Moreover, in just about any
logical extension of focusing beyond this fragment, we need to
pause when the goal becomes synchronous during the asynchronous
decomposition phase and consider whether to focus on an
assumption instead.  Here, this would always fail.

In practice, it is convenient to admit an even slightly
richer set of goals, whose meaning can be explained either via
a transformation to the connectives already shown
above or directly via synchronous or asynchronous rules
for them (see Exercise~\ref{exc:more-goals}).

\subsection{Completeness of Focusing}

Soundness of the focusing system is easy to see, since each rule
is a restriction of the corresponding left and right rules for
the non-focused sequent calculus.  Completeness is somewhat more
difficult.  We can continue the path mapped out in the proof that
various connectives are asynchronous as goals, proving that the
same connectives are indeed synchronous as programs.
Alternatively, we can prove a generalization of the cut
elimination results for focused derivations and use that in an
overall completeness proof.  The references below give some
pointers to the two different styles of proof in the literature.

\subsection{Historical Notes}

Cut elimination, one of the most fundamental theorems in logic,
is due to Gentzen~\cite{Gentzen35}, who introduced the sequent
calculus and natural deduction for both classical and
intuitionistic logic and showed cut elimination.  His formulation
of the sequent calculus had explicit rules for exchange, weaking,
and contraction, which make the proof somewhat more tedious than
the one we presented here.  I first provided proofs by simple
nested structural induction, formalized in a logical framework,
for intuitionistic and
classical~\cite{Pfenning94tra,Pfenning00ic} as well as linear
logic~\cite{Pfenning94trb}.

Andreoli introduced focusing for classical linear
logic~\cite{Andreoli92} and proved its completeness through a
number of inversion and admissibility properties.  An alternative
proof using cut elimination as a central lemma, applied to
intuitionistic linear logic was given by
Chaudhuri~\cite{Chaudhuri06phd}.

\subsection{Exercises}

\begin{exercise}
Prove $A \lolli B$ to be asynchronous on the right in two ways:
\begin{enumerate}\renewcommand{\theenumi}{\roman{enumi}}
\item directly by induction, and
\item by appealing to the admissibility of cut.
\end{enumerate}
\end{exercise}

\begin{exercise}
\label{exc:unres-cutelim}
In order to prove the cut elimination theorem in the presence
of unrestricted assumptions, we generalize to the following:
\begin{enumerate}
\item (Cut) If $\Gamma ; \Delta_A \ldash A\;\jtrue$ and $\Gamma ; \Delta_C, A\,\jres \ldash
C\;\jtrue$ then $\Gamma ; \Delta_C, \Delta_A \ldash C\;\jtrue$.
\item (Cut!) If $\Gamma ; \cdot \ldash A\;\jtrue$
and $(\Gamma, A\,\ures) ; \Delta_C \ldash C\;\jtrue$ then
$\Gamma ; \Delta_C \ldash C\;\jtrue$
\end{enumerate}
The second form of cut expresses that if we can prove $A$ without
using resources, it is legitimate to assume it as an unrestricted
resource, essentially because we can generate as many copies of
$A$ as we need (it requires no resources).

The nested induction now proceeds first on the structure
of the cut formula $A$, then on the form of cut where $\mbox{cut} < \mbox{cut!}$, then simultaneously on the structures of the two given derivations
$\DD$ and $\EE$.  This means we can appeal to the induction
hypothesis
\begin{enumerate}
\item either on a subformula of $A$ with arbitrary derivations, or
\item on the same formula $A$ where $\mbox{cut!}$ appeals to $\mbox{cut}$, or
\item on the same cut formula and same form of cut and same $\DD$, but a subderivation of $\EE$, or
\item on the same cut formula and same form of cut and same $\EE$, but a subderivation of $\DD$.
\end{enumerate}

Show the cases explicitly involving $\lbang A$, $A \limplies B$,
and $\mbox{copy}$ in this proof.  You may assume that weakening
the unrestricted assumptions by adding more is legitimate and does
not change the structure of the given deduction.  Note carefully
appeals to the induction hypothesis and explain why they are
legal.
\end{exercise}

\begin{exercise}
\label{exc:more-goals}
We consider even larger set of goals to squeeze the last
bit of convenience out of our language without actually affecting
its properties.
\begin{enumerate}\renewcommand{\theenumi}{\roman{enumi}}
\item Give the rule(s) to allow $\lbang G$ as a goal.
\item Give the rule(s) to allow $\lone$ as a goal.
\item We could allow simultaneous conjunction on
the left-hand side of linear implication goals, because $(D_1
\otimes D_2) \lolli G$ is equivalent to $D_1 \lolli (D_2 \lolli
G)$, which lies within the permitted fragment.  Explore which
formulas $R$ could be allowed in goals of the form $R \lolli G$
because they can be eliminated by a local equivalence-preserving
transformation such as the one for $\otimes$.
\item Now explore which formulas $S$ could be allowed
in goals of the form $S \limplies G$ without affecting
the essence of the language.
\end{enumerate}
\end{exercise}

\begin{exercise}
Prove that the focusing system with left and right rules
is equivalent to the system with only right rules and
residuation for atomic goals.
\end{exercise}

\begin{exercise}
\label{exc:new-goals}
Through residuation, we have introduced two new connectives to
linear logic, $A \obang B$ and $P' \doteq P$, but we have only
considered their right rules.

Give corresponding left rules for them in the sequent calculus
and prove cut elimination and identity for your rules.
\end{exercise}

\subsection{References}

\bibliographystyle{plain}
\bibliography{lp}

\end{document}