[Prev][Next][Index][Thread]
Undecidability of second order linear logic without exponentials
A new preprint is now available by ftp anonymous on lmd.univ-mrs.fr in the
directory /pub/lafont.
undecid.ps.Z
Undecidability of second order linear logic without exponentials (7 pages)
Recently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment
of second order intuitionistic linear logic is undecidable, using a simple
encoding of second order intuitionistic logic. Here we prove that the
multiplicative-additive fragment of second order (classical) linear logic is
also undecidable. For this, we use an encoding of two counter machines
originally due to Kanovich together with an argument of phase semantics.
I take this opportunity to mention another paper related to linear logic:
proofnets.ps.Z
From Proof-Nets to Interaction Nets (21 pages)
[To appear in the proceedings of the Linear Logic Workshop (Cornell, 1993)]
If we consider the interpretation of proofs as programs, say in intuitionistic
logic, the question of equality between proofs becomes crucial: The syntax
introduces meaningless distinctions whereas the (denotational) semantics makes
excessive identifications. This question does not have a simple answer in
general, but it leads to the notion of proof-net, which is one of the main
novelties of linear logic.
The notion of interaction net comes from an attempt to implement the reduction
of these proof-nets. It happens to be a simple model of parallel computation,
and so it can be presented independently of linear logic. However, we think
that it is also useful to relate the exact origin of interaction nets,
especially for readers with some knowledge in linear logic. We take this
opportunity to give a survey of the theory of proof-nets, including a new proof
of the sequentialization theorem.