[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