Экзистенциальная теория реальности - Existential theory of the reals

В математическая логика, теория сложности вычислений, и Информатика, то экзистенциальная теория реальности это множество всех истинных предложений формы

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

где ${\displaystyle F(X_{1},\dots X_{n})}$ это бескванторная формула включая равенство и неравенство настоящий многочлены.^[1]

В проблема решения для экзистенциальной теории реальности - это проблема нахождения алгоритм это решает для каждой такой формулы, истинна она или ложь. В равной степени это проблема проверки того, полуалгебраическое множество не пусто.^[1] Эта проблема решения NP-жесткий и лежит в PSPACE.^[2] Таким образом, он имеет значительно меньшую сложность, чем Альфред Тарский с исключение квантора порядок принятия решений в теория действительных чисел первого порядка без ограничения экзистенциальными кванторами.^[1] Однако на практике общие методы теории первого порядка остаются предпочтительным выбором для решения этих проблем.^[3]

Многие естественные проблемы в геометрическая теория графов, особенно проблемы распознавания геометрических графы пересечений и выпрямляя края графические рисунки с участием переходы, могут быть решены путем перевода их в примеры экзистенциальной теории реальности и являются полный для этой теории. В класс сложности ${\displaystyle \exists \mathbb {R} }$, который находится между НП и PSPACE, был определен для описания этого класса проблем.^[4]

Задний план

В математическая логика, а теория это формальный язык состоящий из набора фразы написано с использованием фиксированного набора символов. В теория первого порядка реальных замкнутых полей имеет следующие символы:^[5]

• постоянные 0 и 1,
• счетный набор переменных ${\displaystyle X_{i}}$,
• операции сложения, вычитания, умножения и (необязательно) деления,
• символы <, ≤, =, ≥,> и ≠ для сравнения реальных значений,
• то логические связки ∧, ∨, ¬ и ⇔,
• круглые скобки и
• то универсальный квантор ∀ и экзистенциальный квантор ∃

Последовательность этих символов образует предложение, которое принадлежит теории действительных чисел первого порядка, если оно грамматически правильно сформировано, все его переменные правильно определены количественно и (при интерпретации как математическое утверждение о действительные числа ) это верное утверждение. Как показал Тарский, эту теорию можно описать схема аксиомы и процедура принятия решения, которая является полной и эффективной: для каждого полностью количественно выраженного и грамматического предложения либо предложение, либо его отрицание (но не оба сразу) могут быть выведены из аксиом. Та же теория описывает все настоящее закрытое поле а не только реальные числа.^[6] Однако есть и другие системы счисления, которые неточно описываются этими аксиомами; в частности, теория, определенная таким же образом для целые числа вместо реальных чисел неразрешимый, даже для экзистенциальных предложений (Диофантовы уравнения ) от Теорема Матиясевича.^[5][7]

Экзистенциальная теория действительных чисел - это подмножество теории первого порядка, состоящее из предложений, в которых все кванторы экзистенциальны и появляются перед любыми другими символами. То есть это совокупность всех истинных предложений формы

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

где ${\displaystyle F(X_{1},\dots X_{n})}$ это бескванторная формула включая равенство и неравенство настоящий многочлены. В проблема решения для экзистенциальной теории действительного - это алгоритмическая проблема проверки того, принадлежит ли данное предложение этой теории; эквивалентным образом, для строк, которые проходят базовую синтаксическую проверку (в них используются правильные символы с правильным синтаксисом и отсутствуют неквантованные переменные), проблема заключается в проверке того, является ли предложение истинным утверждением о действительных числах. Набор п-наборы действительных чисел ${\displaystyle (X_{1},\dots X_{n})}$ для которого ${\displaystyle F(X_{1},\dots X_{n})}$ правда называется полуалгебраическое множество, поэтому проблема решения для экзистенциальной теории вещественных чисел может быть эквивалентно перефразирована как проверка того, непусто ли данное полуалгебраическое множество.^[1]

