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.

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$