Reaalilukujen eksistentiaalinen teoria

Reaalilukujen eksistentiaaliteoria on kaikkien muodon tosilausekkeiden joukko

missä on kaava ilman kvantaajia [ , joka sisältää reaalipolynomien yhtäläisyydet ja epäyhtälöt [1] .

Reaalilukujen eksistentiaalisen teorian ratkaistavuusongelma on algoritmin löytäminen, joka päättää kunkin kaavan kohdalla, onko se totta vai ei. Vastaavasti tämä on ongelma sen tarkistamisessa, että tietty puolialgebrallinen joukko ei ole tyhjä [1] . Tämä ratkaistavuusongelma on NP-kova ja sijaitsee PSPACE :ssä [2] . Siten ongelma on paljon vähemmän monimutkainen kuin menetelmä Alfred Tarskin kvantorien eliminoimiseksi ensimmäisen asteen reaaliteorioissa [1] . Käytännössä yleiset menetelmät ensimmäisen asteen teorialle ovat kuitenkin suositeltavin vaihtoehto tällaisten ongelmien ratkaisemiseksi [3] .

Monet geometrisen graafiteorian luonnolliset ongelmat , erityisesti geometristen leikkauskaavioiden tunnistamiseen ja leikkauspisteitä sisältävien kaavioiden piirustusten reunojen suoristukseen liittyvät ongelmat , voidaan ratkaista muuntamalla ne reaalilukujen eksistentiaalisen teorian muunnelmaksi ja ovat täydellisiä tälle teorialle. Näiden tehtävien kuvaamiseksi määritellään kompleksisuusluokka , joka on NP :n ja PSPACE :n välillä [4] .

Tausta

Matemaattisessa logiikassa "teoria" on muodollinen kieli , joka koostuu joukosta lauseita , jotka on kirjoitettu käyttämällä kiinteää symbolijoukkoa. Ensimmäisen asteen todellisten suljettujen kenttien teoriassa on seuraavat symbolit [5] :

Näiden symbolien sekvenssi muodostaa lauseen, joka kuuluu reaalien ensimmäisen kertaluvun teoriaan. Jos se on kieliopillisesti oikein, sen kaikilla muuttujilla on sopivat kvantisoijat, ja (kun se tulkitaan matemaattiseksi väittämäksi realiteeteista ) on pätevä lausunto. Kuten Tarski on osoittanut, tätä teoriaa voidaan kuvata aksioomaskeemalla ja päätösmenettelyllä, joka on täydellinen ja tehokas, toisin sanoen: jokaiselle kieliopillisesti oikealle lauseelle, jossa on täysi joukko kvantiaattoreita, joko itse lause tai sen negatiivinen lause (mutta ei molempia). ) voidaan päätellä aksioomista. Sama teoria kuvaa mitä tahansa todellista suljettua kenttää , ei vain reaalilukuja [6] . On kuitenkin muita lukujärjestelmiä, joita nämä aksioomit eivät tarkasti kuvaile. Teoria, joka on määritelty samalla tavalla kokonaisluvuille todellisten lukujen sijaan, Matiyasevichin lauseen mukaan , on ratkaisematon edes diofantiiniyhtälöiden olemassaololausekkeille [5] [7] .

Reaalilukujen eksistentiaalinen teoria on ensimmäisen kertaluvun teorian osajoukko ja se koostuu lauseista, joissa jokainen kvantori on eksistentiaalinen kvantori ja kaikki esiintyvät ennen muita symboleja. Toisin sanoen se on joukko muodon oikeita lausuntoja

jossa on kaava ilman kvantaajia , joka sisältää yhtäläisyydet ja epäyhtälöt polynomien kanssa reaalilukujen yli . Reaalilukujen eksistentiaalisen teorian ratkeavuusongelma on algoritminen ongelma tarkistaa, kuuluuko tietty lause tähän teoriaan. Vastaavasti merkkijonojen, jotka läpäisevät perussyntaksin tarkistukset (eli lauseessa käytetään oikeita merkkejä, on oikea syntaksi ja siinä ei ole muuttujia ilman kvantoreita), on tarkistettava, että lause on tosi lauseke reaalilukujen suhteen. . Reaalilukujen n -sarjan joukkoa , jolle on totta, kutsutaan puolialgebralliseksi joukoksi , joten reaalilukujen eksistentiaalisen teorian ratkaistavuusongelma voidaan vastaavasti muotoilla uudelleen tarkastettavaksi, että tietty puolialgebrallinen joukko ei ole tyhjä [ 1] .

