Valós számok egzisztenciális elmélete

A valós számok egzisztenciális elmélete az alak összes igaz állításának halmaza

ahol egy kvantorok nélküli formula , amely a valós polinomok egyenlőségeit és egyenlőtlenségeit tartalmazza [1] .

A valós számok egzisztenciális elméletének megoldhatósági problémája egy olyan algoritmus megtalálása, amely eldönti, hogy minden képlet igaz-e vagy sem. Ezzel egyenértékűen annak ellenőrzése a probléma, hogy egy adott félalgebrai halmaz nem üres -e [1] . Ez a megoldhatósági probléma NP-nehéz és a PSPACE - ben rejlik [2] . Így a probléma sokkal kevésbé bonyolult, mint az Alfred Tarski-féle kvantorok kiküszöbölésének eljárása az elsőrendű valós elméletekben [1] . A gyakorlatban azonban továbbra is az elsőrendű elmélet általános módszerei maradnak a preferált választás ilyen problémák megoldására [3] .

A geometriai gráfelmélet számos természetes problémája , különösen a geometriai metszetgráfok felismerésének és a metszéspontos gráfok rajzainak éleinek kiegyenesítésének problémái megoldhatók a valós számok egzisztenciális elméletének egy változatára való konvertálásával, és teljesek ehhez az elmélethez. E feladatok leírására egy komplexitási osztályt definiálunk , amely NP és PSPACE között van [4] .

Háttér

A matematikai logikában az "elmélet" olyan formális nyelv , amely rögzített szimbólumkészlettel írt mondatok halmazából áll. A valós zárt mezők elsőrendű elmélete a következő szimbólumokkal rendelkezik [5] :

Ezeknek a szimbólumoknak a sorozata olyan mondatot alkot, amely a valóságok elsőrendű elméletéhez tartozik, ha nyelvtanilag helyes, akkor minden változója rendelkezik megfelelő kvantorral, és (ha a valós értékekre vonatkozó matematikai állításként értelmezzük ) érvényes állítás. Ahogy Tarski megmutatta, ez az elmélet egy axióma sémával és egy olyan döntési eljárással írható le , amely teljes és hatékony, azaz: minden grammatikailag helyes állításhoz kvantorok teljes halmazával, akár maga az állítás, akár annak tagadása (de nem mindkettő) ) az axiómákból levezethető. Ugyanez az elmélet ír le minden valós zárt mezőt , nem csak valós számokat [6] . Vannak azonban más számrendszerek is, amelyeket ezek az axiómák nem írnak le pontosan. A valós számok helyett egész számokra ugyanúgy definiált elmélet Matiyasevics tétele szerint még a diofantinuszi egyenletek [5] [7] létállításaira is eldönthetetlen .

A valós számok egzisztenciális elmélete az elsőrendű elmélet egy részhalmaza, és olyan állításokból áll, amelyekben minden kvantor egzisztenciális kvantor, és mindegyik minden más szimbólum előtt jelenik meg. Vagyis a forma igaz állításainak halmaza

ahol egy kvantorok nélküli képlet , amely valós számok feletti polinomokkal egyenlőségeket és egyenlőtlenségeket tartalmaz . A valós számok egzisztenciális elméletének eldönthetőségi problémája annak az algoritmikus problémája, hogy egy adott mondat ebbe az elméletbe tartozik-e. Azon karakterláncok esetében, amelyek átmennek az alapvető szintaktikai ellenőrzéseken (vagyis a mondat a megfelelő karaktereket használja, a szintaxisa megfelelő, és nincsenek kvantorok nélküli változók), az a feladat, hogy ellenőrizzük, hogy az állítás igaz állítás-e valós számok felett. . A valós számok n -es sorát, amelyre igaz, félalgebrai halmaznak nevezzük , így a valós számok egzisztenciális elméletének megoldhatósági problémája ekvivalensen átfogalmazható úgy, hogy ellenőrizzük, hogy egy adott félalgebrai halmaz nem üres-e . 1] .

A valós számok egzisztenciális elméletének megoldhatósági problémájára az algoritmusok időbonyolultságának meghatározásához fontos, hogy legyen mód a bemenet méretének mérésére. Ennek a típusnak a mérésének legegyszerűbb módja a mondat hossza, vagyis az utasításban szereplő karakterek száma [5] . Azonban a probléma algoritmusainak viselkedésének pontosabb elemzése érdekében célszerű a bemenet méretét több változóra bontani, kvantorokkal kiemelve a változók számát, a mondatban lévő polinomok számát, és ezen polinomok fokszámai [8] .

Példák

Az aranymetszés egy polinom gyökeként definiálható . Ennek a polinomnak két gyöke van, amelyek közül csak az egyik (az aranymetszés) nagyobb egynél. Így az aranymetszés megléte kifejezhető a tétellel

Mivel az aranymetszés létezik, az állítás igaz, és a valós számok egzisztenciális elméletéhez tartozik. A válasz a valós számok egzisztenciális elméletének megoldhatósági problémájára, ha ezt a mondatot adjuk meg bemenetként, az igaz ( igaz ) logikai érték.

A számtani és a geometriai átlag közötti egyenlőtlenség kimondja, hogy bármely két nemnegatív számra és a következő egyenlőtlenség teljesül:

Az állítás egy elsőrendű állítás a valós számok felett, de univerzális (nem tartalmaz egzisztenciális kvantorokat), és extra szimbólumokat használ az osztáshoz, a négyzetgyökhöz és a 2-es számhoz, amelyek nem megengedettek az elsőrendű elméletben. a valós számokat. Azonban mindkét rész négyzetre emelése után a mondat a következő egzisztenciális kijelentéssé alakítható, amely úgy értelmezhető, hogy megkérdezi, van-e ellenpélda az egyenlőtlenségre:

