[Prev][Next][Index][Thread]
Linear logic + weakening
To: linear@cs.stanford.edu
Date: Wed, 17 Jun 92 15:37:22 +1200
Dear all,
I gather from reading this list that the term affine logic
has become more or less the standard one to describe the logic obtained by
adding weakening (but not contraction of course) to linear logic. A
question that has occurred to me of late is what sort of logic is obtained
by adding a more restricted form of weakening to linear logic --- in
particular if we add not arbitrary weakening, but the dual to contraction,
which in my ignorance I have called expansion, or "static" weakening. In a
sequent calculus, this rule may be written as (pardon the TeX)
\Gamma, F \vdash \Delta
---------------------------
\Gamma, F, F, \vdash \Delta
and similarly for the right hand side. Have there been any investigations
of such a logic? (or even a name for it?). Any help would be greatly
appreciated, as would any pointers to papers on affine logic.
This question arose out of some work I have been doing on a notion
of Negation as Failure in intuitionistic logic, for which one wants not
arbitrary weakening, but the more restricted form of static weakening (I
refuse to talk about strong and weak weakening! :-). Hence it would be
interesting to see how such a notion differs in the absence of contraction.
Cheers,
James Harland.