[Prev][Next][Index][Thread]

A Hitchhiker's Guide to Linear Decorating



  ---------------This is a LaTeX-file, cut here-----------------

\documentstyle{article}
\title{{\bf A Hitchhiker's Guide to \\ Linear Decorating}}
\author{{\scriptsize {by}} \\ Harold Schellinx}
\date{}
\begin{document}
\maketitle

\noindent{\small
The following gives an overview of my thesis {\em `The Noble Art of Linear
Decorating'},\/ published in the dissertation series of the Dutch Institute
for Logic, Language and Computation, University of Amsterdam.
(ILLC-Dissertation Series, 1994-1). For further information, please contact\\
}

\begin{center}
Institute for Logic, Language and Computation\\
Universiteit van Amsterdam\\
Plantage Muidergracht 24\\
1018 TV Amsterdam\\
phone: +31-20-5256090\\
fax: +31-20-5255101\\
e-mail: illc@fwi.uva.nl\\
\rule{5.3cm}{0.1mm}
\end{center}

\bigskip
Take some derivation $\pi$ in sequent calculus for classical or intuitionistic logic.
Can we transform it into a sequent derivation in linear logic in a way that essentially
preserves its structure, i.e.\ can we define a {\em linear decoration} of the original proof?
And if `yes', then is there an {\em optimal} way to do this?

The bulk of the considerations in this thesis originated in attempts to give some kind of an
answer to this, natural, question. It describes our work on the subject, major parts of it done in close
cooperation with Vincent Danos and Jean-Baptiste Joinet,
under the agreeable lee of the Universit\'{e} Paris VII's `\'{E}quipe de Logique', between spring 1992
and fall 1993.

\par\smallskip

Our main concern will be with {\em mappings}: from formulas to linear formulas, 
from classical and intuitionistic proofs to linear proofs, 
from classical (intuitionistic) proofs to classical (intuitionistic) proofs, and from linear
proofs to linear proofs, mappings that in most cases will preserve, at least, what 
we call the {\em skeleton} of the original, in the case `linear to linear' moreover its
{\em dynamics}\index{dynamics} (i.e.\ behaviour under cut elimination). 

\par\bigskip\bigskip

{\sc from formulas to linear formulas}

\par\smallskip

We define (chapter 2) {\em modal translations} of formulas into
linear formulas, which are obtained by replacing each connective
by one of its linear analogues, and prefixing each subformula by a {\em
modality}, i.e.\ a (possibly empty) string of linear exponentials. Girard's
original embedding of intuitionistic into linear logic is an example.

When turning our attention to {\em classical} logic, we find 
there exists no {\em unique} minimal choice for a modal translation. 
Instead we are confronted with {\em two} embeddings ({\sf Q}  and {\sf T}),
corresponding to distinct, one might say {\em dual}, linear decompositions of classical implication.

\par\bigskip

{\sc from classical and intuitionistic proofs to linear proofs}

\par\smallskip

Though the minimal modal embeddings of chapter 2 in general do not
automatically extend to derivations, there are (less economical) modal
translations whose inductive application to sequent proofs defines a
structure-preserving mapping of intuitionistic and classical to linear
derivations. The existence of such {\em inductive decoration strategies}
(chapter 3) 
provides a positive answer to the first part of our original
question. 
Moreover we show that in the classical case there exist essentially {\em two}
distinct modal translations whose inductive application to a proof preserves
the skeleton. We call them {\sf q} (which is closely related to the embedding
{\sf Q} of chapter 2) and {\sf t} (related to the {\sf T}-embedding).
For certain fragments, most notably the one containing the rules for
implication, universal first order quantification and universal second order
(propositional) quantification, this `linear decorating' of a classical
proof is {\em deterministic}, and unambiguously defines a procedure for
eliminating its cuts as a `reflection' of the procedure for its linear
image. It is e.g.\ immediate from the strong normalization theorem for
linear logic that these reductions for (the given fragment
of) classical sequent calculus enjoy strong normalization.

\par\smallskip

As it is essentially
the {\em absence} of exponentials that provides us with information on the
dynamics of a proof (section 4.4),	
we would like also to find {\em optimal} decorations, which,
intuitively, should be obtainable by tracing the effects of occurrences
of structural rules throughout a given proof. This is carried out
in detail for intuitionistic implicational logic in chapter 4. In the
case of derivations in classical sequent calculus, though, such a
procedure cannot be defined unequivocally, and optimality results can
only be relative to prior choices, e.g.\ by optimizing the results of
the inductive application of the modal translations of chapter 3.

\par\bigskip

{\sc from classical proofs to classical proofs, and}

{\sc from intuitionistic proofs to intuitionistic proofs}

\par\smallskip

The economic, non-decorating, embeddings of chapter 2 suggest restrictions
on the form of rules, both in intuitionistic and classical sequent
calculus. These restrictions can be built into alternative formulations
of these calculi, that remain complete for provability, and for which
the economic embeddings become decorating. We thus obtain the calculus
{\bf ILU} for intuitionistic logic, corresponding to Girard's embedding
of intuitionistic into linear logic, and the calculi {\bf LKT} and
{\bf LKQ} for classical logic, corresponding to the {\sf T}-, resp.   
the {\sf Q}-embedding of classical into linear logic. We characterize
these calculi (chapter 3) as proper fragments of linear logic:
they inherit linear logic's computational properties.

\par\smallskip

When inductively applying the economic embeddings to {\bf IL}-, resp.\
{\bf CL}-derivations, at several points we have to apply cuts, in order
for the conclusion to remain within the scope of the embedding. We refer to these cuts
as {\em correction cuts}. They are of a specific form: in all
cases one cuts with the linear decoration of a derivation of an identity
$A \Rightarrow A$. We show (chapter 6) that elimination of these cuts
realizes the restrictions imposed by the embeddings on the form of
the rules, whence we refer to them as {\em `constrictive morphisms'}\/: after elimination of the correction cuts from the derivation
obtained by inductively applying Girard's translation to an {\bf IL}-%
derivation, the skeleton of the result is an {\bf ILU}-proof. 
Similarly when applying the {\sf Q}- or {\sf T}-translation to a {\bf CL}-derivation $\pi$, elimination
of the corresponding correction cuts transforms $\pi$ into an {\bf LKQ}-,
resp.\ {\bf LKT}-proof.

\par\bigskip

{\sc from linear proofs to linear proofs}

\par\smallskip

In chapter 5 we construct the {\em exponential graph} of a linear proof $\pi$,
an artefact that displays the interdependencies of exponentials. 
Using this graph we characterize exponentials that are superfluous.
Removing (`stripping') them determines a lattice of linear derivations with top $\pi$ and
as bottom a unique normal form $\pi^{\triangleright}$, having essentially the
same set of reductions. When applying this removal to the linear derivation
 obtained by inductively applying a decorating modal translation to an
{\em intuitionistic} derivation $\pi$, the result obtained is essentially
equivalent to the linear derivation $\partial(\pi)$ constructed in
chapter 4 by
tracing the effects of occurrences of structural rules throughout $\pi$,
whence $\partial(\pi)$ is shown to be the optimal linear decoration of
$\pi$.

We similarly may apply stripping to the result of the inductive application
of decorating modal translations to {\em classical} derivations, in which
case we obtain optimal decorations relative to the chosen initial
decoration (i.e.\ relative to the choice of a normalization protocol for
the original proof).

\par\smallskip

`Stripping' in fact is a basic example of {\em dilatation} (chapter 8)
of linear derivations, i.e.\ the replacement of exponentiated formulas
by non-exponentiated ones in such a way that the reductions of
the original can be simulated by reductions of the image. 
We show that a (fully expanded) linear derivation $\pi$ is, in some strong
sense, dilatable 
if and only if its exponential graph is acyclic.
\end{document}