[Prev][Next][Index][Thread]
Non-commutative MLL2 is undecidable
Undecidability of Non-Commutative Second Order Multiplicative
Linear Logic
Max Kanovich
In referring to linear logic fragments,
let N stands for non-commutative versions
(with "\" and "/" being left and right implications, respectively,
and "*" being non-commutative product),
M for multiplicatives,
A for additives,
E for exponentials,
2 for second order quantifiers, and
I for "intuitionistic" version of linear logic fragments.
Lincoln, Scedrov, and Shankar showed the undecidability
of IMLL2 and IMALL2 by embedding of LJ2 (announced in this forum,
to appear in LICS '95).
Lafont has proved the undecidability of MALL2 (announced in this
forum, to appear in the Journal of Symbolic Logic).
Recently, Lafont and Scedrov proved that MLL2 is undecidable
(announced in this forum).
As for non-commutative linear logic,
Emms shows embedding of LJ2 into N-IMLL2 as well,
Kanovich proved the undecidability of Lambek calculus enriched by
the exponential !, and thereby the undecidability of N-MELL.
Here we prove that classical N-MLL2 is also undecidable.
We follow the pattern developed in the Lafont's paper and refined in
the subsequent Lafont and Scedrov's paper.
1. The 'self-reproductive' work of the absent exponential ! is
provided with the following formula
R = forall C,A,T ( (C * #C * #A * T * A)/(#C * #A * T) )
where #B = ((1/B) * B).
In addition to that, we use the following restricted weakening:
Q = forall C,A ( (C * #C * #A)\1 )
2. We simulate Minsky machines with two counters x and y in the
following way.
Any configuration of a given Minsky machine M
(l_i,a,b)
is represented by a 'string' of the form
b * p^a * l_i * q^b * e
(where literals b and e are the end 'markers').
An instruction of the form
l_i: x:=x+1; goto l_j;
is axiomatized by:
forall A,B ( (b * A * p * l_j * B * e)/(b * A * l_i * B * e)).
A zero-test instruction of the form
l_i: if (x=0) then goto l_k;
is axiomatized by:
forall B ( (b * l_k * B * e)/(b * l_i * B * e)).
etc.
Theorem.
Let A_1, A_2, ..., A_n
be the formulas encoding instructions of M.
Let
Gamma = R, #R, #Q, R, #R, #A_1, R, #R, #A_2, ..., R, #R, #A_n.
The following sentences are equivalent:
1. M can go from an initial configuration (l_1,a,b) to the terminal
configuration (l_0,0,0).
2. A sequent of the form
Gamma, b, p^a, l_1, q^b, e |- (b * l_0 * e)
is derivable in N-IMLL2.
3. The above sequent is derivable in classical N-MLL2.
4. The above sequent is derivable in second order cyclic linear
logic.
Proof.
1 -> 2: By a straightforward induction.
4 -> 1: The faithfulness of our encoding is proved by means of
the Girard's phase semantics adapted to the non-commutative
case.
As a corollary, we get the undecidability of both N-MLL2 and second
order cyclic multiplicative linear logic (and N-IMLL2 as well).
Best regards,
Max Kanovich