[Prev][Next][Index][Thread]

MLL2 is undecidable



       The Undecidability of Second Order Multiplicative Linear Logic 


                         Yves Lafont and Andre Scedrov 



                                    Abstract

In referring to linear logic fragments, let M stand for multiplicatives, 
A for additives, 2 for second order quantifiers, and I for "intuitionistic" 
version of linear logic fragments.  

Lincoln, Scedrov, and Shankar showed the undecidability IMLL2 and IMALL2 
(announced in this forum, to appear in LICS '95). Lafont has subsequently 
proved the undecidability of MALL2 (announced in this forum, to appear in 
the Journal of Symbolic Logic). It is the case that MLL2 is undecidable. 

Consider 
              #A = A * (A -o 1) 
and  
               D = Forall X Forall Y (#X * #Y  -o  X * X * #Y * Y). 

The formula D may be used to encode a restricted kind of contraction. 
Indeed, the rules 

           Gamma |- B                 D^2, #A, A, Gamma |- B
   -------------------------         ------------------------
    D^2, #Theta, Gamma |- B            D^2, #A, Gamma |- B  

are derivable. Also, D holds in any phase model in which {1} is 
closed under double orthogonal (i.e., the singleton {1} is a "fact") 
and in which 1 is the only invertible element of the commutative 
monoid underlying the phase model. 

A register machine configuration (i,p,q) consisting of a state i, 
first counter value p, and second counter value q, is encoded as 
b_i * F[a^p] * G[a^q], where b_i is an atom, a^p is the p-fold 
tensor of a's, and the formulas F and G are defined as follows: 

 F[X] = X^3 * (X -o d) * (X -o e)  -o  f , 

 G[X] = X^3 * (X -o d) * (X -o e)  -o  g , 

where d,e,f,g are atoms. For instance, first counter increment 
is encoded as Forall X (b_i * F[X]  -o  b_j * F[a*X]), zero test as 
b_i * F[1] -o b_k * F[1], and similarly for the other transitions. 

Theorem. Let T_1, ..., T_n be the formulas encoding the machine 
transitions. The following are equivalent: 
  1. A machine configuration id (i,p,q) is accepted, 
  2. The sequent

        D^2, #T_1, ..., #T_n, b_i * F[a^p] * G[a^q] |- b_0 * F[1] * G[1] 
 
     is provable in IMLL2, 
  3. The above sequent is provable in MLL2. 

The direction 1 -> 2 does not depend on the particular choice of F,G. 
The difficult part, 3 -> 1, uses a particular phase model constructed 
to represent exactly the accepted configurations.