При определении временная сложность из алгоритмы для решения проблемы экзистенциальной теории вещественных чисел важно иметь меру размера входных данных. Самая простая мера этого типа - длина предложения, то есть количество содержащихся в нем символов.^[5] Однако, чтобы добиться более точного анализа поведения алгоритмов для этой проблемы, удобно разбить размер входных данных на несколько переменных, выделив количество переменных для количественной оценки, количество многочленов в предложении, и степень этих многочленов.^[8]

Примеры

В Золотое сечение ${\displaystyle \varphi }$ можно определить как корень из многочлен ${\displaystyle x^{2}-x-1}$. Этот многочлен имеет два корня, только один из которых (золотое сечение) больше единицы. Таким образом, существование золотого сечения можно выразить предложением

${\displaystyle \exists X_{1}(X_{1}>1\wedge X_{1}\times X_{1}-X_{1}-1=0).}$

Поскольку золотое сечение действительно существует, это верное предложение, относящееся к экзистенциальной теории действительных чисел. Ответом на проблему принятия решения для экзистенциальной теории вещественных чисел, учитывая это предложение в качестве входных данных, является логическое значение true.

В неравенство средних арифметических и геометрических утверждает, что для каждых двух неотрицательных чисел ${\displaystyle x}$ и ${\displaystyle y}$, имеет место неравенство

${\displaystyle {\frac {x+y}{2}}\geq {\sqrt {xy}}.}$

Как указано выше, это предложение первого порядка о действительных числах, но одно с универсальными, а не экзистенциальными кванторами, и другое, в котором используются дополнительные символы для деления, квадратные корни и число 2, которые недопустимы в первом порядке. теория действительного. Однако, возведя в квадрат обе стороны, его можно преобразовать в следующее экзистенциальное утверждение, которое можно интерпретировать как вопрос, есть ли у неравенства какие-либо контрпримеры:

${\displaystyle \exists X_{1}\exists X_{2}{\bigl (}X_{1}\geq 0\wedge X_{2}\geq 0\wedge (X_{1}+X_{2})\times (X_{1}+X_{2})<(X_{1}+X_{1})\times (X_{2}+X_{2}){\bigr )}.}$

Ответом на проблему принятия решения для экзистенциальной теории вещественных чисел, учитывая это предложение в качестве входных данных, является логическое значение false: нет никаких контрпримеров. Следовательно, это предложение не принадлежит экзистенциальной теории действительных чисел, несмотря на то, что оно имеет правильную грамматическую форму.

Алгоритмы

Альфред Тарский метод исключение квантора (1948) показал, что экзистенциальная теория действительных чисел (и в более общем плане теория реальных чисел первого порядка) алгоритмически разрешима, но без элементарный связано с его сложностью.^[9][6] Методика цилиндрическое алгебраическое разложение, от Джордж Э. Коллинз (1975) улучшили временную зависимость до дважды экспоненциальный,^[9][10] формы

${\displaystyle L^{3}(md)^{2^{O(n)}}}$

где ${\displaystyle L}$ это количество битов, необходимых для представления коэффициентов в предложении, значение которых необходимо определить, ${\displaystyle m}$ это количество многочленов в предложении, ${\displaystyle d}$ их общая степень, и ${\displaystyle n}$ - количество переменных.^[8]К 1988 г. Дима Григорьев и Николай Воробьев показал, что сложность экспоненциальна от многочлена от ${\displaystyle n}$,^[8][11][12]

${\displaystyle L(md)^{n^{2}}}$

и в серии статей, опубликованных в 1992 г., Джеймс Ренегар улучшил эту зависимость до однократно экспоненциальной зависимости на ${\displaystyle n}$,^{[8][13][14][15]}

${\displaystyle L\log L\log \log L(md)^{O(n)}.}$

Между тем, в 1988 г. Джон Кэнни описал другой алгоритм, который также имеет экспоненциальную зависимость от времени, но имеет только полиномиальную пространственную сложность; то есть он показал, что проблема может быть решена в PSPACE.^[2][9]

