[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.