Jason (jcreed) wrote,
Jason
jcreed
Wow. After, trying to write it up for a few hours and not running into any major snags, I think I'm convinced this theorem actually goes through. The result is that, as far as decidability of MELL is concerned, ! need only occur on the left of the turnstile on the top level. So if you can reliably tell me whether things like
!((A -o B) -o (C (x) D)), !E, !(F -o G) |- H -o I
are derivable, I can decide whether things like
!((!A -o !B) -o (!C (x) !D)), !E, !(!F -o !G) |- !H -o !I
with lots of "deeply buried" !s are derivable. This restriction of MELL to only "top-left" bangs is, in turn, equivalent to a slight variant of Petri Nets, or at least I think I've worked it out correctly. It doesn't even seem entirely impossible that the standard Petri Net decidability machinery might even be adaptable to these bizarre Petri-Nets-with-a-Stack. I'm not quite ready to lay my left nut on the line as Rudich did about Primes in P, but I'm really starting to suspect MELL is decidable.
Subscribe

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 6 comments