В асимптотическая вычислительная сложность Эти алгоритмы могут вводить в заблуждение, потому что на практике они могут выполняться только на входах очень маленького размера. В сравнении 1991 года Хун Хонг оценил, что дважды экспоненциальная процедура Коллинза могла бы решить проблему, размер которой описывается установкой всех вышеупомянутых параметров на 2 менее чем за секунду, тогда как алгоритмы Григорьева, Ворбьева и Ренегара вместо этого потребовалось бы больше миллиона лет.^[8] В 1993 году Джоос, Рой и Солерно предположили, что должна быть возможность внести небольшие изменения в процедуры экспоненциального времени, чтобы сделать их быстрее на практике, чем цилиндрическое алгебраическое решение, а также быстрее в теории.^[16] Однако по состоянию на 2009 год общие методы теории действительных чисел первого порядка на практике превосходили одноэкспоненциальные алгоритмы, специализированные для экзистенциальной теории вещественных чисел.^[3]

Полные проблемы

Несколько проблем в вычислительной сложности и геометрическая теория графов можно классифицировать как полный для экзистенциальной теории реальности. То есть, каждая проблема в экзистенциальной теории реальности имеет редукция "много-один" за полиномиальное время к примеру одной из этих проблем, а эти проблемы, в свою очередь, сводятся к экзистенциальной теории действительного.^[4][17]

Ряд проблем этого типа касается распознавания графы пересечений определенного типа. В этих задачах входом является неориентированный граф; цель состоит в том, чтобы определить, могут ли геометрические фигуры из определенного класса фигур быть связаны с вершинами графа таким образом, чтобы две вершины были смежными в графе тогда и только тогда, когда связанные с ними фигуры имеют непустое пересечение. Проблемы этого типа, которые являются завершенными для экзистенциальной теории действительного, включают в себя признание графы пересечений из отрезки линии в самолете,^[4][18][5]признание графы единичного диска,^[19]и распознавание графов пересечений выпуклых множеств на плоскости.^[4]

Для графиков, нарисованных на плоскости без пересечений, Теорема Фари заявляет, что каждый получает тот же класс планарные графы независимо от того, нарисованы ли ребра графа как отрезки прямых или как произвольные кривые. Но эта эквивалентность не выполняется для других типов рисунков. Например, хотя номер перехода графа (минимальное количество пересечений на чертеже с произвольно искривленными краями) может быть определено в NP, для экзистенциальной теории вещественных чисел полное определение, существует ли рисунок, достигающий заданной границы числа прямолинейных пересечений ( минимальное количество пар ребер, пересекающихся на любом чертеже с ребрами, нарисованными как отрезки прямых линий на плоскости).^[4][20]Для экзистенциальной теории вещественных чисел также полно проверить, может ли данный граф быть нарисован на плоскости с прямыми линиями и с заданным набором пар ребер в качестве его пересечений, или, что эквивалентно, можно ли нарисовать изогнутый рисунок с пересечениями выпрямлен таким образом, чтобы сохранить пересечения.^[21]

Другие законченные проблемы экзистенциальной теории действительного включают:

