Cancellative LL

To: linear@cs.Stanford.EDU
Subject: Cancellative LL
From: Masaru Shirahata <sirahata@jaist.ac.jp>
Date: Fri, 23 Jun 95 09:48:49 JST
Approved: types@dcs.gla.ac.uk



This posting is related to Jean-Marc's following question

> Long ago, I ran into a thing called "cancellative Linear Logic" or 
> something like that, where the operators "par" and "times" are blurred. 
> Can anyone give me pointers about that. Thanks.
>
>	Jean-Marc

I am not sure exactly what cancellative linear logic is, but I am 
familiar with a category theoretic counterpart of LL in which "par" 
and "times" are identified. That is compact category, considered by
M. Barr and used by S. Abramsky. One of the motivations to consider this 
category is that one can define "of course" in terms of finite "times" 
and infinitary "with." Recently, I formulated a proof theoretic version
of compact category. Without additives, it behaves fairly well, in the
sense that it allows cut-elimination. With infinitary additives, however,
it turned out that one can derive anything in such a system! Does this 
mean that compact category is not a good category to consider? Or does this
simply mean that provability is not so important in LL? 

Masaru Shirahata