[Prev][Next][Index][Thread]
Strong Completeness Theorem for MLL
Date: Thu, 28 May 1992 13:44:38 +0100 (BST)
A preliminary announcement of a result we have recently obtained follows.
A paper is in preparation; as soon as it's ready, it will be made
available by ftp.
The announcement is a latex source file. If anyone has difficulty
decoding this, let us know and we'll send you an unformatted
version.
Samson Abramsky and Radha Jagadeesan
-------------------------------
\documentstyle[11pt]{article}
\newtheorem{theorem}{Theorem}
\newcommand{\entails}{\mbox{$\;\vdash$}}
\newcommand{\tensor}{\mbox{$\otimes$}}
\newcommand{\category}[1]{{\bf #1}}
\newcommand{\mytwotrans}[2]{\mbox{$ \frac{\mbox{$#1$}}{\mbox{$#2$}}$}}
\author{Samson Abramsky and Radha Jagadeesan}
\title{A Strong Completeness Theorem for Multiplicative Linear Logic:\\
Preliminary Announcement}
\begin{document}
\maketitle
\section{Background}
Blass has recently described a Game semantics for Linear Logic in which
formulas are interpreted by games and proofs by winning strategies. This
has good claims to be the most intuitively appealing semantics
for Linear Logic presented so far. However, there is a considerable gap
between Blass' semantics and Linear Logic:
\begin{enumerate}
\item The semantics validates Weakening, so he is actually modelling Affine
logic.
\item Blass characterises validity in his interpretation for the
multiplicative fragment: a formula is game semantically valid if and only
if it is an instance of a binary classical propositional tautology (where
tensor, par, linear negation are read as classical conjunction,
disjunction and negation).
Thus there is a big gap even between provability in Affine logic and validity
in his semantics.
\end{enumerate}
This leaves open the challenge of refining Blass' interpretation to get a
closer fit with Linear Logic while retaining its intuitive appeal.
On the other hand, there is the challenge of obtaining a {\em strong
completeness
theorem}. The usual completeness theorems are stated with respect to
provability; a strong completeness theorem is with respect to proofs.
This is best formulated in terms of a categorical model of the
logic, in which formulas denote objects, and proofs denote
morphisms. One is looking for a model \category{C} such that:
\begin{description}
\item[Completeness: ]
$\category{C}(A,B)$ is non-empty only if $A \entails B$ is provable in the
logic.
\item [Strong Completeness: ]
Any $f: A \rightarrow B$ is the denotation of a proof of $A
\entails B$. One may even ask for there to be a {\em unique} cut-free such
proof.
\end{description}
With strong completeness, one has the tightest possible connection between
syntax and semantics. This idea is related to coherence theorems in
category theory; to full abstraction theorems in programming language
semantics; to studies of parametric polymorphism; and to Girard's
completeness conjecture in his paper ``A new constructive logic: Classical
Logic''.
We now make a first statement in broad terms of our results. We have
refined Blass' game semantics for Linear Logic.
This refinement is not a complication; on the contrary, it makes the
definitions smoother and more symmetric. Then, we prove a Strong
Completeness Theorem for this semantics, with respect to MLL + MIX
(Multiplicative
Linear Logic plus the Mix Rule). Recall that the MIX rule~\cite{Gir87} has
the form
\[ \mytwotrans{\entails \Gamma \; \; \; \; \entails \Delta}{\entails
\Gamma,\Delta} \]
There is a notion of proof net for this logic: one uses the Danos/Regnier
criterion, simply omitting the connectedness part. Thus, a proof
structure will
be a valid proof net for MLL + MIX just if, for every switching, the
corresponding graph is acyclic. This criterion was used by Blute
in his work on coherence theorems, and adapted by Lafont for his work on
interaction nets.
Now, we can state our result in more precise terms.
\begin{theorem}
Every proof in MLL + MIX denotes a uniform, history independent winning
strategy for Player in our game interpretation. Conversely, every
such strategy is the denotation of a unique cut-free proof.
(To be quite precise, to get uniqueness we restrict proofs to only
use atomic instances of Axiom).
\end{theorem}
Of course, we now have to explain uniform, history independent strategies.
Note that a formula in MLL+MIX is built from atomic formulae and the
binary connectives tensor and par. Its denotation will then be a {\em variable
type}. We construe this as a functor over a category of games and
embeddings, in the fashion of domain theoretic semantics of polymorphism.
(In fact, this interpretation of variable types is part of our game
theoretic semantics of polymorphism). An element of variable type, the
denotation of a proof, will then be a family of strategies $\{\sigma_A\}$,
one for each game $A$. The uniformity of this family is expressed by the
condition that it is a natural transformation $\sigma: I \rightarrow F$,
where $I$ is the constant functor valued at the tensor unit.
A history independent strategy is one in which the player's move is a
function only of the last move of the opponent and not of the preceding
history of the play.
Thus such a strategy is induced by a partial function on the set of
moves in the game.
The interpretation of proofs in MLL + MIX by strategies,
when analyzed in terms of these underlying functions on moves,
turns out to be very closely related to the Geometry of Interaction
interpretation.
\appendix
\section{ A few details}
We give some basic definitions of the Game semantics.
A game is a structure $A = (M_A,\lambda_A,P_A,W_A)$, where
\begin{itemize}
\item $M_A$ is the set of moves.
\item $\lambda_A: M_A \rightarrow \{ P,O \}$ is the labelling function to
indicate if a move is by Player or Opponent.
\item $P_A$ is a prefix closed set of finite,
alternately labelled sequences of moves.
This is the set of valid {\em positions} of the game.
\item $W_A$ is the set of infinite plays of the game (infinite
sequences of moves, all of whose finite
prefixes are in $P_A$) that are won by Player.
\end{itemize}
A history independent strategy for player $P$ in $A$ is induced by
a partial function $f$
on moves: thus, at a position $s\cdot a$, with Player to move, he
plays $f(a)$ if defined.
Our plays are always with Opponent to start.
A strategy for Player is {\em winning} if, whatever moves
Opponent makes, the resulting play is {\em either} finite, resulting
in a position with Opponent to play and no valid moves; {\em or}
infinite, resulting in an infinite play in $W_A$.
\subsection{Defining the connectives}
\subsubsection*{Involution}
The dual $A^{\perp}$ is obtained by inverting the labelling function
$\lambda_A$ and complementing the set of wins $W_A$.
\subsubsection*{Tensor}
The game $A \tensor B$ is defined as follows.
\begin{itemize}
\item $M_{A \tensor B} = M_A + M_B$, the disjoint union of the two move
sets.
\item $\lambda_{A \tensor B} = [\lambda_A,\lambda_B]$, the source tupling.
\item $P_{A \tensor B}$ is the set of all alternately labelled finite sequences
of moves such
that:
\begin{enumerate}
\item The restriction to the moves in $M_A$ (resp. $M_B$) is in
$P_A$ (resp. $P_B$)
\item If two successive moves are in different components, ({\em i.e.} one
is in $A$ and the other is in $B$), it is the Opponent who has switched
components.
\end{enumerate}
\item $W_{A \tensor B}$ is the set of infinite plays of the game, such that
the restriction to each component is either finite or is a win for Player
in that component.
\end{itemize}
Some remarks about the comparison with Blass' definitions may be helpful.
In our definition, a game may admit some plays in which Player starts,
some in which Opponent starts.
This is significant when combining games, e.g. with tensor.
The crucial difference between Blass' definition of tensor and ours is with
respect to how the game can {\em start}.
In particular, Blass has a special case when Player is to start in both games.
This special case is at the heart of the pathologies in his semantics.
The reader may like to check that with our definitions neither Weakening,
nor the example discussed on pp. 51--55 of Blass' paper, are valid.
\end{document}