Экзистенциальная теория вещественных чисел

Экзистенциальная теория вещественных чисел — это множество всех верных утверждений вида

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

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

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

Многие естественные задачи геометрической теории графов, особенно задачи распознавания геометрических графов пересечений и выпрямления рёбер рисунков графов с пересечениями, могут быть решены путём преобразования их в вариант экзистенциальной теории вещественных чисел и являются полными для этой теории. Для описания этих задач определяется класс сложности $\exists \mathbb {R}$, находящийся между NP и PSPACE .

Предпосылки

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

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

Последовательность этих символов образует предложение, которое принадлежат теории первого порядка вещественных чисел, если грамматически правильно построено, все его переменные имеют соответствующие кванторы и (когда интерпретируется как математическое утверждение о вещественных числах) является верным утверждением. Как показал Тарский, эта теория может быть описана схемой аксиом и процедурой принятия решений, которая является полной и эффективной, это: для любого грамматически верного утверждения с полным набором кванторов либо само утверждение, либо его отрицание (но не оба) может быть выведено из аксиом. Та же самая теория описывает любое вещественно замкнутое поле, не просто вещественные числа. Существуют, однако, другие числовые системы, которые не описываются этими аксиомами точно. Теория, определённая тем же образом для целых чисел вместо вещественных чисел, согласно теореме Матиясевича, является неразрешимой даже для утверждений существования для диофантовых уравнений.

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

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

где $F(X_{1},\dots X_{n})$ — формула без кванторов, содержащая равенства и неравенства с многочленами над вещественными числами. Задача разрешимости для экзистенциальной теории вещественных чисел — это алгоритмическая задача проверки, принадлежит ли данное предложение этой теории. Эквивалентно, для строк, проходящих базовые синтаксические проверки (то есть предложение использует правильные символы, имеет правильный синтаксис и не имеет переменных без кванторов), является задачей проверки, что утверждение является верным утверждением над вещественными числами. Множество n-кортежей вещественных чисел $(X_{1},\dots X_{n})$, для которых $F(X_{1},\dots X_{n})$ верно, называется полуалгебраическое множество, так что задача разрешимости для экзистенциальной теории вещественных чисел может эквивалентно быть перефразирована как проверка, что заданное полуалгебраическое множество не пусто.

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

Примеры

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

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

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

Неравенство между средним арифметическим и средним геометрическим утверждает, что для любых двух неотрицательных чисел $x$ и $y$ выполняется следующее неравенство:

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

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

$\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})<(1+1+1+1)\times X_{1}\times X_{2}{\bigr )}.$

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

Алгоритмы

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

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

где $L$ — число бит, требуемых для представления коэффициентов в утверждении, значение которого требуется определить, $m$ — число многочленов в утверждении, $d$ — их общая степень, а $n$ — число переменных В 1988 Дмитрий Григорьев и Николай Воробьёв показали, что сложность экспоненциальна со степенью, являющейся многочленом от $n$,

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

и в последовательности статей, опубликованных в 1992, Джеймс Ренегар улучшил оценку до слегка превышающей экспоненту on $n$.

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

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

Асимптотическая вычислительная сложность этих алгоритмов может ввести в заблуждение, поскольку алгоритмы могут работать с входом только очень малого размера. Сравнивая в 1991 алгоритмы, Хун Хонг оценил время работы процедуры Коллинза (с двойной экспоненциальной оценкой) для задачи, размер которой описывается установкой всех приведённых выше параметров в 2, в менее чем две секунды, в то время как алгоритмы Григорьева, Воробьёва и Ренегара потратили бы на решение задачи более миллиона лет. В 1993 Йос, Рой и Солерно высказали предположение, что должна существовать возможность небольшой модификации процедур с экспоненциальным временем, чтобы сделать их на практике быстрее цилиндрического алгебраического решения, что соответствовало бы теории. Однако, на момент 2009, общие методы для теории первого порядка вещественных чисел остаются лучшими на практике по сравнению с алгоритмами с простой экспоненциальной оценкой, специально разработанными для экзистенциальной теории вещественных чисел.

Полные задачи

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

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

• распознавание графов пересечений отрезков на плоскости,
• распознавание графов единичных кругов
• распознавание графов пересечений выпуклых множеств на плоскости.

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

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

• задача о картинной галерее заключается в поиске наименьшего числа точек, из которых видны все точки заданного многоугольника.
• распознавание графов единичных графов и проверка, не превосходит ли размерность или евклидова размерность графа заданного значения.
• выпрямление псевдопрямых (то есть, если дано семейство кривых на плоскости, определение, гомеоморфны ли они конфигурации прямых);
• слабая и сильная выполнимость геометрической квантовой логики в любой фиксированной размерности >2;
• алгоритмическая задача Штайница (дана решётка, определить, является ли она решёткой грани выпуклого многогранника), даже если ограничиться четырёхмерными многогранниками;
• реализация пространств размещения некоторых выпуклых тел.
• различные свойства равновесия Нэша игр нескольких лиц

;

• вложение заданного абстрактного комплекса треугольников и четырёхугольников в трёхмерное евклидово пространство;
• вложение нескольких графов на общем множестве вершин в плоскость так, что все графы будут нарисованы без пересечений;
• распознавание графов видимости плоских множеств точек;
• (проективная или нетривиальная аффинная) выполнимость равенства двух векторных произведений;
• определение минимального числа наклонов рисунка без пересечений рёбер планарного графа.

Опираясь на это, класс сложности $\exists \mathbb {R}$ определяется как множество задач, имеющих полиномиальное время сведения по Карпу к экзистенциальной теории вещественных чисел.