[Prev][Next][Index][Thread]
MLLW2 is undecidable
Second order Linear Affine Logic is Undecidable.
Alexei Kopylov
In referring to linear logic fragments,
N stands for non-commutative versions
(with -o and o- being left and right implications, respectively,
and "*" being non-commutative product),
M for multiplicative fragment,
A for additive fragment,
2 for second order quantifiers, and
I for "intuitionistic" version of linear logic fragments,
W for Linear Logic with the weakening rule (called Linear Affine Logic).
Lincoln, Scedrov, and Shankar showed the undecidability of IMLL2 and IMALL2
by embedding of LJ2 (announced in this forum, 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).
Emms shows embedding of LJ2 into N-IMLL2 as well.
Kanovich demonstrated the undecidability of N-MLL2 and second order
Lambek Calculus (LC2). (Announced in this forum).
Here we prove that MLLW2 is also undecidable. The main ideas of the proof is
similar to ideas in Lafont and Scedrov's paper. Namely, we encode two counter
machines (Minsky machines) in LLW2. In order to obtain the faithfulness of
the encoding we use the phase semantic. But here we need the phase semantic
for linear affine logic. So, we introduce such semantic.
Let we have a phase space (M,\bot), where M is a commutative monoid, and \bot
is a subset of M. We say that the phase space (M,\bot) is suitable for LLW if
M*\bot=\bot.
Theorem. If a formula A is derivable in MALLW2, then any phase space
(M,\bot) which is suitable for LLW satisfies A.
We can encode Minsky machines by the following way. Let us consider two
formulas:
F[x]=(x -o f) -o h, G[x]=(x -o g) -o e.
Then we construct the following infinite sets of formulas:
F_0=F[a], F_1=F[F[a]], ...., F_n=F[F_{n-1}]
G_0=G[b], G_1=G[G[b]], ...., G_n=G[G_{n-1}]
Any machine configuration (i,p,q) is encoded by the following formula:
c_i * F_p * G_q.
Here a, b, c_i, e, f, g, h are literals.
A increment transition (i,p,q) -> (j,p+1,q) is encoded by the formula
\forall x,y (c_i * F[x] * G[y] -o c_j * F[F[x]] * G[y]).
A decrement transition (i,p,q) -> (j,p-1,q), if p>0 is encoded by the formula
\forall x,y (c_i * F[F[x]] * G[y] -o c_j * F[x] * G[y]).
And a test-for-zero transition (i,0,q) -> (k,0,q) is encoded by the formula
\forall y (c_i * F[a] * G[y] -o c_k * F[a] * G[y].
By analogous for the second register transitions (i,p,q) -> (j,p,q+1);
(i,p,q) -> (j,p,q-1), if q>0; and (i,p,0) -> (k,p,0) are encoded by the
following formulas
\forall x,y (c_i * F[x] * G[y] -o c_j * F[x] * G[G[y]]).
\forall x,y (c_i * F[x] * G[G[y]] -o c_j * F[x] * G[y]).
\forall x (c_i * F[x] * G[b] -o c_k * F[x] * G[b].
Let \Gamma be a set of formulas of the above kind which encode all
transitions of our machine.
Theorem. The following three assertions are equivalent:
(i) The configuration (i,p,q) is accepted by the machine.
(ii) The following sequent is derivable in MLLW2:
c_i * F_p * G_q, \Gamma^4, C^5 |- c_0 * F_0 * G_0
where C=\forall x (x^4 -o x^5). Here x^n means x*x*...*x (n times),
and \Gamma^n means {A^n | A in G}.
(iii) The above sequent is derivable in MALLW2.
Ptoof.
(i) => (ii). By induction on the length of the computation.
(ii) => (iii). This implication is trivial.
(iii) => (i). By means of phase space.
Moreover, if we add in our sequent the formula W=\forall x,y,z (x*y*z -o y),
then we obtain a stronger theorem:
Theorem. The following four assertions are equivalent:
(1) The configuration (i,p,q) is accepted by the machine.
(2) The following sequent is derivable in LC2:
c_i*F_p*G_q, \Gamma, W, \Gamma, W, \Gamma, W, \Gamma, W, C'^5, W |- c_0*F_0*G_0
where C'=\forall x (x^4 -o x^6).
(3) The above sequent is derivable in any logic L, such that L is a subset
of LLW2, and a superset of LC2.
(4) This sequent is derivable in LLW2.
Proof.
(1) => (2). By induction on the length of the computation.
(2) => (3), (3) => (4). These implications are trivial.
(4) => (1). By means of phase space.
As a corollary, we get the undecidability of all logics described in the
item (3). The undecidability of some of these logics are already known:
IMLL2, IMALL2 (Lincoln, Scedrov and Shankar), MALL2 (Lafont), MALL2 (Lafont
and Scedrov), N-IMLL2 (Emms), N-MLL2, LC2 (Kanovich). Additionally we obtain
some new undecidability results. For example, MLLW2, MALLW2, LLW2, IMLLW2,
N-IMLLW2 and so on.
Best regards,
Alexei Kopylov.