Czy można zastosować opisową złożoną wersję twierdzenia Rice'a do oddzielenia AC0 i PSPACE?

W tym pytaniu wspomniano, że istnieją opisowe wersje złożoności twierdzenia Rice'a. Znalazłem dowód na następujące twierdzenie:

Biorąc pod uwagę klasę złożoności C , nietrywialnych właściwości języków w C nie można obliczyć w C

Wcześniej opublikowałem znaleziony dowód, ale ponieważ był on tak długi i ponieważ w komentarzach wskazano, że ten artykuł zawiera już dowód tego twierdzenia, usunąłem go. (Jeśli z jakiegoś powodu desperacko chcesz zobaczyć mój dowód, zapoznaj się z poprzednimi wersjami tego pytania).

Interesuje mnie, czy to twierdzenie może być użyte do rozdzielenia AC0 i PSPACE. Oto argument:

Rozważ właściwość P klasy złożoności AC0 zdefiniowaną następująco:

P : właściwość bycia zapytaniem FO, które akceptuje określoną stałą strukturę, a mianowicie strukturę składającą się z jednego elementu, bez funkcji, bez stałych i bez relacji

Oczywiście, zgodnie z powyższym twierdzeniem, P nie jest rozstrzygalne w AC0; jest to nietrywialna właściwość zapytań FO.

Jednak małe badanie powinno wykazać, że obliczenie, czy zapytanie FO akceptuje tak prostą strukturę, może być ustalone tak łatwo, jak TQBF; zatem P jest rozstrzygalne w PSPACE.

Aby zapewnić jasność w tym punkcie (że P jest obliczalny w PSPACE): Zauważ, że właściwość, która nas interesuje, wymaga, aby struktura była FO. Próbujemy więc ustalić, czy zapytanie FO działające na strukturze jednoelementowej bez relacji akceptuje. Ponieważ nie ma żadnych relacji do rozwiązania, powinno być jasne, że zadanie podjęcia decyzji o takim zapytaniu FO jest równoważne z podjęciem decyzji o wystąpieniu TQBF; nie ma żadnych relacji, więc jedynym wyzwaniem pozostaje ocena, czy skwantyfikowana formuła boolowska jest prawdziwa. Jest to w zasadzie tylko TQBF, więc P jest obliczalny w PSPACE.

Ponieważ P jest obliczalny w PSPACE, ale nie w AC0, powinniśmy móc stwierdzić, że AC0! = PSPACE. Czy to rozumowanie jest prawidłowe, czy też gdzieś popełniłem błąd? Jestem szczególnie zaniepokojony poprzednim akapitem; Spróbuję wyjaśnić i zaktualizować argument jutro po tym, jak będę miał okazję nieco bardziej przemyśleć ekspozycję.

Jako odpowiedź przyjąłbym przykład zapytania FO, które, gdy obliczam na jednoelementowej, wolnej od relacji strukturze, którą opisałem, wyraźnie nie ma sensu jako przykład TQBF. (Sugeruję, że nie ma takiego, więc jeśli możesz wykazać, że taki istnieje, byłby to kontrprzykład).

Dzięki.

— Philip White
źródło

@Kaveh: Powinieneś zamienić swój komentarz w odpowiedź.

— Dai Le

@Kaveh: Dzięki za komentarz. Jestem jednak trochę zdezorientowany tym, co mówisz. Która maszyna w PSPACE dla zestawów AC0 miała na myśli? Miałem na myśli właściwość P, która odnosi się konkretnie do zapytań FO dotyczących bardzo prostych struktur. Sugeruję, że ocena, czy zapytania FO akceptują prostą strukturę, jest gwarantowana jako TQBF, czyli PSPACE. Nie wiem, gdzie potrzebny jest uniwersalny symulator dla AC0.

— Philip White

@Kaveh: OK. Przygotuję próbę udowodnienia przypuszczenia w tym pytaniu i opublikuję jako osobne pytanie. Myślałem, że to prawda, ale często się mylę. (Oczywiście, jeśli wcześniej obalisz moją hipotezę, nie zawracam sobie głowy).

— Philip White

O. Właśnie opublikowałem to jako pytanie. Czy powinienem usunąć nowe pytanie i opublikować je jako odpowiedź?

— Philip White

(Usunąłem go i dodałem do tego pytania.)

— Philip White

Podjęcie decyzji o nietrywialnych właściwościach (indeksowania) zbiorów w klasie złożoności jest tak trudne, jak obliczenie wykresu funkcji uniwersalnej dla tej klasy. Intuicyjnie oznacza to, że jedynym sposobem na wybranie nietrywialnej właściwości jest symulacja maszyn i oczekiwanie na odpowiedzi. Wydaje mi się, że pomysł użycia takiej właściwości da po prostu to, co znają twierdzenia o hierarchii. (Patrz twierdzenie 4.2 D. Kozen, „ Indeksowanie klas subrekurencyjnych ”, 1978 w celu uzyskania szczegółów i dokładnego stwierdzenia twierdzenia.)

Możemy zdecydować o (wykres funkcji uniwersalnej dla ) w , powodem jest po prostu to, że i mamy uniwersalną maszynę do języków w w , więc to łatwo jest symulować maszyny (lub opisowy równoważnik złożoności który jest zapytaniami ) w . Oznacza to, że możemy zdecydować o nieruchomości, którą w . Ponieważ jest to nietrywialna właściwość, nie podlega rozstrzygnięciu w . Tak więc ten argument oddziela od $grU_{AC^0}$ $AC^0$ $PSpace$ $AC^0 \subseteq L$ $L$ $PSpace$ $AC^0$ $AC^0$ $FO$ $PSpace$ $PSpace$ $AC^0$ $AC^0$ $PSapce$ .

Ale czy to zaskakujące? Nie, ponieważ znamy już prostszy sposób (zasadniczo) tego samego argumentu: , ostatnim właściwym włączeniem jest twierdzenie o hierarchii przestrzeni. $AC^0 \subseteq L \subset PSpace$

— Kaveh
źródło

Ciekawe dzięki. Więc mówisz: 1) Mój argument był słuszny, ale 2) Był łatwiejszy sposób. :) Chyba muszę odświeżyć twierdzenie o hierarchii przestrzeni.

— Philip White

@Filip: tak, myślę, że twój argument jest zasadniczo słuszny (pomyślałem, że możesz chcieć ponownie sprawdzić definicję , język ma nielogiczne symbole).

F O

$FO$

— Kaveh

Ok świetnie. Właśnie sprawdziłem definicję FO. Wiedziałem, że zawiera symbol równości; dlatego wymagałem, aby struktura była tylko jednym elementem. W ten sposób każde stwierdzenie o równości dwóch zmiennych nie wpłynie na prawdziwość zapytania.

— Philip White

Jeden dodatkowy komentarz ... zrobiłeś ważny punkt na temat nielogicznych symboli. Ponieważ nie ma relacji, symbol równości jest tak naprawdę niezbędny. W szczególności konieczne jest wyrażenie bardzo logicznych literałów, które są potrzebne do wyrażenia TQBF.

— Philip White

@Philip: jeśli dobrze pamiętam, język zawiera również relacje dotyczące porządku, dodawania, mnożenia i bitów (myślę, że niektóre są definiowalne od innych).

F O

$FO$

— Kaveh