Complessità descrittiva

In informatica teorica , la complessità descrittiva è una branca della teoria della complessità e teoria dei modelli , che caratterizza le classi di complessità in termini di logica per la descrizione dei problemi.

La complessità descrittiva offre un nuovo punto di vista perché definiamo le classi di complessità senza fare appello a una nozione di macchine come le macchine di Turing . Ad esempio la classe NP corrisponde all'insieme dei problemi esprimibili in logica esistenziale del secondo ordine : è il teorema di Fagin .

Principio

Esempio: colorare un grafico

Spieghiamo il principio della complessità descrittiva con il problema della 3-colorazione di un grafo . Si tratta del problema decisionale che consiste nel sapere, dato un grafo, se si possono colorare i suoi vertici con tre colori in modo che due vertici adiacenti non siano dello stesso colore. La figura a destra fornisce un esempio di un grafico a 3 colori.

Il problema della 3-colorazione è nella classe NP . Infatti, data una colorazione, è facile verificare (cioè in tempo polinomiale nella dimensione del grafo) che due vertici adiacenti non siano dello stesso colore.
D'altra parte, il problema della 3-colorazione è descritto dalla formula della logica del secondo ordine esistenziale successivo . Questa formula dice "c'è un insieme di vertici C 1 , un altro insieme di vertici C 2 , un altro insieme di vertici C 3 (1, 2, 3 sono i tre possibili colori) come: ∃VS1,∃VS2,∃VS3,(∀S,⋁io=13VSio(S))∧(∀S⋀io,j=1io≠j3(¬VSio(S)∨¬VSj(S)))∧(∀t,R(S,t)→⋀io=13(¬VSio(S)∨¬VSio(t))){\ displaystyle \ esiste C_ {1}, \ esiste C_ {2}, \ esiste C_ {3}, \ left (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ destra) \ terra \ sinistra (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ non C_ {i} (s) \ lor \ l non C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ non C_ {i} (s) \ lor \ non C_ {i} (t)) \ destra)} ${\ displaystyle \ esiste C_ {1}, \ esiste C_ {2}, \ esiste C_ {3}, \ left (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ destra) \ terra \ sinistra (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ non C_ {i} (s) \ lor \ l non C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ non C_ {i} (s) \ lor \ non C_ {i} (t)) \ destra)}$
- ogni vertice è colorato (ogni vertice è in uno dei sottoinsiemi C i ),
- ogni vertice ha al massimo un solo colore (ogni vertice è in al massimo uno dei sottoinsiemi C i ),
- due vertici adiacenti sono di colore diverso.

Problema decisionale come query

Quindi, nella complessità descrittiva, un problema decisionale è descritto da una formula logica, che corrisponde a fare una query (ad esempio, la query "è il grafico 3-coloribile?"). Un'istanza di un problema decisionale è un modello (ad esempio, un grafico per il problema delle 3 colorazioni è visto come un modello) su cui possono essere valutate le formule logiche. Le istanze positive di un problema decisionale (cioè nell'esempio i grafici 3-colorabili) sono esattamente i modelli in cui la formula è vera.

Un altro esempio

Si consideri il problema decisionale A che consiste nel determinare se un grafo G è tale che ogni vertice di G ammette un arco incidente. Un grafo G è visto come un modello in cui gli elementi del dominio sono i vertici del grafo e la relazione del grafo è un predicato . Il problema decisionale A può essere espresso in logica del primo ordine perché le istanze positive sono descritte dalla formula (qualsiasi vertice s ammette un successore t). $R$ ${\ displaystyle \ per tutte le s, \ esiste t, sRt}$

Teorema di Fagin

Il primo risultato del dominio, e uno dei più importanti, è il teorema di Fagin che dà l'equivalenza tra:

la classe NP , per definizione, la classe dei problemi decisionali per i quali è facile verificare una soluzione;
e la classe dei problemi esprimibili in logica esistenziale del secondo ordine , cioè logica del secondo ordine dove si vieta di quantizzare universalmente su predicati e funzioni.