Reaalilukujen eksistentiaalisen teorian ratkaistavuusongelman algoritmien aikamonimutkaisuuden määrittämiseksi on tärkeää, että on olemassa tapa mitata syötteen koko . Yksinkertaisin tapa mitata tämä tyyppi on lauseen pituus eli lauseeseen sisältyvien merkkien määrä [5] . Jotta tämän ongelman algoritmien käyttäytymisestä saataisiin tarkempi analyysi, on kuitenkin kätevää jakaa syötteen koko useiksi muuttujiksi korostamalla muuttujien lukumäärää kvantaaleilla, lauseen polynomien lukumäärää, ja näiden polynomien asteet [8] .

Esimerkkejä

Kultainen suhde voidaan määritellä polynomin juureksi . Tällä polynomilla on kaksi juuria, joista vain yksi (kultainen suhde) on suurempi kuin yksi. Siten kultaisen leikkauksen olemassaolo voidaan ilmaista lauseella

Koska kultainen suhde on olemassa, väite on tosi ja kuuluu reaalilukujen eksistentiaaliseen teoriaan. Vastaus reaalilukujen eksistentiaalisen teorian ratkaistavuusongelmaan, kun tämä lause syötetään, on Boolen arvo tosi ( tosi ).

Aritmeettisen keskiarvon ja geometrisen keskiarvon välinen epäyhtälö tarkoittaa , että kahdelle ei-negatiiviselle luvulle pätee seuraava epäyhtälö :

Lause on ensimmäisen asteen lause reaalilukujen yli, mutta se on universaali (ei sisällä eksistentiaalisia kvantoreita) ja käyttää ylimääräisiä symboleja jakolaskulle, neliöjuurelle ja luvulle 2, jotka eivät ole sallittuja ensimmäisen kertaluvun teoriassa. todelliset luvut. Molempien osien neliöinnin jälkeen lause voidaan kuitenkin muuntaa seuraavaksi eksistentiaaliseksi väittämäksi, joka voidaan tulkita kysyväksi, onko epätasa-arvolle vastaesimerkkiä:

Reaalilukujen eksistentiaalisen teorian, jonka syöte on tämä yhtälö, ratkaistavuusongelman vastaus on Boolen arvo false ( false ), eli vastaesimerkkiä ei ole. Tämä lause ei siis kuulu reaalilukujen eksistentiaaliseen teoriaan, vaikka se onkin oikein kieliopin näkökulmasta.

Algoritmit

Alfred Tarskin kvantorieliminaatiomenetelmä ( 1948 ) osoittaa, että todellisuuksien eksistentiaalinen teoria (ja yleisemmin reaalien ensimmäisen asteen teoria) on algoritmisesti päätettävissä, mutta ilman alkeellisia kompleksisuuden rajoja [9] [6] . Collinsin (1975 ) sylinterialgebrallinen hajottelumenetelmä paransi aikariippuvuutta muodon kaksinkertaiseen eksponentiaalisuuteen [9] , [10] .

missä on bittien määrä, joka vaaditaan kertoimien esittämiseen lauseessa, jonka arvo on määritettävä, on lausekkeen polynomien lukumäärä, on niiden yhteinen aste ja on muuttujien lukumäärä [8] Vuonna 1988 Dmitry Grigoriev ja Nikolai Vorobjov osoittivat, että monimutkaisuus on eksponentiaalinen, kun aste on polynomi [8] [11] [12] ,

ja vuonna 1992 julkaistuissa artikkeleissa James Renegar paransi arviota hieman [ 8] [13] [14] [15] eksponentin yläpuolelle .

Sillä välin vuonna 1988 John Canny kuvasi toisen algoritmin, joka myös riippuu eksponentiaalisesti ajasta, mutta jolla on vain polynomimuistin monimutkaisuus. Eli hän osoitti, että ongelma voidaan ratkaista luokassa PSPACE [2] [9] .

