Techniki odwracania porządku kwantyfikatorów

Dobrze wiadomo, że ogólnie nie można odwrócić kolejności uniwersalnych i egzystencjalnych kwantyfikatorów. Innymi słowy, dla logicznego ogólnym wzorze ,$\phi(\cdot,\cdot)$

$(\forall x)(\exists y) \phi(x,y) \quad \not\Leftrightarrow \quad (\exists y)(\forall x) \phi(x,y)$

Z drugiej strony wiemy, że prawa strona jest bardziej restrykcyjna niż lewa; czyli $(\exists y)(\forall x) \phi(x,y) \Rightarrow (\forall x)(\exists y) \phi(x,y)$ .

To pytanie koncentruje się na technikach uzyskiwania $(\forall x)(\exists y) \phi(x,y) \Rightarrow (\exists y)(\forall x) \phi(x,y)$ , ilekroć jest to ważne dla $\phi(\cdot,\cdot)$ .

Diagonalizacja jest jedną z takich technik. Po raz pierwszy widzę to zastosowanie diagonalizacji w artykule Relatywizacje pytania $\mathcal{P} \overset{?}{=} \mathcal{NP}$ (patrz także krótka notka Katza ). W tym artykule autorzy najpierw udowadniają, że:

Dla każdej deterministycznej, wielomianowej maszyny wyroczniowej M istnieje język B taki, że $L_B \ne L(M^B)$ .

Następnie odwracają kolejność kwantyfikatorów (wykorzystując diagonalizację ), aby udowodnić, że:

Istnieje język B taki, że dla wszystkich deterministycznych M mamy .$L_B \ne L(M^B)$

Ta technika jest używana w innych artykułach, takich jak [CGH] i [AH] .

Znalazłem inną technikę w dowodzie Twierdzenia 6.3 [IR] . Wykorzystuje połączenie teorii miary i zasady gołębia do odwrócenia kolejności kwantyfikatorów.

Chcę wiedzieć, jakie inne techniki są stosowane w informatyce, aby odwrócić kolejność uniwersalnych i egzystencjalnych kwantyfikatorów?

Odwrócenie kwantyfikatorów jest ważną właściwością, która często stoi za dobrze znanymi twierdzeniami.

Na przykład w analizie różnica między i jest różnicą między ciągłością punktową a jednolitą . Dobrze znane twierdzenie mówi, że każda punktowa mapa ciągła jest jednolicie ciągła, pod warunkiem, że domena jest ładna, tj . Zwarta .$\forall \epsilon > 0 . \forall x . \exists \delta > 0$$\forall \epsilon > 0 . \exists \delta > 0 . \forall x$

W rzeczywistości zwartość jest podstawą odwrócenia kwantyfikatora. Rozważmy dwa typy danych i , z których jest jawny i jest zwarty (patrz poniżej wyjaśnienia tych warunkach) i niech być semidecidable stosunek pomiędzy i . Instrukcja można odczytać w następujący sposób: każdy punkt w jest objęty pewnym . Ponieważ zestawy są „obliczalne otwarte” (półdecydowalne) i$X$$Y$$X$$Y$$\phi(x,y)$$X$$Y$$\forall y : Y . \exists x : X . \phi(x,y)$$y$$Y$$U_x = \lbrace z : Y \mid \phi(x,z) \rbrace$$U_x$$Y$jest zwarty, istnieje skończona subcover. Udowodniliśmy, że oznacza, że Często możemy zredukować istnienie skończonej listy do pojedynczego . Na przykład, jeśli jest uporządkowane liniowo, a jest monotoniczny w względem kolejności, to możemy przyjąć, że jest największym z .

$$\forall y : Y . \exists x : X . \phi(x,y)$$ $$\exists x_1, \ldots, x_n : X . \forall y : Y . \phi(x_1,y) \lor \cdots \lor \phi(x_n, y).$$ $x_1, \ldots, x_n$$x$$X$$\phi$$x$$x$$x_1, \ldots, x_n$

Aby zobaczyć, jak ta zasada jest stosowana w znanym przypadku, spójrzmy na stwierdzenie, że jest funkcją ciągłą. Zachowujemy jako wolną zmienną, aby nie pomylić zewnętrznego zewnętrznego uniwersalnego kwantyfikatora: Ponieważ jest zwarta, a porównanie liczb rzeczywistych jest w połowie nierozstrzygalne, instrukcja jest w połowie niezdecydowany. Pozytywne liczby rzeczywiste są jawne, a jest zwarta, więc możemy zastosować zasadę: $f : [0,1] \to \mathbb{R}$$\epsilon > 0$

$$\forall x \in [0,1] . \exists \delta > 0 . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| < \epsilon.$$ $[x - \delta, x + \delta]$$\phi(x, \delta) \equiv \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| < \epsilon$$[0,1]$ $$\exists \delta_1, \delta_2, \ldots, \delta_n > 0 . \forall x \in [0,1] . \phi(\delta_1, x) \lor \cdots \phi(\delta_n, x).$$ Ponieważ jest antymonotonem w najmniejszym z już to robi, więc potrzebujemy tylko : Mamy jednolitą ciągłość .$\phi(\delta, x)$$\delta$$\delta_1, \ldots, \delta_n$$\delta$ $$\exists \delta > 0 . \forall x \in [0,1] . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| < \epsilon.$$ $f$

