Beskrivande komplexitetsteori

Beskrivande komplexitet är en gren av beräkningskomplexitetsteori och finita modellteori som kännetecknar komplexitetsklasser av den typ av logik som behövs för att uttrycka språken i dem. Till exempel PH , föreningen av alla komplexitetsklasser i polynomhierarkin, just den klass av språk som kan uttryckas genom påståenden av andra ordningens logik . Denna koppling mellan komplexitet och ändliga strukturers logik gör att resultat enkelt kan överföras från ett område till ett annat, vilket underlättar nya bevismetoder och ger ytterligare bevis för att de huvudsakliga komplexitetsklasserna på något sätt är "naturliga" och inte knutna till de specifika abstrakta maskiner som används . att definiera dem.

Specifikt producerar varje logiskt system en uppsättning frågor som kan uttryckas i det. Frågorna – när de är begränsade till ändliga strukturer – motsvarar beräkningsproblemen i traditionell komplexitetsteori.

Det första huvudsakliga resultatet av beskrivande komplexitet var Fagins teorem , visad av Ronald Fagin 1974. Den fastställde att NP är just den uppsättning språk som kan uttryckas genom meningar av existentiell andra ordningens logik ; det vill säga andra ordningens logik exklusive universell kvantifiering över relationer , funktioner och delmängder . Många andra klasser karakteriserades senare på ett sådant sätt.

Inställningen

När vi använder den logiska formalismen för att beskriva ett beräkningsproblem, är inputen en finit struktur, och elementen i den strukturen är diskursens domän . Vanligtvis är inmatningen antingen en sträng (med bitar eller över ett alfabet) och elementen i den logiska strukturen representerar strängens positioner, eller så är inmatningen en graf och elementen i den logiska strukturen representerar dess hörn. Längden på ingången kommer att mätas av storleken på respektive struktur. Oavsett struktur kan vi anta att det finns relationer som kan testas, till exempel " $E(x,y)$ är sant om och bara om det finns en kant från $x$ till $y$ " (om strukturen är en graf), eller " $P(n)$ är sant om och endast om den $n:$ te bokstaven i strängen är 1." Dessa relationer är predikaten för första ordningens logiska system. Vi har även konstanter, som är speciella element i respektive struktur, om vi till exempel vill kontrollera nåbarhet i en graf måste vi välja två konstanter s ( start ) och t (terminal).

I deskriptiv komplexitetsteori antar vi ofta att det finns en total ordning över elementen och att vi kan kontrollera likheten mellan elementen. Detta låter oss betrakta element som tal: elementet $x$ representerar talet $n$ om och endast om det finns $(n-1)$ element $y$ med $y<x$ . Tack vare detta kan vi också ha det primitiva predikatet "bit", där $bit(x,k)$ är sant om bara den $k$ :te biten av den binära expansionen av $n$ är 1. (Vi kan ersätta addition och multiplikation med ternära relationer så att $plus(x,y,z)$ är sant om och endast om $x +y=z$ och $times(x,y,z)$ är sant om och endast om $x*y=z$ ).

Översikt över karaktäriseringar av komplexitetsklasser

Om vi begränsar oss till ordnade strukturer med en efterföljande relation och grundläggande aritmetiska predikat, får vi följande karakteriseringar:

Första ordningens logik definierar klassen AC ⁰ , språken som känns igen av polynomstorlekskretsar med begränsat djup, vilket är lika med språken som känns igen av en samtidig direktåtkomstmaskin i konstant tid.
Första ordningens logik utökad med symmetriska eller deterministiska transitiva stängningsoperatorer ger L , problem som kan lösas i logaritmiskt rymd.
Första ordningens logik med en transitiv stängningsoperator ger NL , problemen lösbara i icke-deterministiskt logaritmiskt rymd.
Första ordningens logik med en minsta fixpunktsoperator ger P , de problem som kan lösas i deterministisk polynomtid.
Existentiell andra ordningens logik ger NP .
Universell andra ordningens logik (exklusive existentiell andra ordningens kvantifiering) ger co-NP .
Andra ordningens logik motsvarar polynomhierarkin PH .
Andra ordningens logik med en transitiv stängning (kommutativ eller inte) ger PSPACE , problemen lösbara i polynomrymden.
Andra ordningens logik med en minsta fixpunktsoperator ger EXPTIME , problemen lösbara i exponentiell tid.
HO , komplexitetsklassen definierad av logik av högre ordning , är lika med ELEMENTARY

Subpolynomtid

FO utan några operatörer

⁰ I kretskomplexitet kan första ordningens logik med godtyckliga predikat visas vara lika med AC ⁰ , den första klassen i AC -hierarkin. Det finns faktiskt en naturlig översättning från FO:s symboler till noder av kretsar, där $\forall ,\exists$ är $\land$ och $\lor$ av storleken $n$ . Första ordningens logik i en signatur med aritmetiska predikat kännetecknar begränsningen av AC- familjen av kretsar till de som kan konstrueras i alternerande logaritmisk tid . Första ordningens logik i en signatur med endast ordningsrelationen motsvarar uppsättningen stjärnfria språk .

Transitiv stängningslogik

Första ordningens logik får avsevärt uttryckskraft när den utökas med en operator som beräknar den transitiva stängningen av en binär relation. Den resulterande transitiva stängningslogiken är känd för att karakterisera icke-deterministiskt logaritmiskt rymd (NL) på ordnade strukturer. Detta användes av Immerman för att visa att NL är stängt under komplement (dvs. att NL = co-NL).

När den transitiva stängningsoperatorn begränsas till deterministisk transitiv stängning , karakteriserar den resulterande logiken logaritmiskt utrymme på ordnade strukturer.

Andra ordningens Krom-formler

På strukturer som har en efterföljande funktion kan NL också karakteriseras av andra ordningens Krom-formler .

SO-Krom är uppsättningen booleska frågor som kan definieras med andra ordningens formler i konjunktiv normal form så att första ordningens kvantifierare är universella och den kvantifierarfria delen av formeln är i Krom form, vilket betyder att första ordningens formel är en konjunktion av disjunktioner, och i varje "disjunktion" finns det högst två variabler. Varje andra ordningens Krom-formel motsvarar en existentiell andra ordningens Krom-formel.

SO-Krom kännetecknar NL på strukturer med en efterföljande funktion.

Polynomtid

fångar första ordningens minsta fixpunktslogik PTIME :

Första ordningens minsta fixpunktslogik

FO[LFP] är förlängningen av första ordningens logik med en minst fixpunktsoperator, som uttrycker fixpunkten för ett monotont uttryck. Detta förstärker första ordningens logik med förmågan att uttrycka rekursion. Immerman–Vardi-satsen, visad oberoende av Immerman och Vardi , visar att FO[LFP] karakteriserar PTIME på ordnade strukturer.

Från och med 2022 är det fortfarande öppet om det finns en naturlig logik som kännetecknar PTIME på oordnade strukturer.

Abiteboul–Vianu-satsen säger att FO[LFP]=FO[PFP] på alla strukturer om och endast om FO[LFP]=FO[PFP]; alltså om och endast om P=PSPACE. Detta resultat har utökats till andra fixpunkter.

Andra ordningens hornformler

I närvaro av en efterföljande funktion kan PTIME också karakteriseras av andra ordningens hornformler.

SO-Horn är uppsättningen av booleska frågor som kan definieras med SO-formler i disjunktiv normalform så att första ordningens kvantifierare alla är universella och den kvantifieringsfria delen av formeln är i hornform , vilket betyder att den är en stor AND av OR, och i varje "ELLER" förnekas varje variabel utom möjligen en.

Denna klass är lika med P på strukturer med en efterföljande funktion.

Dessa formler kan omvandlas till prenex-formler i existentiell andra ordningens Horn-logik.

Icke-deterministisk polynomtid

Fagins teorem

Ronald Fagins bevis från 1974 på att komplexitetsklassen NP karakteriserades exakt av de klasser av strukturer som är axiomatiserbara i existentiell andra ordningens logik var utgångspunkten för deskriptiv komplexitetsteori.

