Gibt es eine Logik ohne Induktion, die viel von P erfasst?

38

Das Immerman-Vardi-Theorem besagt, dass PTIME (oder P) genau die Klasse von Sprachen ist, die durch einen Satz der Logik erster Ordnung zusammen mit einem Festkommaoperator über die Klasse von geordneten Strukturen beschrieben werden kann. Der Fixpunktoperator kann entweder der kleinste Fixpunkt (wie von Immerman und Vardi betrachtet) oder der inflationäre Fixpunkt sein. (Stephan Kreutzer, Ausdruck der Äquivalenz von kleinster und inflationärer Festkommalogik , Annals of Pure and Applied Logic 130 61–78, 2004).

Yuri Gurevich vermutete, dass es keine Logik gibt, die PTIME ( Logik und die Herausforderung der Informatik) in den aktuellen Trends der theoretischen Informatik erfasst ( Herausgeber Egon Boerger, 1–57, Computer Science Press, 1988), während Martin Grohe dies erklärt hat weniger sicher ( Die Suche nach einem Logic Capturing PTIME , FOCS 2008).

Der Festkommaoperator soll die Potenz der Rekursion erfassen. Fixpunkte sind mächtig, aber es ist mir nicht klar, dass sie notwendig sind.

Gibt es einen Operator X, der nicht auf Fixpunkten basiert, so dass FOL + X ein (großes) Fragment von PTIME erfasst?

Bearbeiten: Soweit ich weiß, kann lineare Logik nur Aussagen über Strukturen ausdrücken, die eine recht restriktive Form haben. Idealerweise würde ich gerne einen Verweis auf oder eine Skizze einer Logik sehen, die Eigenschaften beliebiger Mengen relationaler Strukturen ausdrücken kann, wobei Fixpunkte vermieden werden. Wenn ich mich in der Aussagekraft der linearen Logik irre, wäre ein Hinweis oder Hinweis willkommen.

cc.complexity-theory lo.logic descriptive-complexity finite-model-theory András Salamon
quelle

2

Mit "Logik" meine ich, was Grohe bedeutet: eine entscheidbare Menge von Sätzen über das Vokabular, und eine Beziehung "ist ein Modell von" zwischen endlichen Strukturen und Sätzen, mit der Eigenschaft, dass die Menge von Modellen eines Satzes immer unter Isomorphismus geschlossen ist .

András Salamon

Siehe auch cstheory.stackexchange.com/questions/174/… für die Frage, ob es eine Logik gibt, die PTIME erfasst.

András Salamon

Lineare Logik ist eine Aussagenlogik, die klassische Aussagenlogik enthält. Es kann erweitert werden, um Quantifizierer zuzulassen. Aber wenn ich mich richtig erinnere, unterscheidet sich das Verhältnis zwischen linearer Logik (Aussagen) und Komplexitätsklassen von dem, was Grohe vor Augen hat, zumindest verstehe ich nicht, wie man lineare Logik mit Abfragen über endliche Strukturen in Beziehung setzt.

Kaveh,

Es gibt Mengen-Theorien, die auf linearer Logik aufbauen, wie zum Beispiel die Light-Affine-Set-Theorie von Terui, die die Eigenschaft haben, dass eine Funktion darin vollständig bewiesen werden kann, und zwar genau dann, wenn die Funktion in Polynomzeit berechenbar ist. Siehe citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730

Neel Krishnaswami

1

Kaveh, aus diesem Grund habe ich das Kopfgeld an Slimton vergeben. Eine ausführlichere Antwort wäre trotzdem nett.

András Salamon

23

Sie möchten einen Blick auf das werfen, was manche Leute den Satz von Grädel nennen. Sie können es in Papadimitriou Buch „Computational Complexity“ finden (es ist Theorem 8.4 in Seite 176) oder in Grädel ursprünglichen Papier .

(\exists R) (\forall x) (ϕ)

$(\exists R)(\forall x)(\phi)$

R

$R$

x

$x$

ϕ

$\phi$

R

$R$

R

$R$

Slimton
quelle

3

Hoppla, jetzt, da ich Ihre Frage noch einmal lese, merke ich, dass sie sich ein bisschen von der vorherigen Version unterscheidet. Nun fragen Sie für einen Operator X , so dass FOL + X Captures ein großes Fragment von P. In diesem Fall können Sie einen Blick auf Dawar der sollte <a href=" logcom.oxfordjournals.org/content/5/2/...> . Er zeigt, dass wenn es eine Logik für P gibt, es eine gibt, indem FOL mit verallgemeinerten Quantifizierern erweitert wird

