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

38

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

András Salamon
źródło
2
Przez „logikę” rozumiem, co oznacza Grohe: rozstrzygający zestaw zdań nad słownictwem, a relacja „jest modelem” między skończonymi strukturami i zdaniami, z tą właściwością, że zbiór modeli zdania jest zawsze zamknięty w ramach izomorfizmu .
András Salamon,
Zobacz także cstheory.stackexchange.com/questions/174/..., aby dowiedzieć się, czy istnieje logika przechwytująca PTIME.
András Salamon,
Logika liniowa to logika zdań, która zawiera klasyczną logikę zdań. Można go rozszerzyć, aby umożliwić kwantyfikatory. Ale jeśli dobrze pamiętam, związek między logiką liniową (zdania) a klasami złożoności różni się od tego, co Grohe ma na myśli, przynajmniej nie widzę, jak powiązać logikę liniową z zapytaniami o struktury skończone.
Kaveh
Istnieją teorie oparte na logice liniowej, takie jak Teoria zbiorów afinicznych Terui, które mają tę właściwość, że można w niej udowodnić, że funkcja jest całkowita, i tylko wtedy, gdy funkcja jest obliczalna w czasie wielomianowym. Zobacz citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730
Neel Krishnaswami
1
Kaveh, dlatego przyznałem nagrodę Slimtonowi. Bardziej szczegółowa odpowiedź nadal byłaby miła.
András Salamon,

Odpowiedzi:

23

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 .

(R)(x)(ϕ)
RxϕRR
slimton
źródło
3
Ups, teraz, kiedy ponownie przeczytałem twoje pytanie, zdaję sobie sprawę, że jest nieco inne niż poprzednia wersja. Teraz poprosisz o operator X, aby FOL + X przechwycił duży fragment P. W takim przypadku powinieneś spojrzeć na <a href=" logcom.oxfordjournals.org/content/5/2/…> Dawara . pokazuje, że jeśli istnieje logika dla P, to istnieje taka, rozszerzając FOL o uogólnione kwantyfikatory
slimton
3
Powinienem dodać, że fragment Rogu egzystencjalnej logiki drugiego rzędu na nagich strukturach jest raczej słaby: właściwy podzbiór LFP na nagich strukturach. Potrzebujemy następcy, aby uzyskać twierdzenie Grädela. Wynik Dawara dotyczy nagich konstrukcji.
slimton
8
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 is a finite graph and nnodes(g)}

(g,n)ϕnϕ():M×MM

(g,n)(g,n)={(g,nn)when g=gnn=undefinedotherwise

Łą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:

(g,n)In=(g,n)ϕψn1,n2.n=n1n2 and (g,n1)ϕ and (g,n2)ψ(g,n)ϕψn.if nn= and (g,n)ϕ then (g,nn)ψ(g,n)always(g,n)ϕψ(g,n)ϕ and (g,n)ψ

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.

Neel Krishnaswami
źródło
Jaką rolę odgrywa struktura wykresu w powyższym modelu? Powyższa definicja wydaje się działać dobrze, jeśli powiemy, że zakresy g są na wykresach dyskretnych.
Charles Stewart,
Ponieważ dowolny (częściowy) przemienny monoid może być użyty do stworzenia modelu BI / logiki liniowej, struktura wykresu nie jest używana do interpretacji połączeń i - ma to znaczenie tylko dla zdań atomowych. Na przykład w logice separacji istnieje propozycja atomowa „punkty do” , którą używamy do interpretacji struktury wskaźnika. nn
Neel Krishnaswami,
8

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.

Sebastian Siebertz
źródło
1
Zauważ, że Anderson / Dawar / Holm ostatnio pokazał, że FP + C może wyrażać programowanie liniowe ( arxiv.org/abs/1304.6870 ). Podważa to interpretację wcześniejszego wyniku Dawara na wzór „FP + C nie może rozwiązać układów równań liniowych”; Dawar tylko twierdził, że pewne „naturalne problemy polegające układów równań liniowych nie są definiowane w tym logiki”, z którym wydaje się on mieć oznaczało obliczeń rangi.
András Salamon,
7

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

Aaron Sterling
źródło
1
Myślę, że András chce logiki w sensie złożoności opisowej.
Kaveh
7

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.

Dave Clarke
źródło