Eksistentiel teori om reelle tal

Den eksistentielle teori om reelle tal er mængden af ​​alle sande udsagn af formen

hvor er en formel uden kvantifikatorer , som inkluderer ligheder og uligheder af reelle polynomier [1] .

Opløselighedsproblemet for den eksistentielle teori om reelle tal er problemet med at finde en algoritme , der afgør for hver formel, om den er sand eller ej. Tilsvarende er dette problemet med at kontrollere, at en given semi-algebraisk mængde ikke er tom [1] . Dette løselighedsproblem er NP-hårdt og ligger i PSPACE [2] . Problemet er således meget mindre komplekst end proceduren til at eliminere Alfred Tarskis kvantificerere i førsteordens reelle teorier [1] . Men i praksis forbliver generelle metoder til førsteordensteori det foretrukne valg til løsning af sådanne problemer [3] .

Mange naturlige problemer med geometrisk grafteori , især problemer med genkendelse af geometriske skæringsgrafer og udretning af kanter på tegninger af grafer med skæringspunkter , kan løses ved at konvertere dem til en variant af den eksistentielle teori om reelle tal og er fuldstændige for denne teori. For at beskrive disse opgaver defineres en kompleksitetsklasse , som er mellem NP og PSPACE [4] .

Baggrund

I matematisk logik er en "teori" et formelt sprog, der består af et sæt sætninger skrevet ved hjælp af et fast sæt symboler. Den første ordens teori om rigtige lukkede felter har følgende symboler [5] :

Rækkefølgen af ​​disse symboler danner en sætning, der hører til teorien om den første orden af ​​realerne, hvis grammatisk korrekte, har alle dens variable passende kvantifiers, og (når det fortolkes som en matematisk udsagn om realerne ) er en gyldig udsagn. Som Tarski har vist, kan denne teori beskrives ved et aksiomskema og en beslutningsprocedure, der er komplet og effektiv, det vil sige: for enhver grammatisk korrekt udsagn med et komplet sæt af kvantificerere, enten selve udsagnet eller dets negation (men ikke begge dele) ) kan udledes af aksiomerne. Den samme teori beskriver ethvert reelt lukket felt , ikke kun reelle tal [6] . Der er dog andre talsystemer, som ikke præcist er beskrevet af disse aksiomer. Teorien, defineret på samme måde for heltal i stedet for reelle tal, ifølge Matiyasevichs sætning , er uafgørlig selv for eksistensudsagn for diofantiske ligninger [5] [7] .

Den eksistentielle teori om reelle tal er en delmængde af første-ordens teori og består af udsagn, hvor hver kvantifier er en eksistentiel kvantifier og alle står foran ethvert andet symbol. Det vil sige, at det er et sæt sande udsagn af formen

hvor er en formel uden kvantifikatorer , der indeholder ligheder og uligheder med polynomier over reelle tal . Afgørelighedsproblemet for den eksistentielle teori om reelle tal er det algoritmiske problem med at kontrollere, om en given sætning tilhører denne teori. Tilsvarende gælder det for strenge, der består de grundlæggende syntakstjek (det vil sige, at sætningen bruger de korrekte tegn, har den korrekte syntaks og ingen variable uden kvantifikatorer), er det opgaven at kontrollere, at udsagnet er et sandt udsagn over reelle tal . Sættet af n -tupler af reelle tal , som er sandt, kaldes et semi-algebraisk sæt , så problemet med løselighed for den eksistentielle teori om reelle tal kan tilsvarende omformuleres som at kontrollere, at en given semi-algebraisk mængde ikke er tom [ 1] .

For at bestemme tidskompleksiteten af ​​algoritmer for problemet med løselighed af den eksistentielle teori om reelle tal, er det vigtigt at have en måde at måle størrelsen af ​​input. Den enkleste måde at måle denne type på er længden af ​​sætningen, det vil sige antallet af tegn, der indgår i udsagnet [5] . Men for at få en mere nøjagtig analyse af adfærden af ​​algoritmerne til dette problem, er det praktisk at opdele størrelsen af ​​input i flere variabler, fremhæve antallet af variabler med kvantifier, antallet af polynomier i sætningen, og graderne af disse polynomier [8] .

Eksempler

Det gyldne snit kan defineres som roden af ​​et polynomium . Dette polynomium har to rødder, hvoraf kun én (det gyldne snit) er større end én. Således kan eksistensen af ​​det gyldne snit udtrykkes ved påstanden

Da det gyldne snit eksisterer, er udsagnet sandt og hører til den eksistentielle teori om reelle tal. Svaret på løselighedsproblemet for den eksistentielle teori om reelle tal, givet denne sætning som input, er den boolske værdi sand ( sand ).

Uligheden mellem den aritmetiske middelværdi og den geometriske middelværdi angiver, at for alle to ikke-negative tal og følgende ulighed gælder:

Udsagnet er en førsteordens udsagn over de reelle tal, men den er universel (indeholder ikke eksistentielle kvantifiers) og bruger ekstra symboler for division, kvadratrod og tallet 2, som ikke er tilladt i førsteordensteorien for de reelle tal. Men efter at have kvadreret begge dele, kan sætningen omdannes til følgende eksistentielle udsagn, som kan tolkes som at spørge, om der er et modeksempel til uligheden:

Svaret på løselighedsproblemet for den eksistentielle teori om reelle tal, hvis input er denne ligning, er den boolske værdi falsk ( false ), det vil sige, at der ikke er noget modeksempel. Denne sætning hører således ikke til den eksistentielle teori om reelle tal, selvom den er korrekt fra et grammatisk synspunkt.

Algoritmer

Alfred Tarskis metode til kvantificerende eliminering (1948) viser, at den eksistentielle teori om realerne (og mere generelt førsteordensteorien om realerne) er algoritmisk afgørbar, men uden elementære grænser for kompleksitet [9] [6] . Den cylindriske algebraiske dekomponeringsmetode ifølge Collins (1975) forbedrede tidsafhængigheden af ​​dobbelt eksponentialitet [9] , [10] af formen

hvor er antallet af bits, der kræves for at repræsentere koefficienterne i sætningen, hvis værdi skal bestemmes, er antallet af polynomier i sætningen, er deres fælles grad og er antallet af variable [8] I 1988 , Dmitry Grigoriev og Nikolai Vorobyov viste, at kompleksiteten er eksponentiel, hvor grad er et polynomium i [8] [11] [12] ,

og i en række artikler udgivet i 1992 forbedrede James Renegar estimatet til lidt over på [8] [13] [14] [15] eksponenten .

I mellemtiden beskrev John Canny i 1988 en anden algoritme, der også afhænger eksponentielt i tid, men som kun har polynomiel hukommelseskompleksitet. Det vil sige, at han viste, at problemet kan løses i klassen PSPACE [2] [9] .

Den asymptotiske beregningskompleksitet af disse algoritmer kan være vildledende, da algoritmerne kun kan fungere med meget små inputstørrelser. Ved at sammenligne algoritmerne i 1991 estimerede Hong Hong tiden for Collins-proceduren (med dobbelt eksponentiel evaluering) for et problem, hvis størrelse er beskrevet ved at sætte alle ovenstående parametre til 2 til at være mindre end to sekunder, mens algoritmerne for Grigoriev, Vorobyov og Renegar ville bruge på at løse problemet i mere end en million år [8] . I 1993 foreslog Yos, Roy og Solerno, at det skulle være muligt at ændre de eksponentielle tidsprocedurer lidt for at gøre dem hurtigere i praksis end den cylindriske algebraiske løsning, hvilket ville være i overensstemmelse med teorien [16] . Men fra 2009 er generelle metoder til førsteordensteori for reelle tal stadig de bedste i praksis sammenlignet med algoritmer med simpel eksponentiel evaluering, der er specielt designet til eksistentiel teori om reelle tal [3] .

Fuldfør opgaver

Nogle problemer med beregningsmæssig kompleksitet og geometrisk grafteori kan klassificeres som fuldstændige for den eksistentielle teori om reelle tal. Det vil sige, at ethvert problem fra den eksistentielle teori om reelle tal har en polynomisk flerværdireduktion til en variant af et af disse problemer, og omvendt kan disse problemer reduceres til den eksistentielle teori om reelle tal [4] [17] .

Adskillige problemer af denne type vedrører genkendelsen af ​​skæringsgrafer af en bestemt art. I disse problemer er input en urettet graf . Målet er at afgøre, om det er muligt at associere geometrier af en bestemt klasse med grafens hjørnepunkter på en sådan måde, at to spidser i grafen støder op til hinanden, hvis og kun hvis de tilknyttede geometrier har et ikke-tomt skæringspunkt. Komplet problemer af denne type for den eksistentielle teori om reelle tal omfatter

For grafer tegnet i planen uden skæringspunkter, siger Fareys sætning , at vi får samme klasse af plane grafer , uanset om grafens kanter skal tegnes som linjestykker eller kan tegnes som kurver. Men denne klasseækvivalens er ikke sand for andre typer grafplotning. For eksempel, selvom skæringsnummeret for en graf (det mindste antal skæringspunkter af kanter for krumlinjede kanter) kan defineres som tilhørende klassen NP, er det for den eksistentielle teori om reelle tal problemet med at bestemme, om der er mønstre, hvorpå en givne grænse for det retlinede skæringsnummer (det mindste antal af kantepar, der skærer hinanden i enhver figur med kanter i form af lige linjestykker på planet) er fuldstændig [4] [20] . Det komplette problem for den eksistentielle teori om reelle tal er også problemet med at kontrollere, om en given graf kan tegnes på en plan med segmenter i form af lige kanter og med et givet sæt af par af skærende kanter, eller tilsvarende, om en tegning med buede kanter med skæringer kan rettes op på en sådan måde, at skæringerne bevares [21] .

Andre komplette problemer for den eksistentielle teori om reelle tal:

[31] ;

Ud fra dette defineres kompleksitetsklassen som et sæt af problemer, der har polynomisk tidsreduktion ifølge Karp til den eksistentielle teori om reelle tal [4] .

Noter

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

Litteratur