Mówiąc niejasnie, typ danych jest zwarty, jeśli ma obliczalny uniwersalny kwantyfikator, i jawnie, jeśli ma obliczalny kwantyfikator egzystencjalny. (Nieujemne) liczby całkowite są jawne, ponieważ w celu ustalenia, czy , przy czym połowie nierozstrzygalny, przeszukujemy równolegle przez połączenie typu jaskółczy ogon . Przestrzeń Cantora jest zwarta i jawna, jak wyjaśniono w Abstract Stone Duality Paula Taylora oraz w „ Syntetycznej topologii typów danych i przestrzeni klasycznych ” Martina Escardo (zobacz także powiązane pojęcie przestrzeni do przeszukiwania ).$\mathbb{N}$$\exists n \in \mathbb{N} . \phi(n)$$\phi(n)$$2^\mathbb{N}$

Pozwól nam zastosować zasadę do wspomnianego przykładu. Widzimy język jako mapę od (skończonych) słów nad ustalonym alfabetem do wartości boolowskich. Ponieważ słowa skończone są w obliczalnej biotywnej korespondencji z liczbami całkowitymi, możemy postrzegać język jako mapę od liczb całkowitych do wartości boolowskich. Oznacza to, że typem danych wszystkich języków jest, aż do obliczalnego izomorfizmu, dokładnie przestrzeń Cantora nat -> boollub zapis matematyczny , który jest zwarty. Maszyna Turinga w czasie wielomianowym jest opisana przez swój program, który jest ciągiem skończonym, w związku z czym można przyjąć, że przestrzeń wszystkich (reprezentacji) maszyn Turinga jest jawna lub .$2^\mathbb{N}$nat$\mathbb{N}$

Biorąc pod uwagę maszynę Turinga i język , wyrażenie które mówi „język jest odrzucany przez ”, jest w połowie nierozstrzygalne, ponieważ w rzeczywistości jest rozstrzygalne: po prostu uruchom z wejściem i zobacz, co to robi. Warunki dla naszej zasady są spełnione! Stwierdzenie „każda maszyna wyroczni ma język taki, że nie jest akceptowane przez ”, jest zapisywane symbolicznie jako Po odwróceniu kwantyfikatorów otrzymujemy $M$$c$$\mathsf{rejects}(M,c)$$c$$M$$M$$c$$M$$b$$b$$M^b$

$$\forall M : \mathbb{N} . \exists b : 2^\mathbb{N} . \mathsf{rejects}(M^b,b).$$ $$\exists b_1, \ldots, b_n : 2^\mathbb{N} . \forall M : \mathbb{N} . \mathsf{rejects}(M^{b_1}, b_1) \lor \cdots \lor \mathsf{rejects}(M^{b_n},b_n).$$ Ok, więc skończymy z wieloma językami. Czy możemy połączyć je w jeden? Zostawię to jako ćwiczenie (dla mnie i dla ciebie!).

Być może zainteresuje Cię nieco bardziej ogólne pytanie, jak przekształcić do równoważnego wyrażenia formularza lub odwrotnie. Można to zrobić na kilka sposobów, na przykład:$\forall x . \exists y . \phi(x,y)$$\exists u . \forall v . \psi(u,v)$

• Skolem normalna forma ,
• Postać normalna Herbrand ,
• Interpretacja funkcjonalna Gödela .

Twardy rdzeń lematu Impagliazzo umożliwia zmianę kwantyfikatorów w kontekście założeń dotyczących twardości obliczeniowej. Oto oryginalny artykuł . Możesz znaleźć mnóstwo powiązanych artykułów i postów od Googling.

Lemat mówi, że jeśli dla każdego algorytmu A istnieje duży zestaw danych wejściowych, na których A nie oblicza stałej funkcji f, to w rzeczywistości istnieje duży zestaw danych wejściowych, na których każdy algorytm nie oblicza f z prawdopodobieństwem bliskim 1 / 2.

Ten lemat można udowodnić za pomocą twierdzenia min-max lub wzmocnienia (technika z teorii uczenia obliczeniowego), które są przykładami kwantyfikatorów przełączających.

Dla mnie „kanoniczny” dowód twierdzenia Karp-Lipton (że ) ma ten smak. Ale tutaj nie chodzi o rzeczywiste twierdzenie, w którym kwantyfikatory ulegają odwróceniu, ale raczej „kwantyfikatory” odwracane są w modelu obliczeń przemiennych, przy założeniu, że ma małe obwody.$NP \subseteq P/poly \Longrightarrow \Pi_2 P = \Sigma_2 P$$NP$

Chcesz symulować obliczenia formularza

$(\forall y)(\exists z)R(x,y,z)$

