Teoria existențială a numerelor reale

Teoria existențială a numerelor reale este mulțimea tuturor afirmațiilor adevărate ale formei

unde este o formulă fără cuantificatori , care include egalități și inegalități de polinoame reale [1] .

Problema de solubilitate pentru teoria existențială a numerelor reale este problema găsirii unui algoritm care decide pentru fiecare formulă dacă este adevărată sau nu. În mod echivalent, aceasta este problema verificării că o mulțime semi-algebrică dată nu este goală [1] . Această problemă de solubilitate este NP-hard și se află în PSPACE [2] . Astfel, problema este mult mai puțin complexă decât procedura de eliminare a cuantificatorilor lui Alfred Tarski în teoriile reale de ordinul întâi [1] . Cu toate acestea, în practică, metodele generale pentru teoria de ordinul întâi rămân alegerea preferată pentru rezolvarea unor astfel de probleme [3] .

Multe probleme naturale ale teoriei graficelor geometrice , în special problemele de recunoaștere a graficelor de intersecție geometrică și de îndreptare a muchiilor desenelor de grafice cu intersecții , pot fi rezolvate prin conversia lor într-o variantă a teoriei existențiale a numerelor reale și sunt complete pentru această teorie. Pentru a descrie aceste sarcini, se definește o clasă de complexitate , care se află între NP și PSPACE [4] .

Fundal

În logica matematică , o „teorie” este un limbaj formal format dintr-un set de propoziții scrise folosind un set fix de simboluri. Teoria de ordinul întâi a câmpurilor reale închise are următoarele simboluri [5] :

Secvența acestor simboluri formează o propoziție care aparține teoriei primului ordin al realelor, dacă este corectă din punct de vedere gramatical, toate variabilele sale au cuantificatori adecvați și (atunci când este interpretată ca o afirmație matematică despre reale ) este o afirmație validă. După cum a arătat Tarski, această teorie poate fi descrisă printr-o schemă de axiomă și printr-o procedură de decizie completă și eficientă, adică: pentru orice enunț corect din punct de vedere gramatical cu un set complet de cuantificatori, fie afirmația în sine, fie negația sa (dar nu ambele). ) se poate deduce din axiome . Aceeași teorie descrie orice câmp închis real , nu doar numere reale [6] . Există totuși și alte sisteme numerice care nu sunt descrise exact de aceste axiome. Teoria, definită în același mod pentru numere întregi în loc de numere reale, conform teoremei lui Matiyasevich , este indecidabilă chiar și pentru enunțurile de existență pentru ecuațiile diofante [5] [7] .

Teoria existențială a numerelor reale este un subset al teoriei de ordinul întâi și constă din afirmații în care fiecare cuantificator este un cuantificator existențial și toate apar înaintea oricărui alt simbol. Adică este un set de afirmații adevărate de formă

unde este o formulă fără cuantificatori care conține egalități și inegalități cu polinoame peste numere reale . Problema decidabilitatii pentru teoria existențială a numerelor reale este problema algoritmică a verificării dacă o propoziție dată aparține acestei teorii. În mod echivalent, pentru șirurile care trec verificările de sintaxă de bază (adică propoziția folosește caracterele corecte, are sintaxa corectă și nu are variabile fără cuantificatori), sarcina este de a verifica dacă declarația este o declarație adevărată peste numere reale. . Mulțimea de n -tupluri de numere reale pentru care este adevărată se numește mulțime semi-algebrică , astfel încât problema solubilității pentru teoria existențială a numerelor reale poate fi reformulată în mod echivalent prin verificarea faptului că o mulțime semi-algebrică dată nu este goală . 1] .

Pentru a determina complexitatea în timp a algoritmilor pentru problema de rezolvare a teoriei existențiale a numerelor reale, este important să existe o modalitate de a măsura dimensiunea intrării. Cel mai simplu mod de a măsura acest tip este lungimea propoziției, adică numărul de caractere incluse în enunțul [5] . Cu toate acestea, pentru a obține o analiză mai precisă a comportamentului algoritmilor pentru această problemă, este convenabil să se împartă dimensiunea intrării în mai multe variabile, evidențiind numărul de variabile cu cuantificatori, numărul de polinoame din propoziție, iar gradele acestor polinoame [8] .

Exemple

