[Prev][Next][Index][Thread]
proof nets for classical MLL and linear lambda terms (401 lines)
Date: Sat, 21 Mar 92 18:31:05 GMT
To: linear@cs.stanford.edu
Every proof net for classical multiplicative linear logic (CMLL)
represents an equivalence class of linear lambda terms,
which are built also with a constructor `tensor' and its dual `let'.
In fact, each Danos-Regnier switching on a proof net determines
such a lambda term, hence a natural deduction [or sequent] derivation
in intuitionistic multiplicative linear logic (IMLL).
This property clarifies the difference between Danos and Regnier'
correctness conditions for proof nets (The structure of multiplicatives,
Arch. for Math. Log. 28, 1989) and the others, e.g., by Ketonen and myself.
The above remark results from conversations with Jacques van de Wiele.
Thanks to Jacques and Laurent Regnier for their stimulating visit to Edinburgh.
Gianluigi Bellin
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%this is TeX, not LaTeX%%%%%%%%%%%%%%%%
\magnification = \magstep1
\raggedbottom
\def\phbl0{\vrule height .5ex width .0ex} %%thin phantom box
\def\bull{\vrule height 1.3ex width 1.0ex depth -.1ex } %%black box
\def\limp{\mathrel{-\!\circ}}
\def\bang{\hbox{\bf !}}
\def\whynot{\hbox{\bf ?}}
V.~Danos, L.~Regnier and J.~van~de~Wiele, among others, have given representations
of the pure lambda-calculus in the formalism of {\it pure nets}.
These are nets that contain no formula occurrences, only expressions built from
symbols $I$ and $O$ (for input and output) using the exponentials. The links are:
$$
\hbox{axiom links}\ \overline{I\quad O}\qquad\qquad%
\hbox{cut links}\ \underline{O\quad I}\quad \hbox{and}\quad \underline{\bang O\quad \whynot I}$$
and moreover
$$
\hbox{$\wp$-links}\ {{\whynot I\quad O}\over O}\qquad
\hbox{$\otimes$-links}\ {{\bang O\quad I}\over I}
$$
together with contraction, dereliction links and $\bang$-boxes.
The choice of the $\wp$-link is motivated by the domain equation
$O \rightarrow O = O$, i.e., $\whynot I \wp O = O$, etc.
\smallskip
Clearly for the {\it linear} lambda calculus it is enough to consider
$$
\hbox{$\wp$-links}\ {{I\quad O}\over O}\quad{{O\quad I}\over O}\qquad
\hbox{$\otimes$-links}\ {{O\quad I}\over I}\quad{{I\quad O}\over I}\leqno{(i)}
$$
which in the linear typed case can be interpreted as orientations of usual proof nets.
Obviously, this yields a map from derivations in a sequent calculus
or natural deduction system for the {\it implicational fragment} of ILL
into oriented proof nets.
Notice that it is not always possible to orient a proof net $R$, using
(i) for $\otimes$- and $\wp$-links, in such a way that exactly one of the
conclusions of $R$ has value $O$.
\smallskip
The interpretation can be extended to an interpretation
of {\it linear typed lambda terms with a $\otimes$-constructor and a
{\tt let} destructor} into proof nets. Here we use the orientations
$$
\hbox{$\wp$-links}\ {{I\quad I}\over I}\qquad
\hbox{$\otimes$-links}\ {{O\quad O}\over O}\leqno{(ii)}
$$
in addition to (i). This translation has the property that,
conversely, given a proof net $R$, a choice of one of the conclusions
of $R$ as output and, for each $\wp$-link, a choice of one of the premises as output
according to (i), then we can find a corresponding term $t_{S(R)}$.
It is natural to regard such choices in terms of a {\it Danos-Regnier-switching}
$S(R)$ of a proof net $R$ (extended to the choice of one conclusion of $R$).
This remark clarifies the connection between proof-nets for classical multiplicative
linear logic CMLL and natural deduction systems [or sequent calculi] for
intuitionistic linear logic IMLL: each proof net R in {\it classical} MLL
represents an equivalence class $\{{\cal D}_i\}$ of natural deduction derivations
for {\it intuitionistic} MLL, hence also an equivalence class of sequent derivations in MLL.
Let ${\cal D}_i$, ${\cal D}_j$ be derivations of $\Gamma_i \vdash A_i$
and $\Gamma_j \vdash A_j$, respectively. Then $(\bigotimes \Gamma_i) \limp A_i$
and $(\bigotimes \Gamma_j) \limp A_j$ are provably equivalent in CMLL,
(not necessarily in IMLL).
\smallskip
If we allow also assignments
$$
\hbox{$\wp$-links}\ {{O\quad O}\over O}\qquad
\hbox{$\otimes$-links}\ {{I\quad I}\over I}\leqno{(iii)}
$$
in addition to (i) and (ii), then there is a one to one map between oriented
proof-nets and derivations in a two-sided sequent formulation of CMLL
in the language with $(\cdot)^{\bot}$, $\otimes$, $\limp$ and $\wp$.
\smallskip
The system of Full Intuitionistic Linear Logic (V. de Paiva and M. Hyland)
has the language with ${\bot}$, $\otimes$, $\limp$ and $\wp$,
and can be formulated in a multiple-conclusion or in a sequent calculus
with term assignments [or in a multiple-conclusions natural deduction system]
and a restriction on the $\limp$ Introduction rule.
Then there are classical proof nets and assignments as in $(i)$, $(ii)$ and
$(iii)$ that do not correspond to a sequent derivation in FILL, due to the
restrictions on the $\limp$ Introduction rule. As in the case of the purely
implicational fragment of ILL, the oriented proof nets corresponding to
a correct derivation may essentially use the constants $\bot$ and $\bf 1$
and the definition of $A^{\bot}$ as $A \limp \bot$.
\bigskip
\centerline{\bf Intuitionistic and Classical Multiplicative Linear Logic.}
\bigskip
Consider the well-known sequent calculus for intuitionistic linear logic ILL;
the corresponding natural deduction system (using sequent notation),
has assumptions $$ A \vdash A $$ and rules
$$\vbox{\halign{\hfil#&#&\qquad#&#&#\hfil\cr
&$\limp$ introduction:\hfil${\displaystyle\strut{\strut\Gamma, A \vdash B}\over{\displaystyle\strut\Gamma\vdash A \limp B}}$\hfil&%
&$\limp$ elimination:\hfil${\displaystyle\strut{\strut\Gamma \vdash A\qquad\Pi \vdash A \limp B}\over{\displaystyle\strut\Gamma, \Pi \vdash B}}$\hfil&\cr
&\strut&\cr
&$\otimes$ introduction:\hfil${\displaystyle\strut{\strut\Gamma \vdash A\qquad\Pi \vdash B}\over{\displaystyle\strut\Gamma, \Pi \vdash A\otimes B}}$\hfil&%
&$\otimes$ elimination:\hfil${\displaystyle\strut{\strut\Delta \vdash A \otimes B\qquad\Gamma, A, B \vdash C}\over{\displaystyle\strut\Delta, \Gamma \vdash C}}$\hfil&\cr
}}$$
\bigskip
Let $R$ be a proof net with conclusions $A_1$,$\ldots$,$A_k$,
for classical multiplicative linear logic (CMLL).
A {\it Danos-Regnier-switch} for a {\it par} link is a choice of one premise.
A proof net $R$ together with a switching $S$ determines
a {\it Danos-Regnier-graph} $S(R)$ in a well known manner --
[ $S(R)$ has formula-occurrences as vertices; it has edges
corresponding to each axiom and cut, two edges for each
{\it times} link (linking each premise to the conclusion)
and one edge for each {\it par} link, corresponding to the switch.]
A proof structure $R$ is a proof-net iff for each switching $S$,
the D-R-graph $S(R)$ is an unordered tree (acyclic and connected graph).
We map $S(R)$ into a derivation in the system of Natural Deduction for
intuitionistic multiplicative linear logic (IMLL) with linear implication
$\limp$ and times $\otimes$.
Consider a map $v: R \rightarrow \{O,I\}$ decorating a proof
with input-output marks satisfying the following restrictions:
$$\vbox{\halign{\hfil#&#&#&#&#&#\hfil\cr
\hfil axiom:&\hfil$\overline{O\quad I}$\hfil&\hfil or \hfil&\hfil$\overline{I\quad O}$&\cr
&\strut&\cr
\hfil cut: &\hfil$\underline{O\quad I}$\hfil&\hfil or \hfil&\hfil$\underline{I\quad O}$&\cr
&\strut&\cr
\hfil times:&(1)\hfil$\displaystyle{\strut{O\quad I}\over I}$\hfil&\qquad%
(2)\hfil$\displaystyle{\strut{I\quad O}\over I}$\hfil&\qquad%
(3)\hfil$\displaystyle{\strut{O\quad O}\over O}$\hfil&\cr
&\strut&\cr
\hfil par:&(4)\hfil$\displaystyle{\strut{O\quad I}\over O}$\hfil&\qquad%
(5)\hfil$\displaystyle{\strut{I\quad O}\over O}$\hfil&\qquad%
(6)\hfil$\displaystyle{\strut{I\quad I}\over I}$\hfil&\cr
}}$$\noindent
($v(A)$ = I or O is to be interpreted as ``$A$ belongs
to the elimination or introduction part, respectively, of a branch
in a natural deduction derivation'')
Call such a map an {\it orientation}. An orientation of the proof net
is {\it natural} if it assigns $O$ to exactly one conclusion of $R$.
Notice that a D-R-switching on the net R can be extended to include
a choice of exactly one conclusion $A_i$ (take the net $R'$ with
conclusion $A_1 \wp \ldots \wp A_k$.
\smallskip\noindent
{\bf Lemma:} (i) {\it If $R$ is a proof net, then any D-R-switching $S$
determines an orientation $v : R \rightarrow \{O,I\}$
and every orientation is natural.}
\smallskip\noindent
(ii) {\it Every orientation $v : R \rightarrow \{O,I\}$ on
a proof structure $R$ corresponds to a set of D-R-switchings for $R$.}
\smallskip\noindent
(iii) {\it Every orientation $v : R \rightarrow \{O,I\}$ on
a proof structure $R$ with conclusions $\Gamma$ yields a translation
$\Gamma^*$ into the language of intuitionistic linear logic.}
\smallskip\noindent
{\bf Theorem:} (i)
{\it If $R$ is a proof net with conclusions $A_1$,$\ldots$,$A_{k+1}$,
then every D-R switching determines a derivation of
$A'_1 \otimes\ldots\otimes A'_k \limp A'_{k+1}$ in intuitionistic
multiplicative linear logic, where $A_1 \wp \ldots \wp A_{k+1}$
and $A'_1 \otimes\ldots\otimes A'_k \limp A'_{k+1}$
are equivalent in classical linear logic.}
(ii) {\it Let $R$ be a proof structure with conclusion $\Gamma$.
If we have a derivation of $\Gamma^*$ in intuitionistic linear logic
and $\Gamma^*$ results from an orientation $v: R \rightarrow \{O, I\}$
then $R$ is a proof net.}
\smallskip\noindent
{\bf Proof of the Lemma.} (i) If $A$ is the selected conclusion, let $v(A) = O.$
Proceeding from $A$, follow the D-R-tree and let $v(X) = O$ when $X$
is reached upwards; let $v(X) = I$ otherwise. Thus
\smallskip
\item{(i)} proceeding upwards, across a {\it times} link: give value O
to both premises, as in (3) and continue upwards from both premises;
\item{\quad} proceeding upwards, across a {\it par} link: give value O
to the premise connected by the switch, as in (4) or (5);
\item{(ii)} proceeding to the side, across an axiom or cut links:
change the value from O to I [from I to O] and direction;
\item{(iii)} proceeding downwards, across a {\it times} link: give value I
to the conclusion and continue downwards from it; also
give O to the other premise and continue upwards from it, as in (1) or (2);
\item{\quad} proceeding downwards across a {\it par} link: give I to
the conclusion, if there is edge, as in (6).
\smallskip\noindent
The procedure yields a well defined orientation $v: R \rightarrow \{O, I\}$,
since the D-R tree is acyclic and connected,
hence every node is reached exactly once.
Such a $v$ is also natural: indeed the above procedure starts
with an $A$ such that $v(A) = O$ and each subroutine stops only at
a conclusion of the net or at a premise of {\it par} link,
in all cases proceeding downwards, i.e., after assigning value I.
\smallskip
The orientation $v$ assigns value O to some conclusion $A$ by definition.
Finally, we must show that if $v$ is {\it any} orientation
of a proof net $R$, then it assigns value O to some conclusion of $R$.
Given a conclusion $A$ of $R$ with $v(A) = I$,
we perform the following search in the D-R-tree $S(R)$,
starting from (the vertex corresponding to) $A$:
\smallskip
\item{(*)} proceeding upwards, choose formulas with value I
(there always is one; i.e., we go from I to I, in case of a {\it times} link
(1) or (2) by choosing one branch, and in case of a {\it par} link (6)
by following the switch);
\smallskip
\item{(**)} proceeding downwards, choose formulas with value O;
this is possible in cases (3), (4) or (5).
If from a premise with value O we reach a conclusion with value I,
then the link can be only be a {\it times} link, cases (1) and (2);
since the other premise has value I, we can continue the search upwards
as in (*).
Finally, if we reach a conclusion of $R$, then the search terminates.
\smallskip
Since $R$ is finite and in $S(R)$ there is no cycle, the search terminates;
it can only terminate downwards, giving value O to a conclusion.
\smallskip
(ii) Given a natural orientation of $R$, we obtain a switch for a {\it par}
link by choosing the premise with value O, if the conclusion has value O,
and by making an arbitrary choice, otherwise.
\smallskip
(iii) The translation $(\quad)^*$ of the conclusions of $R$
is defined inductively as follows, assuming that axioms contain
atoms and negations of atoms only.
\noindent
$\bullet$
We translate both occurrences in $\overline{p^{\bot}\quad p}$ to $p$ or
to $p^{\bot}$, depending on whether $v(p) = O$ or $v(p^{\bot}) = O$.
\noindent
$\bullet$
If $v(A) = O = v(B)$, then $v(A \otimes B) = O$;
given $A^*$ and $B^*$, let $(A \otimes B)^* = A^* \otimes B^*$.
\noindent
$\bullet$
If $v(A) = I = v(B)$, then $v(A \wp B) = I$;
given $(A^{\bot})^*$ and $(B^{\bot})^*$,
let $(A \wp B)^* = (A^{\bot})^* \otimes (B^{\bot})^*$.
\noindent
$\bullet$
If $v(A) = I$ and $v(B) = O$, then $v(A \wp B) = O$, $v(A \otimes B) = I$;
given $(A^{\bot})^*$ and $B^*$, let $(A \wp B)^* = (A^{\bot})^* \limp B^*$
and $(A \otimes B)^* = B^* \limp (A^{\bot})^*$.
\noindent
$\bullet$
Dually, if $v(A) = O$ and $v(B) = I$. \bull
\smallskip\noindent
{\bf Proof of the Theorem:}
{\it times} links in cases (1) (2) correspond to $\limp$ elimination;
a {\it times} link in case (3) corresponds to $\otimes$ introduction;
{\it par} links in cases (4) (5) correspond to $\limp$ introduction;
a {\it par} link in case (6) corresponds to $\otimes$ elimination.
% E.g.:(1) A B A' A-oB'
% ----- becomes --------, where in CLL, A' equiv A, B' equiv -B.
% A x B B'
%
% [A']
% :
% (5) A B B'
% ------- becomes --------, where in CLL, A' equiv -A, B' equiv B.
% A par B A'-o B' C
%
% [A'][B']
% :
% (6) A B A' x B' C
% ------- becomes -------------, where in CLL, A' equiv -A,
% A par B C B' equiv -B.
Following a D-R-tree, it is easy to construct a natural deduction
derivation step-by-step in cases of links (1), (2) and (3).
But $\limp$-introductions and $\otimes$-eliminations, corresponding to
links (4) (5) and (6), have global conditions. To show that these can be
satisfied, given a link with conclusion $A \wp B$ and
notice that the natural orientation of $R$ induces an orientation of
$k(A \wp B)$, the smallest subnet of $R$ containing $k(A \wp B)$
as a conclusion, which is natural by the Lemma.
Thus exactly one door of $k(A \wp B)$ is given value O.
It follows that the value O is given to $A$ or $B$
in cases (4), (5) or to some $C$ in $k(A \wp B)$ in case (6).
Arguing by induction on the number of links, we obtain a derivation
corresponding to $k(A \wp B) \setminus \{A \wp B\}$; finally,
we conclude by applying $\limp$ introduction or $\otimes$ elimination.
Let $R$ be a proof net with conclusions $A_1$, $\ldots$, $A_{k+1}$;
given a D-R-switching, we obtain a natural deduction derivation of
$A'_{k+1}$ from $A'_1$, $\ldots$, $A'_k$
[or a sequent derivation in IMLL of $A'_1\ldots A'_k \vdash A'_{k+1}$].
It is clear from the construction that
$A_1\wp \ldots \wp A_{k+1}$ is equivalent in CMLL to
$A'_1\otimes \ldots \otimes A'_k \limp A'_k$.
Conversely, given a proof structure $R$ with conclusions
$A_1$, $\ldots$, $A_{k+1}$, let $\cal D$ be a sequent derivation in IMLL of
$A'_1\ldots A'_k \vdash A'_{k+1}$, where
$A'_1\ldots A'_k \vdash A'_{k+1}$ comes from an orientation of $R$
(hence $A_1\wp \ldots \wp A_{k+1}$ is equivalent to
$A'_1\otimes \ldots \otimes A'_k \limp A'_k$).
Part (ii) of the theorem can be proved by showing that
$\cal D$ corresponds to an inductive generation of $R$ as a proof {\it net}.
\bull
\bigskip
The system of Full Intuitionistic Linear Logic FILL
(Hyland and de Paiva, {\it Full Intuitionistic Linear Logic}, extended abstract)
has the language with ${\bot}$, $\otimes$, $\limp$ and $\wp$
and is formalized in a sequent calculus [or multiple-conclusion
natural deduction system] with term assignments.
In a sequent $x_1:C_1,\ldots, x_m:C_m \vdash t_1:D_1,\ldots, t_n:D_n$
a strong notion of dependency is given by the term calculus:
$D_i$ depends in the strong sense from $C_j$
just in case $x_j$ occurs in $t_i$.
The rule $\limp$-R below is then subjected to the restriction
that no formula in $\Delta$ depends in the strong sense from $A$,
i.e., that $x$ does not occur in $\tilde{u}$
$$
\limp-R:{{\Gamma, x:A \vdash t:B, \tilde{u}:\Delta}\over{\Gamma\vdash \lambda x.t:A \limp B, \tilde{u}:\Delta}}
$$
[Of course, the notion of strong dependency could be defined
directly by induction on the derivation tree.]
Given a proof net $R$ for CMLL, consider
orientations of proof nets taking also the following values:
$$\hbox{par: } {{O\quad O}\over O}\qquad\hbox{times: } {{I\quad I}\over I}\qquad$$
which are associated with the right and left [introduction and elimination] rules for {\it par}.
An extension of the above procedure yields a sequent derivation in a two-sided
formalization of MCLL [a multiple conclusion natural deduction derivation].
However, such a derivation may be incorrect in FILL, because the restriction
on $\limp$-R may be violated. E.g., given the obvious cut-free proof net with conclusions
$$B\wp(B^{\perp} \otimes A^{\perp}), A,$$ the orientation assigning O to both conclusions
corresponds to $\vdash (B \wp A) \limp B, A$, which is unprovable in FILL.
\end
$$\vbox{\halign{\hfil#&#&\quad#&#&#\hfil\cr
&$\limp$ intro:\hfil${\displaystyle\strut{\strut\Gamma, A \vdash B, \Delta}\over{\displaystyle\strut\Gamma\vdash A \limp B, \Delta}}$\hfil&%
&$\limp$ elim:\hfil${\displaystyle\strut{\strut\Gamma \vdash A, \Delta \qquad\Pi \vdash A \limp B, \Theta}\over{\displaystyle\strut\Gamma, \Pi \vdash B, \Delta, \Theta}}$\hfil&\cr
&\strut&\cr
&$\otimes$ intro:\hfil${\displaystyle\strut{\strut\Gamma \vdash A, \Delta \qquad\Pi \vdash B, \Theta}\over{\displaystyle\strut\Gamma, \Pi \vdash A\otimes B, \Delta, \Theta}}$\hfil&%
&$\otimes$ elim:\hfil${\displaystyle\strut{\strut\Gamma \vdash A \otimes B\qquad\Delta, A, B \vdash \Xi}\over{\displaystyle\strut\Delta, \Gamma \vdash \Theta, \Xi}}$\hfil&\cr
&$\wp$ intro:\hfil${\displaystyle{\strut\Gamma \vdash A, B, \Delta}\over{\displaystyle\strut\Gamma \vdash A \wp B, \Delta}}$\hfil&%
&$\wp$ elim:\hfil${\displaystyle{\strut\Gamma \vdash \Delta, A \wp B\qquad A, \Pi \vdash \Theta \qquad\Lambda, B \vdash \Xi}\over\displaystyle{\strut\Gamma, \Pi, \Lambda \vdash \Delta, \Theta, \Xi}}$\hfil\cr
}}$$
\smallskip
\end
It is defined inductively as follows:
\smallskip\noindent
(1) If $A$ is an assumption, then $f(A) = \{A\}$;
\smallskip\noindent
(2) if $A$ and $B$ are the premises of an $\otimes$- or $\wp$-introduction,
then for the conclusion $A\otimes B$ or $A \wp B$ we have $f(A\otimes B) = f(A) \cup f(B)$ or
$f(A\wp B) = f(A) \cup f(B)$; if $A$, $A\limp B$ are the premises of
a $\limp$-elimination, then for the conclusion $B$ we have $f(B) = f(A) \cup f(A \limp B)$;
\smallskip\noindent
(3) if $B$ is the premise of a $\limp$ introduction with conclusion $A \limp B$
then $f(A \limp B) = f(B) \setminus \{A\}$;
\smallskip\noindent
(4) If $A$, $B$ are dependencies discharged in virtue of an $\otimes$-elimination $\cal R$,
and $A$ or $B$ belong to $f(C)$ in the premise of $\cal R$, then in the conclusion of $\cal R$
we have $f(C) =
the premise $B$
of a $\limp$-introduction relevantly depends on $C$ and $C \neq A$,
then so does the conclusion $A \limp B$.
Here the rule of $\limp$ introduction holds with the restriction that
no
Gamma |- A, B, Delta Gamma, A |- Delta Pi, B |- Theta
intro:----------------------- elim: -----------------------------------
Gamma |- A par B, Delta Gamma, Pi, A par B |- Delta, Theta
The rule of intro for -o has the restriction that no occurrence in Delta
depends on A.]