Czy istnieje logika bez indukcji, która wychwytuje dużą część P?

Twierdzenie Immermana- Vardiego stwierdza, że ​​PTIME (lub P) to właśnie klasa języków, którą można opisać zdaniem logiki pierwszego rzędu wraz z operatorem punktu stałego, nad klasą uporządkowanych struktur. Operator punktu stałego może być albo najmniejszym punktem stałym (według Immermana i Vardiego), albo inflacyjnym punktem stałym. (Stephan Kreutzer, Ekspresyjna równoważność logiki stałoprzecinkowej najmniejszej i inflacyjnej , Annals of Pure and Applic Logic 130 61–78, 2004).

Jurij Gurewicz domyślił się, że nie ma logiki przechwytującej PTIME ( Logika i wyzwanie informatyki , w Aktualne trendy w teoretyce informatyki, red. Egon Boerger, 1–57, Computer Science Press, 1988), podczas gdy Martin Grohe stwierdził, że jest mniej pewny ( The Quest for a Logic Capturing PTIME , FOCS 2008).

Operator punktu stałego ma na celu uchwycenie mocy rekurencji. Punkty stałe są potężne, ale nie jest dla mnie oczywiste, że są konieczne.

Czy istnieje operator X, który nie jest oparty na punktach stałych, tak że FOL + X przechwytuje (duży) fragment PTIME?

Edycja: O ile rozumiem, logika liniowa może wyrażać tylko wypowiedzi o strukturach, które mają dość restrykcyjną formę. Idealnie chciałbym zobaczyć odniesienie lub szkic logiki, która może wyrażać właściwości dowolnych zestawów struktur relacyjnych, jednocześnie unikając stałych punktów. Jeśli się mylę co do ekspresyjnej mocy logiki liniowej, mile widziany jest wskaźnik lub podpowiedź.

Chcesz rzucić okiem na to, co niektórzy nazywają twierdzeniem Grädela. Można go znaleźć w książce Papadimitriou „Złożoność obliczeniowa” (to Twierdzenie 8.4 na stronie 176) lub w oryginalnej pracy Grädela .

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

O ile rozumiem, logika liniowa może wyrażać tylko wypowiedzi o strukturach, które mają dość restrykcyjną formę. Idealnie chciałbym zobaczyć odniesienie lub szkic logiki, która może wyrażać właściwości dowolnych zestawów struktur relacyjnych, jednocześnie unikając stałych punktów. Jeśli się mylę co do ekspresyjnej mocy logiki liniowej, mile widziany jest wskaźnik lub podpowiedź.

To nie jest właściwe: wszystkie zamienione przemienne sieci monoidalne są modelami logiki liniowej. Oto prosty sposób na utworzenie takiej siatki z skończonych wykresów. Zacznij od zestawu

$$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') = \left\{\begin{array}{ll} (g, n \uplus n') & \mbox{when } g = g' \land n \cap n' = \emptyset \\ \mathrm{undefined} & \mbox{otherwise} \end{array}\right.$$

Łączy to dwa elementy, łącząc posiadane zestawy, jeśli wykresy są równe, a posiadane zestawy są rozłączne.

Teraz możemy podać model logiki liniowej w następujący sposób:

$$\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}$$

Ten model jest w rzeczywistości wariantem tych używanych w logice separacji, która jest szeroko stosowana w weryfikacji programów do manipulacji stertami. (Jeśli chcesz, pomyśl o wykresie jako strukturze wskaźnika stosu, a analogia jest dokładna!)

Nie jest to jednak właściwy sposób myślenia o logice liniowej: jej prawdziwe intuicje są teoretyczne, a związek ze złożonością wynika z złożoności obliczeniowej twierdzenia o eliminacji cięć. Modelową teorią logiki liniowej jest cień rzucany przez jej teorię dowodu.

Istnieją ostatnie ekscytujące wyniki dotyczące wyszukiwania logiki przechwytującej PTIME. Słynny przykład Cai, Fürera i Immermana pokazujący, że LFP + C nie przechwytuje PTIME, opierał się jednak na pozornie sztucznej klasie grafów. Oczywiście został skonstruowany do konkretnego zadania polegającego na wykazaniu ograniczeń LFP + C. Dopiero niedawno Dawar wykazał, że klasa wcale nie jest sztuczna. Można to raczej traktować jako przykład tego, że LFP + C nie może rozwiązać układów równań liniowych!

Dlatego Dawar, Grohe, Holm i Laubner rozszerzyli logikę przez operatorów z algebry liniowej, na przykład przez operatora w celu zdefiniowania rangi definiowalnej macierzy. Wynikowa logika rangi LFP + może wyrażać ściśle więcej niż LFP + C, w rzeczywistości nie ma znanej właściwości PTIME, której ranga LFP + nie może wyrazić.

Nawet FO + rk jest zaskakująco silny, może wyrażać deterministyczne i symetryczne przechodnie przechodzenie. Nadal pozostaje otwarte, czy może wyrazić ogólne przechodnie zamknięcie wykresu.

W zależności od tego, co rozumiesz przez „przechwytywanie”, miękka logika liniowa i czas wielomianowy Yvesa Lafonta mogą być interesujące. W tej logice i algorytmach PTIME występuje odpowiednik 1-1, który przyjmuje ciąg wejściowy i wyjściowy 0 lub 1.

Artykuł w Wikipedii na temat logiki liniowej jest tutaj . To nie jest logika punktu stałego. Intuicja „klasycznej logiki nad algebrami zamiast algebrów boolowskich” jest dla mnie najłatwiejsza do zrozumienia.$C^*$

Niektóre starsze prace nad tym problemem, znowu w żyłach logiki liniowej, to Jean-Yves Girard, Andre Scedrov i Philip Scott. Ograniczona logika liniowa: modułowe podejście do obliczania czasu wielomianowego. Theoretical Computer Science, 97 (1): 1–66, 1992.

Nowsze prace obejmują Bounded Linear Logic, ponownie odwiedzone przez Ugo Dal Lago i Martina Hofmanna.