Slimton

3

Ich sollte hinzufügen, dass das Horn-Fragment der existentiellen Logik zweiter Ordnung auf nackten Strukturen eher schwach ist: eine richtige Teilmenge von LFP auf nackten Strukturen. Wir brauchen den Nachfolger, um den Satz von Grädel zu erhalten. Dawars Ergebnis ist für nackte Strukturen.

Slimton

8

Nach meinem Verständnis kann die lineare Logik nur Aussagen über Strukturen treffen, die eine recht restriktive Form haben. Idealerweise würde ich gerne einen Verweis auf oder eine Skizze einer Logik sehen, die Eigenschaften beliebiger Mengen relationaler Strukturen ausdrücken kann, wobei Fixpunkte vermieden werden. Wenn ich mich in der Aussagekraft der linearen Logik irre, wäre ein Hinweis oder Hinweis willkommen.

Dies ist nicht richtig: Alle residuierten kommutativen monoiden Gitter sind Modelle der linearen Logik. Hier ist eine einfache Möglichkeit, ein solches Gitter aus endlichen Graphen zu erstellen. Beginnen Sie mit dem Set

M = {(g, n) | g is a finite graph and n \subseteq n o d e s (g)}

$M = \{(g, n) \;|\; g\mbox{ is a finite graph and }n \subseteq \mathrm{nodes}(g)\}$

$(g,n) \models \phi$ $n$ $\phi$ $(\cdot) : M \times M \to M$

