[Prev][Next][Index][Thread]
notation
Date: Fri, 20 Dec 91 13:04:50 -0800
X-Organisation: Faculty of Mathematics & Computer Science
University of Amsterdam
Plantage Muidergracht 24
NL-1018 TV Amsterdam
The Netherlands
X-Phone: +31 20 525 5200
X-Telex: 16460 facwn nl
X-Fax: +31 20 525 5101
To: Linear@cs.stanford.edu
Dear colleagues,
There is already a great variety in the notation for the operators of linear
logic, and quite regularly I see new variants cropping up. Below I have
reproduced for your information as a latex file the part in my
"Lectures on linear logic" (which should appear this or the next month
in the Lecture Notes series of the Stanford CSLI) where I motivate my choice of
notation.
But some preliminary remarks are in order.
I am aware of the fact that arguments for and against some particular notation
can become endless, and that the perfect unique choice does not exist. I
certainly DO NOT WANT to start an endless discussion over the linear logic
news net concerning the merits of various notations.
Most people tend to feel emotional attachments or aversions relative to certain
notations (I too!). But you should realize that ventilating these emotions does
not help others in choosing a satisfactory notation. So don't.
Certain proposed notations are motivated as fitting into the category theoretic
tradition. But even there several traditions exist; e.g. some advocate "times"
and "plus" for product and coproduct, but others (e.g. MacLane) prefer "pi" and
"inverted pi" as symbols. So this also determines the choice not uniquely.
One can get used to any notation, after some time. But for beginners a
confusing aspect in Girard's original choice is that dual operations do not
have "similar" symbols. So it seems really desirable to avoid that.
Another example: I would feel perfectly happy with Blute and Seely's choice for
"circledtimes" and "circledplus" for tensor and par, except for the fact that
Girard used "circledplus" already in a different sense
Therefore I give my choice here just for your information, not to start long
debates.
%------cut here-------------------------------------------------
\documentstyle[11pt,leqno,fleqn]{article}
\raggedbottom
\textwidth 15cm
\mathindent 2cm
\textheight 22cm
\evensidemargin 5mm
\oddsidemargin 5mm
\topmargin 0mm
\input{mssymb3}
\title{}
\author{}
\date{}
% LINEAR LOGIC
\def\bo{{\bf 0}}
\def\tr{\top}
\def\ee{{\bf 1}}
\def\li{\multimap}
\def\non{\mbox{$\sim$}}
\def\lie{\:\circ\!\!\!\relbar\!\!\!\hskip .05pt\circ\:}
\def\ps{\sqcup}
\def\en{\sqcap}
\def\pa{+}
\def\fa{\bot}
\def\ma{\star}
% OTHER LOGIC
\def\rar{\rightarrow}
\def\lrar{\leftrightarrow}
\def\Rar{\Rightarrow}
\def\LRar{\Leftrightarrow}
\def\longar{\longrightarrow}
% GREEK
\def\GG{\Gamma}
\def\DD{\Delta}
\def\aa{\alpha}
\def\bb{\beta}
\def\gg{\gamma}
\def\dd{\delta}
% SPECIAL
\def\CLL{{\bf CLL}}
\def\CLLn{\mbox{$\mbox{{\bf CLL}}_{0}$}}
\def\CLLq{\mbox{$\mbox{{\bf CLL}}_{{\rm q}}$}}
\def\CLLe{\mbox{$\mbox{{\bf CLL}}_{{\rm e}}$}}
\def\ILL{{\bf ILL}}
\def\ILLn{\mbox{$\mbox{{\bf ILL}}_{0}$}}
\def\ILLq{\mbox{$\mbox{{\bf ILL}}_{{\rm q}}$}}
\def\ILLe{\mbox{$\mbox{{\bf ILL}}_{{\rm e}}$}}
\def\N{{{\rm I}\!{\rm N}}}
\def\lbrac{\mbox{$[ \! [$}}
\def\rbrac{\mbox{$] \! ]$}}
\def\PA{$\wp$}
%
\begin{document}
\pagestyle{plain}
\subsection*{Remarks on the choice of notation}
In this version of these lectures on linear logic, we have kept Girard's
symbols $\non$, $\forall$, $\exists$, !, ?, $\tr$, $\ee$, and replaced \&,
\PA, $\otimes$, $\oplus$ by $\en$, $\pa$, $\ma$, $\ps$ respectively, and
interchanged $\fa$ and $\bo$. Instead of $A^{\fa}$ we write $\non A$. Thus we
have achieved that the pairs $\en$, $\ps$; $\pa$, $\ma$; !, ?; $\forall$,
$\exists$; $\bo$, $\ee$; $\fa$, $\tr$ are de Morgan duals, where each pair
consists of ``similar'' symbols. With the ordering $\leq$ on the set of
equivalence classes ${\cal F}$ of formulas modulo linear equivalence, i.e.
%
\begin{displaymath}
[A] = [B] \mbox{ {\rm iff} }\vdash\, \Rar A \li B \mbox{ {\rm and} }\vdash\,
\Rar B \li A
\end{displaymath}
%
\noindent and
%
\begin{displaymath}
[A] \leq [B] \mbox{ {\rm iff} } \vdash\, \Rar A \li B,\mbox{ {\rm or
equivalently} } \vdash A \Rar B
\end{displaymath}
%
\noindent we obtain a lattice with $\tr$, $\fa$, $\ps$,
$\en$ corresponding to top,
bottom, join and meet respectively.
We have chosen $\ps, \en$ instead of $\vee, \wedge$, since on the one hand the
shape of $\ps, \en$ is reminiscent of $\vee, \wedge$ (and so $\ps$ suggests
join and disjunction, and $\en$ suggests meet and conjunction), and on the other
hand we do not want to identify $\ps$ with disjunction and $\en$ with
conjunction in classical or intuitionistic logic, since in linear logic $\vee,
\wedge$ have in fact two analogues each ( a multiplicative and an additive
one). An additional advantage (to me) is that the shape of $\ps, \en$ is also
reminiscent of $\coprod, \prod$, widely used for categorical coproducts and
products respectively. We thought it better to use $\ma$ instead of $\otimes$,
since $\otimes$ inevitably evokes $\oplus$ of Girard's notation, a source of
confusion we wished to avoid.
$({\cal F},\ma,\ee)$ is a commutative monoid with unit; in classical linear
logic, $({\cal F},\pa,\bo)$ is a dual commutative monoid. Since $\ma$, $\pa$
suggest ``times'' and ``plus'', it is only natural to use $\ee$ and $\bo$ for
the respective neutral elements.
Girard's choice of notation was motivated differently. Since $\ma$ behaves as a
tensor product in algebra, he choose $\otimes$; $\ps$ was reminiscent of direct
sum, hence the choice of $\oplus$. This led to a familiar-looking distributive
law:
%
\[ A \otimes (B \oplus C) \mbox{ is equivalent to } (A \otimes B)
\oplus (A \otimes C) \]
%
which is thus easily memorized. This choice also dictated the use of $\ee$ and
$\bo$ as the respective neutral elements. On the other hand, the fact that
$\otimes$ and $\oplus$ are not dual to each other is confusing, as is
the fact that not $\tr$, $\fa$ but $\tr$, $\bo$, and not $\ee$, $\bo$, but
$\ee$, $\fa$ are duals when one uses Girard's notation.
There is little confusion to be expected from our change of \&, \PA,
$\otimes$, $\oplus$ into $\en$, $\pa$, $\ma$, $\ps$, since the symbols are
disjoint. On the other hand, the interchange between $\fa$ and $\bo$ may cause
confusion when using this text next to papers in Girard's notation.
A completely new set of four symbols for the neutral elements here designated
by $\tr, \fa, \ee, \bo$ could avoid this confusion, but we were unable to find
an alternative which is mnemonically convenient and fits the other symbols as
well as the present set. The best alternative seems to be one proposed by K.
Do\v{s}en, namely to use ${\bf T}, {\bf F}, {\bf t}, {\bf f}$ for the present
$\tr, \fa, \ee, \bo$ respectively. Ordinary ``true'' splits into additive {\bf
T} and multiplicative {\bf t}; ``false'' similarly splits into {\bf F} and {\bf
f}. (One might follow Do\v{s}en's proposal in discussions with someone
accustomed to Girard's notation, so as to avoid confusion.)
Since already quite a number of papers and
reports have been written using Girard's original notation, we propose a change
of notation with some hesitation, though it seems to us there are some obvious
advantages, especially to someone new to the subject. Of course, one can get
used to almost any notation provided it is not too cumbersome, and unambiguous!
%
\end{document}