Corrispondenza tra classi e logiche

Anche molte altre classi sono state caratterizzate allo stesso modo e sono riassunte nella tabella seguente, principalmente da Neil Immerman .

Classi di complessità	Logica corrispondente
AC⁰	logica del primo ordine
NL	logica del primo ordine con chiusura transitiva
P	logica del primo ordine con punto fisso più piccolo
NP	logica esistenziale del secondo ordine
co-NP	logica universale del secondo ordine
PH	logica del secondo ordine
PSPACE	logica del secondo ordine con chiusura transitiva
SCADENZA	logica del secondo ordine con punto fisso più piccolo
ELEMENTARE	logica di ordine superiore
RI	logica esistenziale del primo ordine su interi
nucleo	logica universale del primo ordine su interi

Esempio per NL

Interessi

Neil Immerman giustifica la teoria della complessità descrittiva perché mostra che le classi di complessità definite utilizzando le macchine di Turing sono naturali : sono definibili anche se non utilizziamo modelli computazionali classici. Inoltre questa teoria fornisce un nuovo punto di vista su certi risultati e certe congetture della teoria della complessità, ad esempio il teorema di Abiteboul e Vianu (en) indica che le classi P e PSPACE sono uguali se le logiche Inflationary Fix Point (IFP) e Partial Fix Point (PFP) sono uguali.

Link esterno

La pagina di Neil Immerman sulla complessità descrittiva, con diagramma .

varianti

La classe PTIME intersecata con problemi invarianti per bisimulazione corrisponde alla logica del mu-calcolo dimensionale superiore.

Bibliografia

Articoli

(it) Ronald Fagin , " Spettri del primo ordine generalizzati e insiemi riconoscibili in tempo polinomiale " , Proc. Simposi SIAM-AMS. Appl. Matematica. , Ame. Matematica. Soc., vol. VII "Complessità di calcolo" ,1974, pag. 43-73 ( Math Reviews 0371622 , lettura online , accesso 7 novembre 2019 )
(it) Neil Immerman , “ Linguaggi che catturano classi di complessità ” , STOC '83 Atti del quindicesimo simposio annuale ACM sulla teoria dell'informatica ,1983, pag. 347-354 ( ISBN 0-89791-099-0 , DOI 10.1145 / 800061.808765 , leggi online )
(it) Serge Abiteboul et Victor Vianu , “ Calcolo generico e sua complessità ” , STOC '91 Atti del ventitreesimo simposio annuale ACM sulla teoria dell'informatica ,1991, pag. 209-219 ( ISBN 0-89791-397-3 , DOI 10.1145 / 103418.103444 )

Lavori

(it) Neil Immerman , Complessità descrittiva , New York, Springer-Verlag,1999( ISBN 0-387-98600-6 , presentazione online )
(it) Martin Grohe , Complessità descrittiva, canonizzazione e teoria della struttura grafica definibile , Cambridge University Press,2017, 554 pag. ( ISBN 978-1-139-02886-8 , leggi in linea ) , cap. I.3 (“Complessità descrittiva”) , p. 40-93

Note e riferimenti

( Fagin 1974 ).
Fonti per importanza: Siamo ora pronti a Teorema di stato di Fagin e l'Immerman-Vardi Teorema, probabilmente i due maggior parte dei risultati fondamentali nella teoria della complessità descrittiva. in ( Grohe 2017 )
Vedi introduzione di ( Immerman 1983 ).
( Abiteboul e Vianu 1991 ).
Martin Otto , “ PTIME invariante per bisimulazione e μ-calcolo dimensionale superiore ”, Informatica teorica , vol. 224, n . 1,6 agosto 1999, pag. 237-265 ( ISSN 0304-3975 , DOI 10.1016 / S0304-3975 (98) 00.314-4 , leggere on-line , accessibile 22 nov 2019 )