Raportul de aur poate fi definit ca rădăcina unui polinom . Acest polinom are două rădăcini, dintre care doar una (rația de aur) este mai mare decât una. Astfel, existența raportului de aur poate fi exprimată prin propoziție

Deoarece există raportul de aur, afirmația este adevărată și aparține teoriei existențiale a numerelor reale. Răspunsul la problema de solubilitate pentru teoria existențială a numerelor reale, dată fiind această propoziție ca intrare, este valoarea booleană adevărată ( adevărat ).

Inegalitatea dintre media aritmetică și media geometrică afirmă că pentru oricare două numere nenegative și următoarea inegalitate este valabilă:

Enunțul este un enunț de ordinul întâi asupra numerelor reale, dar este universal (nu conține cuantificatori existențiali) și folosește simboluri suplimentare pentru diviziune, rădăcină pătrată și numărul 2, care nu sunt permise în teoria de ordinul întâi a numerele reale. Cu toate acestea, după pătrarea ambelor părți, propoziția poate fi transformată în următoarea afirmație existențială, care poate fi interpretată ca întrebând dacă există un contraexemplu pentru inegalitate:

Răspunsul la problema de solubilitate pentru teoria existențială a numerelor reale, a cărei intrare este această ecuație, este valoarea booleană false ( false ), adică nu există un contraexemplu. Astfel, această propoziție nu aparține teoriei existențiale a numerelor reale, deși este corectă din punct de vedere al gramaticii.

Algoritmi

Metoda eliminării cuantificatorilor a lui Alfred Tarski (1948) arată că teoria existențială a realurilor (și mai general teoria de ordinul întâi a realurilor) este algoritmic decidabilă, dar fără limite elementare ale complexității [9] [6] . Metoda de descompunere algebrică cilindrică a lui Collins (1975) a îmbunătățit dependența de timp de exponențialitate dublă [9] , [10] a formei

unde este numărul de biți necesari pentru a reprezenta coeficienții din instrucțiunea a căror valoare urmează să fie determinată, este numărul de polinoame din enunț, este gradul lor comun și este numărul de variabile [8] În 1988 , Dmitri Grigoriev și Nikolai Vorobyov au arătat că complexitatea este exponențială, gradul fiind un polinom în [8] [11] [12] ,

și într-o serie de lucrări publicate în 1992, James Renegar a îmbunătățit estimarea la puțin peste exponentul on [8] [13] [14] [15] .

Între timp, în 1988 John Canny a descris un alt algoritm care, de asemenea, depinde exponențial de timp, dar are doar complexitate de memorie polinomială. Adică a arătat că problema poate fi rezolvată în clasa PSPACE [2] [9] .

Complexitatea computațională asimptotică a acestor algoritmi poate induce în eroare, deoarece algoritmii pot funcționa doar cu dimensiuni de intrare foarte mici. Comparând algoritmii din 1991, Hong Hong a estimat timpul procedurii Collins (cu evaluare dublă exponențială) pentru o problemă a cărei dimensiune este descrisă prin setarea tuturor parametrilor de mai sus la 2 la mai puțin de două secunde, în timp ce algoritmii lui Grigoriev, Vorobyov iar Renegar ar cheltui pentru a rezolva problema mai mult de un milion de ani [8] . În 1993 Yos, Roy și Solerno au sugerat că ar trebui să fie posibil să se modifice ușor procedurile de timp exponențial pentru a le face mai rapide în practică decât soluția algebrică cilindrică, ceea ce ar fi în concordanță cu teoria [16] . Cu toate acestea, din 2009, metodele generale pentru teoria de ordinul întâi a numerelor reale rămân cele mai bune în practică în comparație cu algoritmii cu evaluare exponențială simplă special concepute pentru teoria existențială a numerelor reale [3] .

Finalizați sarcini

Unele probleme de complexitate computațională și teoria grafurilor geometrice pot fi clasificate ca complete pentru teoria existențială a numerelor reale. Adică orice problemă din teoria existențială a numerelor reale are o reducere polinomială multivalorică la o variantă a uneia dintre aceste probleme și, invers, aceste probleme sunt reductibile la teoria existențială a numerelor reale [4] [17] .

