Existentiell teori om reella tal

Den existentiella teorin om reella tal är mängden av alla sanna påståenden i formen

där är en formel utan kvantifierare , som inkluderar likheter och olikheter för reella polynom [1] .

Lösbarhetsproblemet för den existentiella teorin om reella tal är problemet med att hitta en algoritm som avgör för varje formel om den är sann eller inte. På motsvarande sätt är detta problemet med att kontrollera att en given semi-algebraisk mängd inte är tom [1] . Detta lösbarhetsproblem är NP-hårt och ligger i PSPACE [2] . Problemet är alltså mycket mindre komplext än proceduren för att eliminera Alfred Tarskis kvantifierare i första ordningens verkliga teorier [1] . Men i praktiken är generella metoder för första ordningens teori fortfarande det föredragna valet för att lösa sådana problem [3] .

Många naturliga problem med geometrisk grafteori , särskilt problem med igenkänning av geometriska skärningsdiagram och uträtning av kanter på ritningar av grafer med skärningspunkter , kan lösas genom att konvertera dem till en variant av den existentiella teorin om reella tal och är kompletta för denna teori. För att beskriva dessa uppgifter definieras en komplexitetsklass , som är mellan NP och PSPACE [4] .

Bakgrund

I matematisk logik är en "teori" ett formellt språk som består av en uppsättning meningar skrivna med en fast uppsättning symboler. Den första ordningens teori om verkliga slutna fält har följande symboler [5] :

Sekvensen av dessa symboler bildar en mening som tillhör teorin om den första ordningen av reals, om grammatiskt korrekt, alla dess variabler har lämpliga kvantifierare, och (när det tolkas som ett matematiskt påstående om reals ) är ett giltigt påstående. Som Tarski har visat kan denna teori beskrivas med ett axiomschema och en beslutsprocedur som är fullständig och effektiv, det vill säga: för varje grammatiskt korrekt påstående med en full uppsättning kvantifierare, antingen själva påståendet eller dess negation (men inte båda ) kan härledas från axiomen. Samma teori beskriver alla reella stängda fält , inte bara reella tal [6] . Det finns dock andra talsystem som inte exakt beskrivs av dessa axiom. Teorin, definierad på samma sätt för heltal istället för reella tal, enligt Matiyasevichs teorem , är oavgjord även för existensuttalanden för diofantiska ekvationer [5] [7] .

Den existentiella teorin om reella tal är en delmängd av första ordningens teori och består av påståenden där varje kvantifierare är en existentiell kvantifierare och alla förekommer före alla andra symboler. Det vill säga, det är en uppsättning sanna påståenden av formen

där är en formel utan kvantifierare som innehåller likheter och olikheter med polynom över reella tal . Beslutbarhetsproblemet för den existentiella teorin om reella tal är det algoritmiska problemet att kontrollera om en given mening tillhör denna teori. På motsvarande sätt, för strängar som klarar de grundläggande syntaxkontrollerna (det vill säga meningen använder rätt tecken, har rätt syntax och har inga variabler utan kvantifierare), är det uppgiften att kontrollera att påståendet är ett sant påstående över reella tal . Mängden av n -tuplar av reella tal som är sanna kallas en semi-algebraisk mängd , så problemet med lösbarheten för den existentiella teorin om reella tal kan på motsvarande sätt omformuleras som att kontrollera att en given semi-algebraisk mängd inte är tom [ 1] .

För att bestämma tidskomplexiteten hos algoritmer för problemet med lösbarhet av den existentiella teorin om reella tal, är det viktigt att ha ett sätt att mäta storleken på inmatningen. Det enklaste sättet att mäta denna typ är längden på meningen, det vill säga antalet tecken som ingår i påståendet [5] . Men för att få en mer exakt analys av beteendet hos algoritmerna för detta problem är det bekvämt att dela upp storleken på inmatningen i flera variabler, markera antalet variabler med kvantifierare, antalet polynom i meningen, och graderna av dessa polynom [8] .

Exempel

Det gyllene snittet kan definieras som roten till ett polynom . Detta polynom har två rötter, varav endast en (det gyllene snittet) är större än en. Således kan förekomsten av det gyllene snittet uttryckas genom propositionen

Eftersom det gyllene snittet existerar är påståendet sant och tillhör den existentiella teorin om reella tal. Svaret på lösbarhetsproblemet för den existentiella teorin om reella tal, givet denna mening som indata, är det booleska värdet true ( true ).

Olikheten mellan det aritmetiska medelvärdet och det geometriska medelvärdet anger att för två icke-negativa tal och följande olikhet gäller:

Påståendet är ett första ordningens uttalande över de reella talen, men det är universellt (innehåller inte existentiella kvantifierare) och använder extra symboler för division, kvadratrot och talet 2, som inte är tillåtna i första ordningens teori om de verkliga siffrorna. Men efter att ha kvadrerat båda delarna kan meningen omvandlas till följande existentiella påstående, vilket kan tolkas som att man frågar om det finns ett motexempel till ojämlikheten:

Svaret på lösbarhetsproblemet för den existentiella teorin om reella tal, vars indata är denna ekvation, är det booleska värdet false ( false ), det vill säga det finns inget motexempel. Den här meningen tillhör alltså inte den existentiella teorin om reella tal, även om den är korrekt ur grammatiksynpunkt.

Algoritmer

Alfred Tarskis metod för eliminering av kvantifierare (1948) visar att den existentiella teorin om de verkliga (och mer allmänt första ordningens teori om de verkliga) är algoritmiskt avgörbar, men utan elementära gränser för komplexitet [9] [6] . Den cylindriska algebraiska nedbrytningsmetoden enligt Collins (1975) förbättrade tidsberoendet av dubbel exponentialitet [9] , [10] av formen

där är antalet bitar som krävs för att representera koefficienterna i påståendet vars värde ska bestämmas, är antalet polynom i påståendet, är deras vanliga grad och är antalet variabler [8] 1988 , Dmitry Grigoriev och Nikolai Vorobyov visade att komplexiteten är exponentiell med grad som ett polynom i [8] [11] [12] ,

och i en serie artiklar publicerade 1992 förbättrade James Renegar uppskattningen till något över exponenten på [8] [13] [14] [15] .

Under tiden beskrev John Canny 1988 en annan algoritm som också beror exponentiellt i tiden, men som bara har polynomminneskomplexitet Det vill säga, han visade att problemet kan lösas i klassen PSPACE [2] [9] .

Den asymptotiska beräkningskomplexiteten för dessa algoritmer kan vara missvisande, eftersom algoritmerna endast kan fungera med mycket små indatastorlekar. Genom att jämföra algoritmerna 1991 uppskattade Hong Hong tiden för Collins-proceduren (med dubbel exponentiell utvärdering) för ett problem vars storlek beskrivs genom att sätta alla ovanstående parametrar till 2 för att vara mindre än två sekunder, medan Grigoriev, Vorobyovs algoritmer och Renegar skulle spendera för att lösa problemet i mer än en miljon år [8] . 1993 föreslog Yos, Roy och Solerno att det borde vara möjligt att något modifiera de exponentiella tidsprocedurerna för att göra dem snabbare i praktiken än den cylindriska algebraiska lösningen, vilket skulle stämma överens med teorin [16] . Men från och med 2009 är generella metoder för första ordningens teori om reella tal fortfarande de bästa i praktiken jämfört med algoritmer med enkel exponentiell utvärdering speciellt utformad för existentiell teori om reella tal [3] .

Slutför uppgifter

Vissa problem med beräkningskomplexitet och geometrisk grafteori kan klassificeras som kompletta för den existentiella teorin om reella tal. Det vill säga, alla problem från den existentiella teorin om reella tal har en polynom flervärdig reduktion till en variant av ett av dessa problem och omvänt är dessa problem reducerbara till den existentiella teorin om reella tal [4] [17] .

Flera problem av denna typ rör igenkänningen av skärningsdiagram av ett visst slag. I dessa problem är ingången en oriktad graf . Målet är att avgöra om det är möjligt att associera geometrier av en viss klass med grafens hörn på ett sådant sätt att två hörn i grafen ligger intill om och endast om de associerade geometrierna har en icke-tom skärningspunkt. Kompletta problem av denna typ för den existentiella teorin om reella tal inkluderar

För grafer ritade i planet utan skärningspunkter säger Fareys sats att vi får samma klass av plana grafer oavsett om grafens kanter måste ritas som linjesegment eller kan ritas som kurvor. Men denna klassekvivalens är inte sant för andra typer av grafritning. Till exempel, även om skärningsnumret för en graf (minsta antalet skärningspunkter av kanter för kurvlinjära kanter) kan definieras som tillhörande klassen NP, för den existentiella teorin om reella tal problemet med att avgöra om det finns mönster på vilka en given gräns för det rätlinjiga skärningsnumret (det minsta antalet par av kanter som skär i någon figur med kanter i form av räta linjesegment på planet) är komplett [4] [20] . Det fullständiga problemet för den existentiella teorin om reella tal är också problemet med att kontrollera om en given graf kan ritas på ett plan med segment i form av raka kanter och med en given uppsättning par av skärande kanter, eller, ekvivalent, om en ritning med krökta kanter med korsningar kan rätas ut på ett sådant sätt att korsningarna bevaras [21] .

Andra kompletta problem för den existentiella teorin om reella tal:

[31] ;

Utifrån detta definieras komplexitetsklassen som en uppsättning problem som har polynom tidsreduktion enligt Karp till den existentiella teorin om reella tal [4] .

Anteckningar

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

Litteratur