A valós számok egzisztenciális elméletének megoldhatósági problémájára, amelynek bemenete ez az egyenlet, a válasz a logikai érték false ( false ), vagyis nincs ellenpélda. Ez a mondat tehát nem tartozik a valós számok egzisztenciális elméletébe, bár nyelvtani szempontból helyes.

Algoritmusok

Alfred Tarski kvantor eliminációs módszere (1948) azt mutatja, hogy a valóságok egzisztenciális elmélete (és általánosabban a valóságok elsőrendű elmélete) algoritmikusan eldönthető, de a komplexitás elemi korlátai nélkül [9] [6] . Collins (1975 ) hengeralgebrai dekompozíciós módszere az időfüggést az alak kétszeres exponencialitásáig javította [9] , [10]

ahol az a bitek száma, amelyek az együtthatók megjelenítéséhez szükségesek a meghatározandó utasításban, a polinomok száma az utasításban, ezek közös foka és a változók száma [8] 1988 -ban Dmitry Grigoriev és Nyikolaj Vorobjov megmutatta, hogy a komplexitás exponenciális, ha a fok polinomiális [8] [11] [12] ,

és egy sor tanulmányban, amelyet 1992-ben publikáltak, James Renegar valamivel a [8] [13] [14] [15] kitevő fölé javította a becslést .

Eközben 1988-ban John Canny egy másik algoritmust írt le, amely szintén exponenciálisan függ az időtől, de csak polinomiális memóriabonyolultságú. Vagyis megmutatta, hogy a probléma a PSPACE [2] [9] osztályban megoldható .

Ezen algoritmusok aszimptotikus számítási bonyolultsága félrevezető lehet, mivel az algoritmusok csak nagyon kis bemeneti méretekkel működnek. Hong Hong 1991-ben az algoritmusokat összehasonlítva megbecsülte a Collins-eljárás idejét (kettős exponenciális kiértékeléssel) egy olyan probléma esetében, amelynek méretét úgy írják le, hogy az összes fenti paramétert 2-re állítva két másodpercnél kisebbre, míg Grigorjev, Vorobjov algoritmusai és Renegar több mint egymillió évig költene a probléma megoldására [8] . 1993-ban Yos, Roy és Solerno azt javasolta, hogy lehetővé kell tenni az exponenciális idő eljárások kismértékű módosítását, hogy a gyakorlatban gyorsabbak legyenek, mint a hengeralgebrai megoldás, ami összhangban állna az elmélettel [16] . 2009-től azonban a valós számok elsőrendű elméletének általános módszerei továbbra is a legjobbak a gyakorlatban az egyszerű exponenciális kiértékelésű algoritmusokhoz képest, amelyeket kifejezetten a valós számok egzisztenciális elméletéhez terveztek [3] .

Feladatok teljesítése

A számítási bonyolultság és a geometriai gráfelmélet egyes problémái teljes kategóriába sorolhatók a valós számok egzisztenciális elméletéhez. Ez azt jelenti, hogy a valós számok egzisztenciális elméletéből származó bármely probléma polinomiális többértékű redukcióval rendelkezik e problémák egyik változatára, és fordítva, ezek a problémák visszavezethetők a valós számok egzisztenciális elméletére [4] [17] .

Számos ilyen típusú probléma egy bizonyos típusú metszés gráfok felismerésével kapcsolatos. Ezekben a problémákban a bemenet egy irányítatlan gráf . A cél annak meghatározása, hogy lehetséges-e egy adott osztály geometriáit a gráf csúcsaihoz úgy társítani, hogy a gráf két csúcsa akkor és csak akkor legyen szomszédos, ha a társított geometriáknak van egy nem üres metszéspontja. A valós számok egzisztenciális elméletének ilyen típusú teljes problémái közé tartozik

A metszéspontok nélküli síkban rajzolt gráfok esetében a Farey- tétel kimondja, hogy a síkgráfok ugyanazt az osztályát kapjuk , függetlenül attól, hogy a gráf éleit vonalszakaszként vagy görbeként kell megrajzolni. Ez az osztályekvivalencia azonban nem igaz a gráfábrázolás más típusaira. Például, bár egy gráf metszéspontszáma (az élek metszéspontjainak minimális száma görbe vonalú éleknél) definiálható az NP osztályba tartozóként, a valós számok egzisztenciális elmélete esetében felmerül a probléma annak meghatározása, hogy vannak-e olyan minták, amelyeken az egyenes vonalú metszésszám adott határa (az élpárok minimális száma, amelyek bármely ábrán a síkon egyenes szakaszok formájában metszik élekkel) teljes [4] [20] . A valós számok egzisztenciális elméletének teljes problémája annak ellenőrzése is, hogy egy adott gráf megrajzolható-e egy síkon egyenes élek formájú szegmensekkel és adott metsző élpárokkal, vagy ezzel egyenértékűen, hogy a metszéspontokkal ívelt élekkel rendelkező rajz úgy kiegyenesíthető, hogy a metszéspontok megmaradnak [21] .

További teljes problémák a valós számok egzisztenciális elméletéhez:

[31] ;

Ennek alapján a komplexitási osztályt olyan problémák halmazaként definiáljuk, amelyek polinomiális időcsökkentéssel rendelkeznek Karp szerint a valós számok egzisztenciális elméletéhez [4] .

Jegyzetek

  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. ↑ 1948, Tarski 12 .
  7. ↑ Matiyasevics, 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. ↑ Grigorjev, 1988 , p. 65–108.
  12. ↑ Grigorjev, 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 és 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 .

Irodalom