Näiden algoritmien asymptoottinen laskennallinen monimutkaisuus voi olla harhaanjohtava, koska algoritmit voivat toimia vain hyvin pienillä syötteillä. Vertailemalla algoritmeja vuonna 1991 Hong Hong arvioi Collins-proseduurin ajan (kaksinkertaisella eksponentiaalisella arvioinnilla) ongelmalle, jonka koko kuvataan asettamalla kaikki yllä olevat parametrit 2:ksi alle kahden sekunnin ajaksi, kun taas Grigorjevin ja Vorobjovin algoritmit ja Renegar käyttäisi ongelman ratkaisemiseen yli miljoona vuotta [8] . Vuonna 1993 Yos, Roy ja Solerno ehdottivat, että eksponentiaalisen aikaproseduurin pitäisi olla mahdollista muuttaa hieman, jotta ne olisivat käytännössä nopeampia kuin sylinterialgebrallinen ratkaisu, mikä olisi teorian mukaista [16] . Vuodesta 2009 lähtien reaalilukujen ensimmäisen asteen teorian yleiset menetelmät ovat kuitenkin edelleen parhaita käytännössä verrattuna algoritmeihin, joissa on yksinkertainen eksponentiaalinen arviointi, jotka on suunniteltu erityisesti reaalilukujen eksistentiaaliseen teoriaan [3] .

Suorita tehtävät

Jotkut laskennallisen monimutkaisuuden ja geometrisen graafiteorian ongelmat voidaan luokitella täydelliseksi reaalilukujen eksistentiaalisen teorian osalta. Toisin sanoen millä tahansa reaalilukujen eksistentiaalisen teorian ongelmalla on polynominen moniarvoinen pelkistys yhden näistä tehtävistä muunnelmaksi, ja päinvastoin nämä ongelmat ovat redusoitavissa reaalilukujen eksistentiaaliseen teoriaan [4] [17] .

Useat tämän tyyppiset ongelmat liittyvät tietyntyyppisten leikkauskaavioiden tunnistamiseen . Näissä tehtävissä syöte on suuntaamaton graafi . Tavoitteena on selvittää, onko mahdollista liittää tietyn luokan geometrioita graafin kärkipisteisiin siten, että kaksi graafin kärkeä ovat vierekkäin silloin ja vain, jos niihin liittyvillä geometrioilla on ei-tyhjä leikkauspiste. Reaalilukujen eksistentiaalisen teorian tämän tyyppisiä täydellisiä ongelmia ovat mm

Tasoon piirretyille graafeille, joissa ei ole leikkauspisteitä, Fareyn lause sanoo, että saamme saman luokan tasograafit riippumatta siitä, pitääkö graafin reunat piirtää janaina vai voidaanko ne piirtää käyrinä. Mutta tämä luokkaekvivalenssi ei pidä paikkaansa muun tyyppisissä graafin piirtämisessä. Esimerkiksi vaikka graafin leikkausnumero (kaarevareunojen reunojen leikkauspisteiden vähimmäismäärä) voidaan määritellä kuuluvaksi luokkaan NP, reaalilukujen eksistentiaalisen teorian ongelmana on määrittää, onko olemassa kuvioita, joissa annettu suoraviivaisen leikkausluvun raja (vähimmäismäärä reunapareja, jotka leikkaavat missä tahansa kuviossa reunojen kanssa suorien viivaosien muodossa tasossa) on täydellinen [4] [20] . Reaalilukujen eksistentiaalisen teorian täydellinen ongelma on myös sen tarkastaminen, voidaanko tietty graafi piirtää tasolle, jossa on suorien reunojen muodossa olevia segmenttejä ja tietyllä joukolla leikkaavia reunapareja, tai vastaavasti, voidaanko kaarevien reunojen ja leikkauspisteiden piirros voidaan oikaista siten, että leikkauskohdat säilyvät [21] .

Muita täydellisiä ongelmia reaalilukujen eksistentiaaliselle teorialle:

[31] ;

Tämän perusteella monimutkaisuusluokka määritellään joukoksi ongelmia, joilla on polynomiaikainen aikavähennys Karpin mukaan reaalilukujen eksistentiaaliseen teoriaan [4] .

Muistiinpanot

  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 Schaefer, 2010 , s. 334-344.
  5. ↑ 1 2 3 4 Matousek, 2014 .
  6. ↑ 12 Tarski , 1948 .
  7. ↑ Matiyasevitš, 2006 , s. 185–213.
  8. ↑ 1 2 3 4 5 Hong, 1991 .
  9. ↑ 1 2 3 4 Schaefer, 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 ja 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 .

Kirjallisuus