(g, n) \cdot (g^{'}, n^{'}) = {\begin{cases} (g, n ⊎ n^{'}) & when g = g^{'} \land n \cap n^{'} = \emptyset \\ u n d e f i n e d & otherwise \end{cases}

$(g,n) \cdot (g',n') = \left\{\begin{array}{ll} (g, n \uplus n') & \mbox{when } g = g' \land n \cap n' = \emptyset \\ \mathrm{undefined} & \mbox{otherwise} \end{array}\right.$

Dies kombiniert zwei Elemente durch Zusammenführen ihrer eigenen Mengen, wenn die Graphen gleich sind und die eigenen Mengen disjunkt sind.

Nun können wir ein Modell der linearen Logik wie folgt angeben:

\begin{array}{lcl} (g, n) ⊨ I & ⟺ & n = \emptyset \\ (g, n) ⊨ ϕ \otimes ψ & ⟺ & \exists n_{1}, n_{2} . n = n_{1} ⊎ n_{2} and (g, n_{1}) ⊨ ϕ and (g, n_{2}) ⊨ ψ \\ (g, n) ⊨ ϕ ⊸ ψ & ⟺ & \forall n^{'} . if n \cap n^{'} = \emptyset and (g, n^{'}) ⊨ ϕ then (g, n ⊎ n^{'}) ⊨ ψ \\ (g, n) ⊨ ⊤ & ⟺ & always \\ (g, n) ⊨ ϕ \land ψ & ⟺ & (g, n) ⊨ ϕ and (g, n) ⊨ ψ \end{array}

$\begin{array}{lcl} (g,n) \models I & \iff & n = \emptyset \\ (g,n) \models \phi \otimes \psi & \iff & \exists n_1,n_2.\; n = n_1 \uplus n_2 \mbox{ and } (g,n_1) \models \phi \mbox{ and } (g,n_2) \models \psi \\ (g,n) \models \phi \multimap \psi & \iff & \forall n'.\; \mbox{if } n \cap n' = \emptyset \mbox{ and } (g,n') \models \phi \mbox{ then } (g,n \uplus n') \models \psi \\ (g, n) \models \top & \iff & \mbox{always} \\ (g,n) \models \phi \land \psi & \iff & (g,n) \models \phi \mbox{ and } (g,n) \models \psi \end{array}$

Dieses Modell ist tatsächlich eine Variante der in der Separationslogik verwendeten, die häufig bei der Verifizierung von Programmen zur Heap-Manipulation verwendet wird. (Wenn Sie möchten, stellen Sie sich das Diagramm als Zeigerstruktur des Heaps vor, und die Analogie ist genau!)

Dies ist jedoch nicht wirklich der richtige Weg, um über lineare Logik nachzudenken: Ihre realen Intuitionen sind beweistheoretisch, und die Verbindung zur Komplexität erfolgt über die rechnerische Komplexität des Cut-Elimination-Theorems. Die Modelltheorie der linearen Logik ist der Schattenwurf ihrer Beweistheorie.

Neel Krishnaswami
quelle

Welche Rolle spielt die Graphenstruktur im obigen Modell? Die obige Definition scheint gut zu funktionieren, wenn wir sagen, dass g über den diskreten Graphen liegt.

Charles Stewart

Da jedes (partielle) kommutative Monoid verwendet werden kann, um ein Modell der BI / linearen Logik zu erhalten, wird die Graphstruktur nicht zur Interpretation der und Verknüpfungen verwendet - sie ist nur für die atomaren Aussagen von Bedeutung. Zum Beispiel gibt es in der Trennungslogik einen "Punkte-zu" -Atomsatz , den wir anhand der Zeigerstruktur interpretieren.

\otimes

$\otimes$

⊸

$\multimap$

n \mapsto n^{'}

$n \mapsto n'$

Neel Krishnaswami

8

Es gibt kürzlich aufregende Ergebnisse in Bezug auf die Suche nach einer PTIME-Logikerfassung. Das berühmte Beispiel von Cai, Fürer und Immerman , das zeigt, dass LFP + C PTIME nicht erfasst, basierte jedoch auf einer scheinbar künstlichen Klasse von Graphen. Natürlich wurde es für die besondere Aufgabe konstruiert, die Einschränkungen von LFP + C aufzuzeigen. Erst kürzlich hat Dawar gezeigt, dass die Klasse überhaupt nicht künstlich ist. Es kann eher als Beispiel dafür gesehen werden, dass LFP + C lineare Gleichungssysteme nicht lösen kann!

Daher erweiterten Dawar, Grohe, Holm und Laubner die Logik durch Operatoren aus der linearen Algebra, beispielsweise durch einen Operator, um den Rang einer definierbaren Matrix zu definieren. Der resultierende logische LFP + -Rang kann streng mehr als LFP + C ausdrücken. Tatsächlich ist keine PTIME-Eigenschaft bekannt, die der LFP + -Rang nicht ausdrücken kann.

Auch wenn FO + rk überraschend mächtig ist, kann es einen deterministischen und symmetrischen transitiven Verschluss ausdrücken. Es ist noch offen, ob es den allgemeinen transitiven Abschluss eines Graphen ausdrücken kann.

Sebastian Siebertz
quelle

1

Beachten Sie, dass Anderson / Dawar / Holm kürzlich gezeigt haben, dass FP + C lineare Programmierung ausdrücken kann ( arxiv.org/abs/1304.6870 ). Dies untergräbt eine Interpretation von Dawars früherem Ergebnis nach dem Motto "FP + C kann lineare Gleichungssysteme nicht lösen". Dawar behauptete nur, dass einige "natürliche Probleme mit linearen Gleichungssystemen in dieser Logik nicht definierbar sind", mit denen er Rangberechnungen gemeint zu haben scheint.

András Salamon

7

Je nachdem, was Sie unter "Erfassen" verstehen, kann die weiche lineare Logik und die Polynomialzeit von Yves Lafont von Interesse sein. In dieser Logik und in PTIME-Algorithmen, die eine Zeichenfolge als Eingabe und Ausgabe 0 oder 1 verwenden, gibt es eine 1: 1-Entsprechung zu Beweisen.

Der Wikipedia-Artikel zu Linear Logic ist hier . Es ist keine Fixpunktlogik. Die Intuition der "klassischen Logik über -Algebren anstelle von Booleschen Algebren" ist für mich am einfachsten zu verstehen. $C^*$

Aaron Sterling
quelle

1

Ich denke, András möchte eine Logik im Sinne der beschreibenden Komplexität.

Kaveh

7

Einige ältere Arbeiten zu diesem Problem, ebenfalls in der linearen Logik, sind Jean-Yves Girard, Andre Scedrov und Philip Scott. Begrenzte lineare Logik: Ein modularer Ansatz zur Berechnung der Polynomzeit. Theoretical Computer Science, 97 (1): 1–66, 1992.

Neuere Arbeiten umfassen Bounded Linear Logic, Revisited von Ugo Dal Lago und Martin Hofmann.

Dave Clarke
quelle

Gibt es eine Logik ohne Induktion, die viel von P erfasst?

Antworten: