Beskrivende kompleksitet

I teoretisk informatikk er den deskriptive kompleksiteten en gren av kompleksitetsteori og modellteori , som karakteriserer kompleksitetsklassene når det gjelder logikk for å beskrive problemene.

Beskrivende kompleksitet gir et nytt synspunkt fordi vi definerer kompleksitetsklasser uten å appellere til forestillingen om maskiner som Turing-maskiner . For eksempel tilsvarer klassen NP det settet med problemer som kan uttrykkes i eksistensiell annenordenslogikk : det er Fagins teorem .

Prinsipp

Eksempel: fargelegge en graf

La oss forklare prinsippet om beskrivende kompleksitet med problemet med trefarging av en graf . Det handler om avgjørelsesproblemet som består i å vite, gitt en graf, om man kan farge toppunktene sine med tre farger, slik at to tilstøtende hjørner ikke har samme farge. Figuren til høyre gir et eksempel på en trefarget graf.

3-fargingsproblemet er i NP-klassen . Faktisk, gitt en farging, er det enkelt å kontrollere (dvs. i polynomisk tid i størrelsen på grafen) at to tilstøtende hjørner ikke har samme farge.
På den annen side er 3-fargeproblemet beskrevet av formelen for logikken til neste eksistensielle andre orden . Denne formelen lyder "det er ett sett med hjørner C 1 , et annet sett med hjørner C 2 , et annet sett med hjørner C 3 (1, 2, 3 er de tre mulige farger) som: ∃VS1,∃VS2,∃VS3,(∀s,⋁Jeg=13VSJeg(s))∧(∀s⋀Jeg,j=1Jeg≠j3(¬VSJeg(s)∨¬VSj(s)))∧(∀t,R(s,t)→⋀Jeg=13(¬VSJeg(s)∨¬VSJeg(t))){\ displaystyle \ eksisterer C_ {1}, \ eksisterer C_ {2}, \ eksisterer C_ {3}, \ venstre (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ høyre) \ land \ venstre (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {i} (t)) \ høyre)} ${\ displaystyle \ eksisterer C_ {1}, \ eksisterer C_ {2}, \ eksisterer C_ {3}, \ venstre (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ høyre) \ land \ venstre (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {i} (t)) \ høyre)}$
- ethvert toppunkt er farget (ethvert toppunkt er i en av undergruppene C i ),
- ethvert toppunkt har maksimalt bare en farge (ethvert toppunkt er i det meste en av delmengdene C i ),
- to tilstøtende hjørner er forskjellige farger.

Beslutningsproblem som et spørsmål

Således, i beskrivende kompleksitet, blir et beslutningsproblem beskrevet med en logisk formel, som tilsvarer å lage et spørsmål (for eksempel spørringen "er grafen 3-fargeløs?"). En forekomst av et avgjørelsesproblem er en modell (f.eks. En graf for 3-fargeproblemet blir sett på som en modell) som logiske formler kan evalueres på. De positive forekomster av et avgjørelsesproblem (dvs. i eksemplet de trefargede grafene) er nøyaktig modellene der formelen stemmer.

Et annet eksempel

Tenk på avgjørelsesproblemet A som består i å avgjøre om en graf G er slik at et G-toppunkt innrømmer en innfallskant. En graf G blir sett på som en modell der elementene i domenet er toppunktene i grafen og forholdet til grafen er et predikat . Beslutningsproblemet A kan uttrykkes i første ordens logikk fordi de positive forekomster er beskrevet av formelen (ethvert toppunkt innrømmer en etterfølger t). $R$ ${\ displaystyle \ forall s, \ exist t, sRt}$

Fagins teorem

Det første resultatet av domenet, og en av de viktigste er Fagins teorem som gir ekvivalensen mellom:

den klasse NP , ved definisjon, klassen av beslutningsproblemer som det er lett å se etter en løsning;
og klassen av problemer som kan uttrykkes i eksistensiell annenordenslogikk , det vil si annenordenslogikk der man forby universell kvantifisering av predikater og funksjoner.

Korrespondanse mellom klasser og logikk

Mange andre klasser har også blitt karakterisert på samme måte og er oppsummert i følgende tabell, for det meste av Neil Immerman .

Kompleksitetsklasser	Tilsvarende logikk
AC⁰	førsteordens logikk
NL	førsteordens logikk med en transitiv lukking
P	første ordens logikk med minste faste punkt
NP	eksistensiell annenordenslogikk
co-NP	universell andreordens logikk
PH	andre ordens logikk
PSPACE	andre ordens logikk med en transitiv lukking
EXPTIME	andre ordens logikk med minste faste punkt
ELEMENTÆR	høyere ordenslogikk
RE	første ordens eksistensielle logikk på heltall
kjerne	universell førsteordenslogikk over heltall

Eksempel for NL

Interesser

Neil Immerman rettferdiggjør beskrivende kompleksitetsteori fordi den viser at kompleksitetsklassene definert ved hjelp av Turing-maskiner er naturlige : de kan defineres selv om vi ikke bruker klassiske beregningsmodeller. Videre gir denne teorien et nytt synspunkt på visse resultater og visse antagelser om kompleksitetsteori, for eksempel teoremet til Abiteboul og Vianu (en) indikerer at klassene P og PSPACE er like hvis logikken Inflationary Fix Point (IFP) og Partial Fix Point (PFP) er like.

Ekstern lenke

Neil Immermans side om beskrivende kompleksitet, med diagram .

Varianter

Klassen PTIME krysset med uforanderlige problemer ved bisimulering tilsvarer logikken til den høyere dimensjonale mu-kalkulus .

Bibliografi

Artikler

(en) Ronald Fagin , “ Generalized First-Order Spectra and Polynomial-Time Recognizable Sets ” , Proc. SIAM-AMS Sympos. Appl. Matte. , Amer. Matte. Soc., Vol. VII "Kompleksitet av beregning" ,1974, s. 43-73 ( Matematikkanmeldelser 0371622 , lest online , åpnet 7. november 2019 )
(en) Neil Immerman , “ Languages which Capture Complexity Classes ” , STOC '83 Proceedings of the femtenth annual ACM symposium on Theory of computing ,1983, s. 347-354 ( ISBN 0-89791-099-0 , DOI 10.1145 / 800061.808765 , les online )
(en) Serge Abiteboul et Victor Vianu , “ Generic Computation and Its Complexity ” , STOC '91 Proceedings of the tjuetredde ACM symposium on Theory of Computing ,1991, s. 209-219 ( ISBN 0-89791-397-3 , DOI 10.1145 / 103418.103444 )

Virker

(no) Neil Immerman , Descriptive Complexity , New York, Springer-Verlag,1999( ISBN 0-387-98600-6 , online presentasjon )
(en) Martin Grohe , Descriptive Complexity, Canonization, and Definable Graph Structure Theory , Cambridge University Press,2017, 554 s. ( ISBN 978-1-139-02886-8 , leses online ) , kap. I.3 (“Beskrivende kompleksitet”) , s. 40-93

Merknader og referanser

( Fagin 1974 ).
Kilder for betydning: Vi er nå klare til å uttale Fagins teorem og Immerman-Vardi-teoremet, uten tvil de to mest grunnleggende resultatene i beskrivende kompleksitetsteori. i ( Grohe 2017 )
Se introduksjon av ( Immerman 1983 ).
( Abiteboul og Vianu 1991 ).
Martin Otto , “ Bisimulation-invariant PTIME og høyere-dimensjonale μ-kalkulus ”, teoretisk informatikk , vol. 224, n o 1,6. august 1999, s. 237–265 ( ISSN 0304-3975 , DOI 10.1016 / S0304-3975 (98) 00314-4 , leses online , åpnes 22. november 2019 )