[Prev][Next][Index][Thread]
Proof Nets and Roorda's Thesis
Date: Thu, 21 Nov 91 20:27:24 GMT
To: linear@cs.stanford.edu
********************************************************************
****** More on Proof Nets and Dirk Roorda's PhD thesis**************
********************************************************************
With regards to the proof nets reference on Dirk Roorda's PhD thesis,
(pointed out by Vijay Gehlot of Glasgow [vijay@dcs.glasgow.ac.uk]),
perhaps I should elaborate on it. I had written a summary and
a comparsion on Roorda's thesis ( Chapter 6) -"Lambek Calculus and
Modal Logic".
Roorda's thesis is divided into the following chapters :
%------------------Part of my latex summary--------------------
%
% note: \lsembrac and \rsembrac are my marcos for semantic brackets
% \llpar \llto etc. are Paul Taylor's marcos for linear logic
% implicaton and "par" respectively
%
%
\section{An Outline of Roorda's thesis}
The key topic in Roorda's doctoral dissertation \cite{Roo91} is Lambek Calculus \cite{Lam58}. It is a logic on the one hand, and a grammar on the other.
At the same time, the Calculus is strongly related to the current
{\em hot issue\/} in theoretical computing science / logic -- namely
{\em Linear Logic\/} \cite{Gir87}, where it is {\em resource-conscious\/}.
The Lambek Caculus, while is {\em linear\/}, is {\em non-commutative\/} and
{\em negationless\/}
\footnote{It is pointed out to me by Steven Vickers that Intuitionistic Linear Logic is also {\em negationless\/}. }.
Although the emphasis of Roorda's thesis is proof-theoretic, many of the
results are actually obtained semantically.\\
\vspace{11pt}
\par
\noindent
The emphasis of Lambek Calculus (LC) is on the following main threads:
\begin{enumerate}
\item the LC as a Grammar;
\item correspondence with Curry-Howard Isomorphism and {\em typed\/}
$\lambda$~-~{\em Calculus\/};
\item model of LC as free semi-group, ie.
\begin{itemize}
\item $\lsembrac A \bullet B \rsembrac =
\{ c \; | \; \exists a \in \lsembrac A \rsembrac \;
\exists b \in \lsembrac B \rsembrac \; c = a \cdot b \}$
\item $\lsembrac A \; \backslash \; B \rsembrac =
\{ c \; | \; \forall a \in \lsembrac A \rsembrac \;
a \cdot c \in \lsembrac B \rsembrac \}$
\item $\lsembrac A \; / \; B \rsembrac =
\{ c \; | \; \forall a \in \lsembrac A \rsembrac \;
c \cdot a \in \lsembrac B \rsembrac \}$
\end{itemize}
\end{enumerate}
\vspace{11pt}
\par
\noindent
%
%
%
%---------Outline of each chapters---------------------
%
%
%
In addition, it is divided into the following chapters:
\begin{description}
\item[Chapter 1] {\em Introduction}
\item[Chapter 2] {\em Cut Elimination and Strong Normalisation.\/}
He starts the ground work on linear logic side,
and proved it for full first order system of classical linear logic.
The result is needed for proving interpolation property later. Moreover,
strong normalisation is proved via the method of Drag\`alin.
\item[Chapter 3] {\em Proof Net for Lambek Calculus.\/}
The proof nets of linear logic are adapted to the non-commutative, negationless
LC, which also shows that they are useful for automated theorem proving.
\item[Chapter 4] {\em Quantum Graphs.\/}
This gives an alternative representation of proof nets -- quantum graphs.
\item[Chapter 5] {\em Interpolation.\/}
This shows that the interpolation theorem holds for full classical linear
logic, but fails for the ( $\llto$ , $\llpar$ ) fragment
\footnote{Here I use the standard notations in linear logic
literature instead of ( $\llto$ , $+$ ) in Roorda's thesis. }.
Several interesting results are also presented.
\item[Chapter 6] {\em Lambek Calculus and Modal Logic.\/}
This shows an embedding of Lambek Calculus into Modal Logic. Note that
this embedding is different from translating {\em of course\/} ! into
$\Box$ of modal logic necessity. It only translates the modal-free Lambek
connectives. This chapter is the main focus of this summary report.
\end{description}
%
%
%-----------------End of my part of summary-------------------- %
%
%
Note that, he introduces a "Quantum Graphs" as an alterantive to
Proof nets. He also proved cut-elimination and strong normalisation.
My personal research interest is on Lambek Calculus and Modal Logic.
I think Roorda's thesis is very interesting and it deserves more attention
in the "Linear Logic" community.
Reference:
@unpulished(
Cha91b author="H. F. Chau",
title="Notes on Lambek Calculus and Modal Logic -
A Summary on Chapter 6 of Roorda's thesis",
address="Dept. of Computing, Imperial College, London SW7 2BZ",
month="November",
year=1991)
@unpublished(
Gab90, author="D. M. Gabbay",
title="Labelled {D}eductive {S}ystems",
month="June",
year=1991,
note="Draft Version 5, Oxford University Press, forthcoming")
@article(
Lam58, author="Lambek, J.",
title="The mathematics of sentence structure",
journal="American Mathematical Monthly",
volume=65,
pages="154--170",
years=1958)
@phdthesis(
Roo91, author="Roorda, D.",
title="Resource {L}ogics {--} {P}roof {T}heoretical {I}nvestigations",
school="Faculteit van Wiskunde en Informatica, Universiteit van
Amsterdam",
address="Plantage Muidergracht 24, 1018 TV Amsterdam, Nederland",
month="September",
year=1991)
Hilfred (Hiu Fai) CHAU
---------------------------------------------------------------------
Hilfred (Hiu Fai) CHAU email: JANET hfc@doc.ic.ac.uk
Department of Computing UUCP ...ukc!icdoc!hfc
Imperial College of telephone: +44 71 589 5111
Science Technology & Medicine (Room 526,Huxley Building) ext. 4990
University of London home tel. (before 9pm)+44 71 589 5111
180 Queen's Gate ext. 98-251
London SW7 2BZ fax: +44 71 581 8024
UNITED KINGDOM
---------------------------------------------------------------------