• то проблема художественной галереи найти наименьшее количество точек, из которых видны все точки данного многоугольника.^[22]
• то проблема упаковки решения, может ли данный набор полигонов поместиться в заданный квадратный контейнер.^[23]
• признание графики единичных расстояний, и проверка того, измерение или евклидово измерение графа не более чем заданное значение.^[9]
• растяжимость псевдолинии (то есть заданное семейство кривых на плоскости, определяющее, являются ли они гомеоморфный к расположение линий );^[4][24][25]
• как слабая, так и сильная выполнимость геометрических квантовая логика в любом фиксированном размере> 2;^[26]
• Модель контрольных интервальных цепей Маркова относительно однозначных автоматов^[27]
• алгоритмический Проблема Стейница (учитывая решетка, определим, является ли это решеткой граней выпуклый многогранник ) даже в случае ограничения на четырехмерные многогранники;^[28][29]
• пространства реализаций расположений некоторых выпуклых тел^[30]
• различные свойства Равновесия Нэша многопользовательских игр^[31][32][33]
• вложение заданного абстрактного комплекса треугольников и четырехугольников в трехмерное евклидово пространство;^[17]
• встраивание нескольких графов на общем множестве вершин в плоскость так, чтобы все графы рисовались без пересечений;^[17]
• признавая графики видимости наборов плоских точек;^[17]
• (проективная или нетривиальная аффинная) выполнимость уравнения между двумя членами над перекрестное произведение;^[34]
• определение минимума номер откоса непересекающегося чертежа планарный граф.^[35]

Исходя из этого, класс сложности ${\displaystyle \exists \mathbb {R} }$ был определен как набор задач, имеющих полиномиальное время много-однозначной редукции к экзистенциальной теории вещественных чисел.^[4]

использованная литература

