[Prev][Next][Index][Thread]
paper on finite phase semantics
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
My paper "The finite model property for various fragments of linear logic" (6
pages) is available by ftp anonymous on lmd.univ-mrs.fr (pub/lafont/model.ps.Z
& pub/lafont/model.dvi.Z).
I prove that the finite phase semantics is complete for MALL and LLW (affine
logic), but not for MELL. In particular, I get a new proof of the decidability
of LLW [Kop95]. The argument works also for the noncommutative versions of
MALL.
Yves Lafont
P.S. In this paper, I use the following semantics of exponentials:
An "enriched phase space" is a phase space M endowed with a submonoid K of
J(M) = {x in {1}**; x in {x^2}**}.
If X is a fact, then ?X = (X* /\ K)* and !X = (X /\ K)**.
[* means "orthogonal"; ^2 means "square"; /\ means "intersection"]
If K = {x in {1}**; x = x^2}, one recovers Girard's phase semantics [Gir95]
as a special case. This generalization allows to define quotients with good
properties.
[Gir95] J.-Y. Girard. Linear logic : its syntax and semantics. In Advances in
Linear Logic (J.-Y. Girard, Y. Lafont & L. Regnier, editors), London
Mathematical Society Lecture Note Series 222, 1-42, Cambridge University Press.
1995.
[Kop95] A. P. Kopylov. Propositional linear logic with weakening is decidable.
In Proc. 10th Annual IEEE Symposium on Logic in Computer Science, San Diego,
California, IEEE Computer Society Press. 1995.