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

unit-only LL is not trivial



>From Max Kanovich:

 Here we focus on the study of the simplest fragments
 of Linear Logic such as one-literal and constant-only ones
 (the latter contains no literals at all) and demonstrate that
 these extremely simple fragments are of the same expressive
 power as the corresponding full versions.

 According to one of the well-known approaches, the hierarchy of
 natural fragments of Linear Logic can be developed in the
 following way:
 For a given fragment of Linear Logic LL{\sigma}
 (its formulas are built up of literals and constants
  by connectives from the set of connectives~$\sigma$,
  constants are taken from \sigma),
 we can reduce the number of the literals used to a fixed
 number $k$ and study the corresponding fragment LL^k{\sigma}.

 We study the simplest cases when $k$ is small, namely,
 we will study the one-literal fragment LL1{\sigma} and
 constant-only fragment LL0{\sigma}.

 Actually, this approach is also quite traditional.

 E.g., consideration of the one-literal fragment of
 intuitionistic propositional logic allows us to obtain the full
 characterization of this fragment and shed light on the
 true nature of intuitionistic logic as a whole.

 As for the expressive power of constant-only fragments of
 traditional logical systems, it is equal to zero:
 the entire problem boils down to primitive Boolean calculations
 over constants.

 Let us recall some results related to the problem in question.

 We use the following connectives:
 Multiplicatives: tensor |x|, Par, and linear implication -o.
 Additives:       & and \oplus.
 Exponentials:    the storage operator ! and 'whynot' ?.
 Constants:       \bottom and 1.

 Let us recall that
 1. LL{|x|,-o} is NP-complete (Kanovich, 1991).
 2. LL{|x|,Par,&,\oplus} is PSPACE-complete
                       (Lincoln, Mitchell, Scedrov, and Shankar, 1990)
 3. LL{|x|,-o,!} can encode Petri Nets reachability.
 4. LL{|x|,Par,&,\oplus,!} is undecidable
                       (Lincoln, Mitchell, Scedrov, and Shankar, 1990)

 For one-literal fragments, we have
 1. LL1{|x|,Par,-o} is NP-complete (Kanovich, 1992).
 2. Moreover, LL1{-o} is NP-complete (Kanovich, 1992).
 3. LL1{-o,&} is PSPACE-complete (Kanovich, 1993).
 4. LL1{-o,!} can encode Petri Nets reachability (Kanovich, 1993).
 5. LL1{-o,&,!} can directly simulate standard Minsky machines,
    and, hence, it is undecidable   (Kanovich, 1992).

 For \bottom-only fragments, we have
 1. LL0{|x|,Par,\bottom} is NP-complete (Lincoln and Winkler, 1992).
 2. Moreover, LL0{-o,\bottom} is NP-complete (Kanovich, 1992).
 3. LL0{-o,&,\bottom} is PSPACE-complete (Kanovich, 1993).
 4. LL0{-o,!,\bottom} can encode Petri Nets reachability (Kanovich, 1993).
 5. LL0{-o,&,!,\bottom} can directly simulate standard Minsky machines,
    and, hence, it is undecidable   (Kanovich, 1992).

 In addition to item 4, we can simulate full 'negation-and-Par-free'
 intuitionistic linear logic ILL{|x|,-o,!} both in
 one-literal LL1{-o,!} and in \bottom-only LL0{-o,!,\bottom}.

 We prove the following results for Unit-only fragments of LL:
 1. LL0{|x|,-o,1} is trivial.
 2. Nevertheless, LL0{|x|,Par,-o,1} is NP-complete.
 3. LL0{|x|,Par,-o,&,1} is PSPACE-complete.
 4. LL0{|x|,Par,-o,!,1} can simulate ILL{|x|,-o,!}, and, hence,
    its complexity level is not less than the level of
    Multiplicative-Exponential Fragment of 'negation-and-Par-free' ILL.
 5. LL0{|x|,Par,-o,&,!,1} can directly simulate standard Minsky machines,
    and, hence, it is undecidable.

 It should be noted that the Unit-only case is the most complicated
 one:
 In the absence of negation and \bottom, the system of connectives
          |x|, Par, -o, &, \oplus
 is functionally incomplete (even in the Boolean sense).

 My best regards,
 Max Kanovich.