Mai multe probleme de acest tip se referă la recunoașterea graficelor de intersecție de un anumit fel. În aceste probleme, intrarea este un grafic nedirecționat . Scopul este de a determina dacă este posibil să se asocieze geometrii dintr-o anumită clasă cu vârfuri ale graficului în așa fel încât două vârfuri din grafic să fie adiacente dacă și numai dacă geometriile asociate au o intersecție nevide. Probleme complete de acest tip pentru teoria existențială a numerelor reale includ

Pentru graficele desenate în plan fără intersecții, teorema lui Farey afirmă că obținem aceeași clasă de grafice plane indiferent dacă marginile graficului trebuie trasate ca segmente de linie sau pot fi desenate ca curbe. Dar această echivalență de clasă nu este valabilă pentru alte tipuri de reprezentare grafică. De exemplu, deși numărul de intersecție al unui grafic (numărul minim de intersecții ale muchiilor pentru muchiile curbilinii) poate fi definit ca aparținând clasei NP, pentru teoria existențială a numerelor reale se pune problema de a determina dacă există modele pe care un limită dată a numărului de intersecție rectilinie (numărul minim de perechi de muchii care se intersectează în orice figură cu muchii sub formă de segmente drepte pe plan) este complet [4] [20] . Problema completă pentru teoria existențială a numerelor reale este și problema verificării dacă un graf dat poate fi trasat pe un plan cu segmente sub formă de muchii drepte și cu un set dat de perechi de muchii care se intersectează sau, în mod echivalent, dacă un desen cu muchii curbilinii cu intersecții poate fi îndreptat în așa fel încât intersecțiile să fie păstrate [21] .

Alte probleme complete pentru teoria existențială a numerelor reale:

[31] ;

Pe baza acesteia, clasa de complexitate este definită ca un set de probleme care au o reducere de timp polinomială conform lui Karp la teoria existențială a numerelor reale [4] .

Note

  1. ↑ 1 2 3 4 Basu, Pollack, Roy, 2006 , p. 505–532.
  2. ↑ 1 2 Canny, 1988 , p. 460–467.
  3. ↑ 1 2 Passmore, Jackson, 2009 , p. 122–137.
  4. ↑ 1 2 3 4 5 6 7 Schaefer, 2010 , p. 334–344.
  5. ↑ 1 2 3 4 Matousek, 2014 .
  6. ↑ 12 Tarski , 1948 .
  7. ↑ Matiyasevici, 2006 , p. 185–213.
  8. ↑ 1 2 3 4 5 Hong, 1991 .
  9. ↑ 1 2 3 4 Schaefer, 2013 , p. 461–482.
  10. ↑ Collins, 1975 , p. 134–183.
  11. ↑ Grigor'ev, 1988 , p. 65–108.
  12. ↑ Grigor'ev, Vorobjov, 1988 , p. 37–64.
  13. ↑ Renegar, 1992 , p. 255–299.
  14. ↑ Renegar, 1992 , p. 301–327.
  15. ↑ Renegar, 1992 , p. 329–352.
  16. ↑ Heintz, Roy, Solerno, 1993 , p. 427–431.
  17. ↑ 1 2 3 4 Cardinal, 2015 , p. 69–78.
  18. ↑ Kratochvíl, Matousek, 1994 , p. 289–315.
  19. ↑ Kang, Müller, 2011 , p. 308–314.
  20. ↑ Bienstock, 1991 , p. 443–459.
  21. ↑ Kynčl, 2011 , p. 383–399.
  22. ↑ Abrahamsen, Adamaszek, Miltzow, 2017 .
  23. ↑ Mnev, 1988 , p. 527–543.
  24. ↑ Shor, 1991 , p. 531–554.
  25. ↑ Herrmann, Ziegler, 2016 .
  26. ↑ Björner, Las Vergnas, Sturmfels, White, Ziegler, 1993 .
  27. ↑ Richter-Gebert și Ziegler 1995 , p. 403–412.
  28. ↑ Dobbins, Holmsen, Hubard, 2014 .
  29. ↑ Garg, Mehta, Vazirani, Yazdanbod, 2015 , p. 554–566.
  30. ↑ Bilo, Mavronicolas, 2016 , p. 17:1–17:13.
  31. ↑ Bilo, Mavronicolas, 2017 , p. 13:1–13:14.
  32. ↑ Herrmann, Sokoli, Ziegler, 2013 .
  33. ↑ Hoffmann, 2016 .

Literatură