[Prev][Next][Index][Thread]
Linear logic semantics (latex file}
To: linear@cs.stanford.edu
Date: Thu, 20 Feb 92 14:25:33 -0500
\documentstyle[]{article}
\title{Notes on the semantics of linear logic}
\author{Jon Barwise}
\date{Feb 1992}
\begin{document}
I recently posted a note to linear@cs.stanford.edu asking for help in
trying to understand linear logic from a semantic point of view. I
have received quite a few direct responses to this message, plus {\it
lots} of messages asking for me to share my findings. I had hoped to
go through all this and write up a summary. However, there is just too
much stuff and time is too short for me to expect to finish this in a
reasonable amount of times. So I have decided to do a quick and dirty
job, hoping it will help others in my predicament.
I have gone through the replies and culled out the recommended reading
in one list. In a second list, I have put extracted other kinds of
comments about the topic. I have tried not to divulge the identity of
the senders, since (a) these were clearly not intended for public
distribution, and (b) some of the comments are rather outspoken. I
hope noone is offended by this form of distribution. Anyone who wants
to take credit or blame for any of the comments can do so on their
own. In any case, none of the remarks below are due to me.
\subsection*{Recommended readings}
Here are the readings. The comments are from the senders.
\begin{enumerate}
\item Samson Abramsky, ``Computational Interpretations of Linear
Logic" It can be ftp'd from: theory.doc.ic.ac.uk
(146.169.2.37) /theory/papers/Abramsky/cill.dvi.Z
\item Samson Abramsky, ``New Foundations for the Geometry of
Interaction'', with Radha Jagadeesan. This is a very
interesting paper.
\item Arnon Avron, ``Relevance and paraconsistency- a new approach",
JSL vol. 55 (1990), pp. 707-732
\item Andreas Blass, ``A game-theoretical semantics for affine linear
logic.'' He is at the University of Michigan mathematics
department. This is an interesting and intuitive semantics, even
if it goes get a little more than linear logic.
\item \ldots{} Deep work, based on information flow through
networks, the work of Girard's students Danos and Regnier is great. A
version is in the LICS 91 proceedings (a paper by Regnier and
Malacria).
\item A rather idiosynchratic but deep paper is girard's paper in
Contemp. Math. (Proc. Boulder Conference in Categorical Logic), 1987,
edited by J.Gray and A. Scedrov
\item Mati-Oliet and Meseguer, ``From Petri Nets to Linear Logic through
Categories: a Survey"
\item From: Remo.Pareschi@ecrc.de:
\begin{quote} If you are interested, and could provide me with your
exact address, I can send you a few papers, written together with my
colleague J-M Andreoli, where we show how to use Linear Logic to model
open information systems. We exploit connectives like ``par" to
account for intra-action inside a complex agent, and ``with" to
account for inter-actions among agents. In one of the papers,
``Communication as Fair Distribution of Knowledge", there is also an
use of the Phase Semantics which is, to us, rather intuitive.
\end{quote}
\item Uday Reddy (Univ. of Illinois) has a couple of recent papers
giving an interpretation in terms of ``accepters'' etc. from standard
programming languages.
\item A series by Phil Wadler (Glasgow) with amusing titles. If
you need them, you can contact him at wadler@dcs.gla.ac.uk.
``Linear types can change the world,'' ``Is there a use for linear
logic?'' and ``There's no substitute for linear logic.''
\end{enumerate}
\subsection*{Other comments}
Now follow the other sorts of commentary on the state of affairs
regarding the semantics of linear logic.
\begin{itemize}
\item I think there is a good explanation of Linear Logic in terms
of ``flow of information'' - but it is very important that this be
interpreted dynamically rather than statically (so that we should
understand the content of a proposition in terms of the processes
which realize it, rather than its truth-conditions). In some sense
that's the whole point, and why the subject is of such interest to
Computer Science.
The interpretation of Linear Logic which comes closest to capturing
this explanation is the ``Geometry of interaction''. Unfortunately,
Girard's papers on this topic are probably his most obscure\ldots{}
\item I'd like to try to answer your question. It would help me to
know what you count as an answer when ``linear" is replaced with
"intuitionistic". Do you prefer to understand intuitionistic logic
via the lambda calculus? Heyting algebras? S4? Kripke structures?
[From Barwise: I think of it intuitively in terms of incomplete
totalities. I think Kripke structures do the best job of modeling
this. I can also think of it in terms of a logic of proofs and
constructions, in which case I prefer the realizability approaches.]
At least for the first two answers there are corresponding answers
for linear logic: various linear lambda calculi and structures such
as quantales. But I would expect your answer to be ``Kripke structures"
and then I am afraid that I am at a loss (though with that extra bit
of prompting someone on the mailing list might be able to help).
As for myself, I looked at linear logic in various ways over time,
but many aspects began to make sense only when I understood better
the proofs and the corresponding lambda calculi. I am disappointed
that truth has little to do here so far. Maybe that is what Girard
meant when he said, with the Chinese leader, that what matters in
the cat is not the color but that it catches mice.
\item My own suspicion is that linear logic {\it looks} like it might
have some deep semantic or information-theoretic foundation waiting to
be served up for it (like modal logic just before Kripke semantics);
but that this appearance is illusory. I think rather that the
structural changes to the Gentzen sequent calculus have been made only
with an eye to reducing the complexity of proof-search (the name for
the system being a dead give-away). But I'm wiling to be proved
wrong. Anyway, what your note draws attention to is the pressing need
for an authoritative and clear intuitive explanation to a wider
public, from a linear logic guru, about what exactly the aims of
linear logic are, and how one can judge whether they are being
achieved \ldots{} I say all this even from the perspective, different
>from your own semantic one, of one who believes that a satisfactory
{\it meaning} theory for logical operators can be given entirely in
terms of rules of inference.
\item Jon, did anyone respond with an ``intuitive" semantics for LL?
According to Girard in the back of his paper, he mentions about where
LL came from. In his words, the semantics did come first. Now, if you
are requiring a model with certain features, aren't you begging the
question somewhat?
My own view is that LL will not be confined within any information oriented
model. The reason being that the semantics we know about aren't informationally
driven in the classical intuitionist sense. Instead, it has more of a
communication feel to it \ldots{}
\item I am also dissatisfied with the semantic state of affairs of linear
logic. But, I guess people are too excited to think things through.
I don't know where you are coming from, i.e., what you believe in and
what you don't. So, I will be brief. Let me know if you need any
elaboration.
While classical (Tarskian?) notion is ``A is true", in passing to
intuitionistic logic, we have ``p is a proof of A". So, the semantics
of A is the set (or whatever) of its of proofs. I found Prawitz's
papers ``Ideas and results in proof theory" and ``The challenge of
intuitionsitc logic" particularly illuminating in understanding this
point of view. However, what is called a proof is not a syntactic
object, but some semantic notion of which the syntactic proof is a
representation. In this respect, the terms ``evidence" and
"construction" are better than ``proof".
Correspondingly, the linear logic notion seems to be
\begin{center}
p is a proof of A in the context of B1,...,Bn
\end{center}
Whether this can be reduced to the simpler notion ``p is a proof of A",
I am not quite sure. As far as I can tell, it is not known. (In the
intuitionistic case, at least the introduction rules are not
contextual. But, things seem more complicated in linear logic).
Proof nets are the best we have for now.
Next, there are the questions of what is a function, what is a
parallelization etc? Coherent spaces are the best answer we have at
present. It will probably take a very long time to resolve these
questions, given that we don't yet have satisfactory answers for even
system F.
In any case, linear logic is a proof theorists' logic, i.e., for
people who believe that the deepest symmetries of logic are in its
proofs. So, even if we don't quite know what proofs are, we are glad
enough to find the symmetries.
I should say I am reasonably happy with proof nets and coherent
spaces, given that linear logic is still too recent. What I find hard
to swallow are all these other models (particularly for noncommutative
linear logic) which don't even begin to talk about proofs.
\item \ldots{} although unlike you, for me proof-theory comes first,
I agree that something crucial is missing if a logical system has no
intuitive (and concrete) semantics\ldots{}
I am much more skeptic than you about Linear Logic. It MIGHT, of
course turn out to be useful/important. There is also, surely, a lot
of activity concerning it (I contributed to it myself). But it can be
much ado about (almost) nothing. So far there are a lot of promises,
but they are still only promises. Time will tell if this is not just a
matter of fashion. I hope it is not, but I suspect it is.
\item Your circular about inear logic has just reached me. I have
been asking the linear people \ldots{} the same question for some
years now, and have never got a satisfactory answer. This is all the
more irritating because (there is the temptation to believe that)
something with such an elegant proof theory must mean {\it something}.
Presumably you know Scedrov's intro? What we need is someone with a
good old-fashioned philosophical training in the use-mention
distinction to sort this out: (I think the right question to start
with is ``what are the entities that are being introduced and
cancelled? They sure as hell aren't propositions")
\end{itemize}
\end{document}