[Prev][Next][Index][Thread]
Constant-Only LL is undecidable
We prove that propositional Linear Logic containing
either only one literal or only one constant \bottom
is of the extreme expressive power.
As a corollary, both one-literal Linear Logic
and constant-only Linear Logic turned out to be undecidable.
P.Lincoln, J.Mitchell, A.Scedrov, and N.Shankar (1990)
proved the undecidability of full propositional Linear Logic
(containing Multiplicatives, Additives, and Exponentials).
We proved the undecidability for a restricted fragment
of Linear Logic (the so-called generalized Horn fragment)
containing only four literals (LICS'92).
Here we prove that any standard Minsky machines can be
directly encoded in each of the two following fragments
of Linear Logic:
1. A one-literal fragment of LL.
It consists of sequents of the form
Gamma, !Delta |- p
where multisets Gamma and Delta contain
(a) the only positive literal p,
(b) no other literals,
(c) neither negative literals, nor constants, nor negations,
(d) two multiplicatives: tensor product and linear implication,
(e) one additive: & (or +),
(f) no exponentials
(! appears only outside of formulas from the multiset !Delta).
2. A constant-only fragment of LL.
It consists of sequents of the form
Gamma, !Delta |- \bottom
where multisets Gamma and Delta contain
(a) no literals at all,
(b) the only constant \bottom,
(c) neither other constants, nor negations,
(d) only one multiplicative: linear implication,
(e) one additive: & (or +),
(f) no exponentials
(! appears only outside of formulas from the multiset !Delta).
Our encoding of computations of standard counter machines by
derivations of the corresponding sequents is based on a
complete computational characterization of certain fragments
of Linear Logic.
Best regards,
Max Kanovich.