gdzie jest predykatem czasu wielomianowego. Możesz to zrobić, odgadując mały obwód kątem (powiedzmy) satysfakcji, modyfikując aby sprawdzał się i tworzy zadowalające przypisanie, gdy jego dane wejściowe są zadowalające. Następnie przez całe utwórz instancję SAT równoważną i rozwiąż ją. Więc stworzyłeś równoważne obliczenie formularza$R$$C$$C$$y$$S(x,y)$$(\exists z)R(x,y,z)$

$(\exists C)(\forall y)[S(x,y)$ jest zadowalające zgodnie z .$C]$

Podstawowe zastosowanie związku związanego w metodzie probabilistycznej można interpretować jako sposób na odwrócenie kolejności kwantyfikatorów. Chociaż jest to już wspomniane w pytaniu w sposób dorozumiany, ponieważ dowód Impagliazzo i Rudicha jest tego przykładem, uważam, że warto to powiedzieć bardziej wyraźnie.

Załóżmy, że X jest skończony i że dla każdego x ∈ X wiemy nie tylko, że niektóre y ∈ Y spełniają φ ( x , y ), ale także że wiele opcji y ∈ Y spełnia φ ( x , y ). Formalnie załóżmy, że wiemy (∀ x ∈ X ) Pr _{y ∈ Y} [￢φ ( x , y )] <1 / | X | dla pewnej miary probabilistycznej na Y. Następnie związek związany pozwala stwierdzić Pr _{y ∈ Y} [(∃ x ∈ X ) Ź φ ( x , y )] <1, co odpowiada (∃ y ∈ Y ) (∀ x ∈ X ) cp ( x , y ).

Istnieją odmiany tego argumentu:

1. Jeśli X jest nieskończony, czasami możemy dyskretyzować X , biorąc pod uwagę odpowiednią metrykę na X i jej wartość ε- net. Po dyskretyzacji X możemy użyć związku związanego jak wyżej.

2. Kiedy zdarzenia φ ( x , y ) dla różnych wartości x są prawie niezależne, możemy użyć lokalnego lematu Lovásza zamiast związać związkiem.

Chciałbym dodać kilka innych technik. Chociaż dwie pierwsze techniki nie służą do odwrócenia kolejności uniwersalnych i egzystencjalnych kwantyfikatorów, mają bardzo podobny smak. Dlatego skorzystałem z okazji, aby opisać je tutaj:

Uśrednianie Lemmy: Służy do udowodnienia i wielu innych interesujących twierdzeń. Nieformalnie załóżmy, że oznacza zbiór subskrybentów jakiejś biblioteki, oznacza zbiór książek w bibliotece, a dla i , propozycja jest prawdziwa dla subskrybenta lubi książkę . ” Lemat uśredniający stwierdza, że: jeśli dla każdego istnieje co najmniej 2/3 w tak że utrzymuje, to istnieje jeden$BPP \subset P/poly$$S$$B$$s\in S$$b \in B$$\phi(s,b)$$s$$b$$s \in S$$b$$B$$\phi(s,b)$$b \in B$Tak, że co najmniej 2/3 „s w , propozycja posiada. (Można to łatwo udowodnić za pomocą reductio ad absurdum i argumentu liczącego.)$s$$S$$\phi(s,b)$

Teraz niech i niech być maszyną PPT który decyduje . Załóżmy, że czas działania jest ograniczony przez wielomian . Następnie, dla każdego i dla co najmniej 2/3 , s , to utrzymuje, że . Tutaj jest maszyny , która wykorzystuje losowość i jest funkcją charakterystyczną . Lemat uśredniający jest następnie używany, aby pokazać, że dla dowolnego$L \in BPP$$M(\cdot)$$L$$M$$q(\cdot)$$x \in \{0,1\}^*$$r$$r \in \{0,1\}^{q(|x|)}$$M_r(x) = \chi_L(x)$$M_r(\cdot)$$M$$r$$\chi_L(\cdot)$$L$$n \in \mathbb{N}$, istnieje pojedynczy , taki że dla co najmniej 2/3 długości , . Ten pojedynczy działa jako rada dla , a zatem .$r \in \{0,1\}^{q(n)}$$x$$n$$M_r(x) = \chi_L(x)$$r$$M$$BPP \subset P/poly$

NOTE: I re-emphasize that this is not a quantifier switching technique, but it has the same spirit.

Zamiana lematu: Zachos i Fürer wprowadzili nowy kwantyfikator probabilistyczny (co z grubsza oznacza „dla większości”). Udowodnili, że (pomijając szczegóły):$\exists^+$

$(\forall y)(\exists^+z) \phi(x,y,z) \Rightarrow (\exists^+ \mathbf{C})(\forall y)(\exists z \in \mathbf{C})\phi(x,y,z)$

Zauważ, że jest to twierdzenie logiczne drugiego rzędu.

Korzystając z lematu wymiany, udowodnili szereg interesujących twierdzeń, takich jak twierdzenie BPP i twierdzenie Babai'ego . Więcej informacji odsyłam do oryginalnej pracy.$MA \subseteq AM$

Twierdzenie podobny do Karp-Lipton twierdzenia wymienionego w Ryan Williams słupka: .$coNP \subset NP/Poly \Longrightarrow \Pi_3 P = \Sigma_3 P$