Eftersom komplementet till en existentiell formel är en universell formel, följer det omedelbart att co-NP kännetecknas av universell andra ordningens logik.

SO, obegränsad andra ordningens logik, är lika med polynomhierarkin PH . Mer exakt har vi följande generalisering av Fagins sats: Uppsättningen formler i prenex normal form där existentiella och universella kvantifierare av andra ordningen omväxlande k tider kännetecknar den k: te nivån i polynomhierarkin.

Till skillnad från de flesta andra karakteriseringar av komplexitetsklasser, förutsätter inte Fagins sats och dess generalisering en total ordning på strukturerna. Detta beror på att existentiell andra ordningens logik i sig är tillräckligt uttrycksfull för att referera till de möjliga totala beställningarna på en struktur med hjälp av andra ordningens variabler.

Bortom NP

Partiell fixpunkt är PSPACE

Klassen för alla problem som kan beräknas i polynomrymden, PSPACE , kan karakteriseras genom att förstärka första ordningens logik med en mer uttrycksfull partiell fixpunktsoperator.

Partiell fixpunktslogik , FO[PFP], är förlängningen av första ordningens logik med en partiell fixpunktsoperator, som uttrycker fixpunkten för en formel om det finns en och returnerar "falskt" annars.

Partiell fixpunktslogik kännetecknar PSPACE på ordnade strukturer.

Transitiv stängning är PSPACE

Andra ordningens logik kan utökas av en transitiv stängningsoperator på samma sätt som första ordningens logik, vilket resulterar i SO[TC]. TC-operatören kan nu även ta andra ordningens variabler som argument. SO[TC] kännetecknar PSPACE . Eftersom ordning kan refereras i andra ordningens logik, förutsätter inte denna karakterisering ordnade strukturer.

Elementära funktioner

Tidskomplexitetsklassen ELEMENTARY av elementära funktioner kan karakteriseras av HO , komplexitetsklassen av strukturer som kan kännas igen av formler av högre ordningslogik . Högre ordningens logik är en förlängning av första ordningens logik och andra ordningens logik med högre ordningens kvantifierare. Det finns ett samband mellan $i$ :e ordningen och icke-deterministiska algoritmer vars tid begränsas av $i-1$ nivåer av exponentialer.

Definition

Vi definierar variabler av högre ordning. En variabel av ordning $i>1$ har en arity $k$ och representerar vilken som helst uppsättning av $k$ - tupler av ordningselement $i-1$ . De skrivs vanligtvis med versaler och med ett naturligt tal som exponent för att indikera ordningen. Högre ordningens logik är uppsättningen av första ordningens formler där vi lägger till kvantifiering över högre ordningens variabler; därför kommer vi att använda termerna som definieras i FO- artikeln utan att definiera dem igen.

HO $^{i}$ är uppsättningen formler med ordningsvariabler som högst $i$ . HO $_{j}^{i}$ är delmängden av formler av formen $\phi =\exists {\overline {X_{1}^{i}}}\forall {\overline {X_{2}^{i}}}\dots Q{\overline {X_{j}^{i}}}\psi$ , där $Q$ är en kvantifierare och $Q{\overline {X^{i}}}$ betyder att ${\overline {X^{i}} }$ är en tuppel av variabel av ordningen $i$ med samma kvantifiering. Så HO $_{j}^{i}$ är uppsättningen formler med $j$ alterneringar av kvantifierare av ordningen ${\displaystyle i} ,$ som börjar med $\exists$ , följt av en formel av ordning $i-1$ .

Med hjälp av standardnotationen för tetrationen , $\exp _{2}^{0}(x)=x$ och $\exp _{2}^{i+1}(x)=2^{\exp _{2}^{i}(x)}$ . $\exp _{2}^{i+1}(x)=2^{2^{2^{2^{\dots ^{2^{x}}}}}$ med $i$ gånger $2$

Normal form

Varje formel av ordning $i$ th är ekvivalent med en formel i prenex normal form, där vi först skriver kvantifiering över variabeln i { $displaystyle i}$ :e ordningen och sedan en formel av ordningen $i -1$ i normal form.