1. Басу, Саугата; Поллак, Ричард; Рой, Мари-Франсуаза (2006), «Экзистенциальная теория реальности», Алгоритмы в реальной алгебраической геометрии, Алгоритмы и вычисления в математике, 10 (2-е изд.), Springer-Verlag, стр. 505–532, Дои:10.1007/3-540-33099-2_14, ISBN  978-3-540-33098-1.
2. Кэнни, Джон (1988), "Некоторые алгебраические и геометрические вычисления в PSPACE", Материалы двадцатого ежегодного симпозиума ACM по теории вычислений (STOC '88, Чикаго, Иллинойс, США), Нью-Йорк, Нью-Йорк, США: ACM, стр. 460–467, Дои:10.1145/62212.62257, ISBN  0-89791-264-0.
3. Пассмор, Грант Олни; Джексон, Пол Б. (2009), "Комбинированные методы принятия решений для экзистенциальной теории реальности", Интеллектуальная компьютерная математика: 16-й симпозиум, Calculemus 2009, 8-я международная конференция, MKM 2009, проведенная как часть CICM 2009, Гранд-Бенд, Канада, 6-12 июля 2009 г., Материалы, часть II, Конспект лекций по информатике, 5625, Springer-Verlag, стр. 122–137, Дои:10.1007/978-3-642-02614-0_14.
4. Шефер, Маркус (2010), «Сложность некоторых геометрических и топологических задач» (PDF), Графический рисунок, 17-й Международный симпозиум, GD 2009, Чикаго, Иллинойс, США, сентябрь 2009 г., исправленные статьи, Конспект лекций по информатике, 5849, Springer-Verlag, стр. 334–344, Дои:10.1007/978-3-642-11805-0_32.
5. Матушек, Иржи (2014), Графики пересечений сегментов и ${\displaystyle \exists \mathbb {R} }$, arXiv:1406.2636, Bibcode:2014arXiv1406.2636M
6. Тарский, Альфред (1948), Метод принятия решений для элементарной алгебры и геометрии, RAND Corporation, Санта-Моника, Калифорния, Г-Н  0028796.
7. Матиясевич, Ю. В. (2006), «Десятая проблема Гильберта: диофантовы уравнения в двадцатом веке», Математические события ХХ века, Берлин: Springer-Verlag, стр. 185–213, Дои:10.1007/3-540-29462-7_10, Г-Н  2182785.
8. Хун, Хун (11 сентября 1991 г.), Сравнение нескольких алгоритмов принятия решений для экзистенциальной теории вещественных чисел, Технический отчет, 91-41, RISC Linz^{[постоянная мертвая ссылка ]}.
9. Шефер, Маркус (2013), «Реализуемость графиков и связей», в Пах, Янош (ред.), Тридцать очерков по теории геометрических графов, Springer-Verlag, стр. 461–482, Дои:10.1007/978-1-4614-0110-0_24.
10. Коллинз, Джордж Э. (1975), "Исключение кванторов для вещественных замкнутых полей цилиндрическим алгебраическим разложением", Теория автоматов и формальные языки (Вторая конференция GI, Кайзерслаутерн, 1975), Конспект лекций по информатике, 33, Берлин: Springer-Verlag, стр. 134–183, Г-Н  0403962.
11. Григорьев, Д.Ю. (1988), "Сложность решающей алгебры Тарского", Журнал символических вычислений, 5 (1–2): 65–108, Дои:10.1016 / S0747-7171 (88) 80006-3, Г-Н  0949113.
12. Григорьев, Д.Ю.; Воробьев Н. Н., мл. (1988), "Решение систем полиномиальных неравенств за субэкспоненциальное время", Журнал символических вычислений, 5 (1–2): 37–64, Дои:10.1016 / S0747-7171 (88) 80005-1, Г-Н  0949112.
13. Ренегар, Джеймс (1992), "О вычислительной сложности и геометрии теории первого порядка вещественных чисел. I. Введение. Предварительные сведения. Геометрия полуалгебраических множеств. Проблема решения для экзистенциальной теории вещественных чисел", Журнал символических вычислений, 13 (3): 255–299, Дои:10.1016 / S0747-7171 (10) 80003-3, Г-Н  1156882.
14. Ренегар, Джеймс (1992), "О вычислительной сложности и геометрии теории первого порядка вещественных чисел. II. Общая проблема решения. Предварительные сведения для исключения квантора", Журнал символических вычислений, 13 (3): 301–327, Дои:10.1016 / S0747-7171 (10) 80004-5, Г-Н  1156883.
15. Ренегар, Джеймс (1992), "О вычислительной сложности и геометрии теории первого порядка вещественных чисел. III. Исключение кванторов", Журнал символических вычислений, 13 (3): 329–352, Дои:10.1016 / S0747-7171 (10) 80005-7, Г-Н  1156884.
16. Хайнц, Джус; Рой, Мари-Франсуаза; Солерно, Пабло (1993), "О теоретической и практической сложности экзистенциальной теории реальности", Компьютерный журнал, 36 (5): 427–431, Дои:10.1093 / comjnl / 36.5.427, Г-Н  1234114.
17. Кардинал, Жан (декабрь 2015 г.), "Столбец 62 вычислительной геометрии", Новости SIGACT, 46 (4): 69–78, arXiv:cs / 0010039, Дои:10.1145/2852040.2852053.
18. Кратохвил, Ян; Матушек, Иржи (1994), "Графы пересечений отрезков", Журнал комбинаторной теории, Серия B, 62 (2): 289–315, Дои:10.1006 / jctb.1994.1071, Г-Н  1305055.
19. Канг, Росс Дж .; Мюллер, Тобиас (2011), "Сферы и представления графов в виде скалярных произведений", Материалы двадцать седьмого ежегодного Симпозиум по вычислительной геометрии (SCG'11), 13–15 июня 2011 г., Париж, Франция, стр. 308–314.
20. Бинсток, Дэниел (1991), "Некоторые доказуемо трудные задачи с числами скрещивания", Дискретная и вычислительная геометрия, 6 (5): 443–459, Дои:10.1007 / BF02574701, Г-Н  1115102.
21. Кинчл, Ян (2011), "Простая реализуемость полных абстрактных топологических графов в P", Дискретная и вычислительная геометрия, 45 (3): 383–399, Дои:10.1007 / s00454-010-9320-х, Г-Н  2770542.
22. Абрахамсен, Миккель; Адамашек, Анна; Мильцов, Тилльманн (2017), Проблема художественной галереи ${\displaystyle \exists \mathbb {R} }$-полный, arXiv:1704.06969, Bibcode:2017arXiv170406969A.
23. Абрахамсен, Миккель; Мильцов, Тилльманн; Сейферт, Надя (2020), Рамки для ${\displaystyle \exists \mathbb {R} }$-Полнота задач двумерной упаковки., arXiv:2004.07558.
24. Мнёв, Н. Е. (1988), "Теоремы универсальности по проблеме классификации многообразий конфигураций и многообразий выпуклых многогранников", Топология и геометрия - семинар Рохлина, Конспект лекций по математике, 1346, Берлин: Springer-Verlag, стр. 527–543, Дои:10.1007 / BFb0082792, Г-Н  0970093.
25. Шор, Питер В. (1991), "Растяжимость псевдолинии NP-трудна", Прикладная геометрия и дискретная математика, Серия DIMACS по дискретной математике и теоретической информатике, 4, Провиденс, Род-Айленд: Американское математическое общество, стр. 531–554, Г-Н  1116375.
26. Херрманн, Кристиан; Зиглер, Мартин (2016), "Вычислительная сложность квантовой выполнимости", Журнал ACM, 63, Дои:10.1145/2869073.
27. Бенедикт, Майкл; Ленхардт, Растислав; Уоррелл, Джеймс (2013), "Проверка модели LTL интервальных цепей Маркова", Инструменты и алгоритмы построения и анализа систем. ТАКАС 2013, Конспект лекций по информатике, 7795, стр. 32–46, Дои:10.1007/978-3-642-36742-7_3
28. Бьёрнер, Андерс; Лас Вергнас, Мишель; Штурмфельс, Бернд; Белый, Нил; Циглер, Гюнтер М. (1993), Ориентированные матроиды, Энциклопедия математики и ее приложений, 46, Кембридж: Издательство Кембриджского университета, следствие 9.5.10, стр. 407, г. ISBN  0-521-41836-4, Г-Н  1226888.
29. Рихтер-Геберт, Юрген; Циглер, Гюнтер М. (1995), «Пространства реализации 4-многогранников универсальны», Бюллетень Американского математического общества, Новая серия, 32 (4): 403–412, arXiv:математика / 9510217, Дои:10.1090 / S0273-0979-1995-00604-X, Г-Н  1316500.
30. Доббинс, Майкл Джин; Холмсен, Андреас; Хабард, Альфредо (2014). «Пространства реализации расположений выпуклых тел». arXiv:1412.0371..
31. Гарг, Джугал; Мехта, Рута; Вазирани, Виджай В.; Язданбод, Садра (2015), «Полнота ETR для решений многопользовательских (симметричных) равновесий Нэша», Proc. 42-й Международный коллоквиум по автоматам, языкам и программированию (ICALP), Конспект лекций по информатике, 9134, Springer, стр. 554–566, Дои:10.1007/978-3-662-47672-7_45.
32. Било, Витторио; Маврониколас, Мариос (2016), «Каталог ETR-Complete задач решения о равновесии Нэша в многопользовательских играх», Материалы 33-го Международного симпозиума по теоретическим аспектам информатики, LIPIcs, Schloss Dagstuhl - Leibnitz Zentrum fuer Informatik, стр. 17: 1–17: 13, Дои:10.4230 / LIPIcs.STACS.2016.17.
33. Било, Витторио; Маврониколас, Мариос (2017), "ETR-Complete Decision Problems о симметричных равновесиях по Нэшу в симметричных многопользовательских играх", Материалы 34-го Международного симпозиума по теоретическим аспектам информатики, LIPIcs, Schloss Dagstuhl - Leibnitz Zentrum fuer Informatik, стр. 13: 1–13: 14.
34. Херрманн, Кристиан; Соколи, Йоханна; Зиглер, Мартин (2013), «Выполнимость условий перекрестного произведения является полной для реальных недетерминированных политимных машин Блюма-Шуба-Смейла», Труды 6-й конференции по машинам, вычислениям и универсальности (MCU'13), Дои:10.4204 / EPTCS.128.
35. Хоффманн, Удо (2016), «Число плоского уклона», Труды 28-й Канадской конференции по вычислительной геометрии (CCCG 2016).