[Prev][Next][Index][Thread]
(Im)Permutabilities of LL
Date: Sat, 30 Nov 91 18:28:50 -0800
To: linear@cs.stanford.edu
In order to make clear what sorts of permutabilities I was talking
about in the discussion of sequentialized kingdoms and empires, here
is a table I have been using which lists all impermutabilities of
linear logic. I'm sure that many others have already discovered these
impermutabilities, perhaps in terms of giving normal forms for linear
logic proofs. For example, Girard, Bellin, Andreoli, Pareschi, Pym,
Miller, just to name a few, have given parts of the table below
implicitly and explicitly in their work (Girard's proof of the
sequentialization theorem for proof nets immediately yields the
permutability of par downward in sequent proofs. Andreoli and
Pareschi's `focusing proofs' heavily utilize many permutabilities.
Bellin has produced a table similar to this one in a recent paper, etc.)
In any any case, I think this presentation is informative.
(This is almost readable in ascii, but it can be LaTeXed as is.)
Patrick Lincoln.
% -----------cut here------------
\documentstyle[12pt,fullpage]{article}
\begin{document}
The following is a list of some impermutabilities of Linear Logic.
A rule R for the main connective of a formula C is permutable below
another rule R' for the main connective of formula C' (C not a
subformula of C') if for any proof with C reduced immediately above
C', then there is a proof with C reduced immediately below C'. Using
other terminology (see Bellin, for example), an inference R permutes
below an inference R' if and only if for any proof where R occurs
immediately above R', and the principal formula of R is not active in
R', there is a proof where R occurs immediately below R'. It is
easiest to consider cut-free proofs, although one may also study
permutabilities involving cut if one is careful with the definitions.
Any numeral in the following table should be read as ``the connective
of this column cannot always permute below the connective of this
row''. For example, number 9 shows that $\exists$ cannot always
permute below $\forall$. Example 9 is essentially the same example
that shows quantifier impermutability in classical logic. That is,
the $\forall$ must be instantiated lower in the proof tree than the
$\exists$ in sequent 9 in classical as well as linear logic. However,
classical logic enjoys all other possible permutabilities, while
intuitionistic and linear logic have many impermutabilities.
Note that $I$, $1$, and $\top$ are trivial cases, since they have no
hypotheses. Also, $!S$ is only rarely permutable, since it requires
all other formulas to be prefixed with ?, (although here only the !'d
formula is considered principal in an application of !S). In all
permutable cases for $!S$, except versus $?W$ and $?C$, the
permutability is trivial. (There are no proofs with $\otimes$
immediately above $!S$ where the principal formulas are not subformula
of one another.)
\newcommand{\Par}{\mbox{\raisebox{.4ex}{$\wp$}}}
\[ \begin{array}{c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|}
&\otimes &\Par &\& &\oplus &?W &?C &?D &!S &\bot &\forall &\exists &Cut\\
\hline %% * par & + ?W ?C ?D !S &bot A E Cut
\otimes & & & & & & & & 0 & & & & \\\hline
\Par & 1 & & & & & & & 0 & & & & - \\\hline
\& & 2 & & & 3 & 4 & & 5 & 0 & & & 6 & - \\\hline
\oplus & & & & & & & & 0 & & & & \\\hline
?W & & & & & & & & & & & & \\\hline
?C & 7 & & & & & & & & & & & - \\\hline
?D & & & & & & & & & & & & \\\hline
!S & & & & & & & 8 & & & & & - \\\hline
\bot & & & & & & & & 0 & & & & \\\hline
\forall & & & & & & & & 0 & & & 9 & \\\hline
\exists & & & & & & & & 0 & & & & \\\hline
Cut & & & & & & & & - & & & & \\\hline
\end{array} \hspace{.6cm}\begin{array}{rl}
0 & \mbox{various examples} \\
1 & \vdash (A \Par B), (A^{\perp} \otimes B^{\perp}) \\
2 & \vdash (A \& B), (\bot \otimes \top), A^{\perp}, B^{\perp} \\
3 & \vdash (A \& B), (A^{\perp} \oplus B^{\perp}) \\
4 & \vdash (1 \& A), ?A^{\perp} \\
5 & \vdash ((!A) \& A), ?A^{\perp} \\
6 & \vdash (A(t)^{\perp} \& A(u)^{\perp}), \exists x.A(x) \\
7 & \vdash ?A, (A^{\perp} \otimes A^{\perp}) \\
8 & \vdash !(A^{\perp} \oplus B), ?A\\
9 & \vdash \forall y. (A(y) \oplus B), \exists x. A(x)^{\perp} \\
\end{array} \]
Note that numbers 4 and 5 are special: if we change the
definition of permutable to ``... if for any proof with C reduced
immediately above C' IN ALL HYPOTHESES, then there is a proof with C
reduced immediately below C'', then 4 and 5 become permutable. Also,
the impermutabilities involving Cut (labeled $-$) are sensitive to the
exact definitions used: here the cut formula must be the same in the
permuted proof, etc. With these definitions Cut versus $\&$ is
special in the same sense as cases 4 and 5.
Patrick Lincoln \end{document}