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

Материал из testwiki
Перейти к навигации Перейти к поиску

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

∃X1⋯∃XnF(X1,…,Xn),

где F(X1,…Xn) — это Шаблон:Не переведено 5, в которую входят равенства и неравенства вещественных многочленовШаблон:Sfn.

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

Многие естественные задачи Шаблон:Не переведено 5, особенно задачи распознавания геометрических графов пересечений и выпрямления рёбер рисунков графов с пересечениями, могут быть решены путём преобразования их в вариант экзистенциальной теории вещественных чисел и являются Шаблон:Не переведено 5 для этой теории. Для описания этих задач определяется класс сложности ∃ℝ, находящийся между NP и PSPACE Шаблон:Sfn.

Предпосылки

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

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

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

∃X1⋯∃XnF(X1,…,Xn),

где F(X1,…Xn) — Шаблон:Не переведено 5, содержащая равенства и неравенства с многочленами над вещественными числами. Задача разрешимости для экзистенциальной теории вещественных чисел — это алгоритмическая задача проверки, принадлежит ли данное предложение этой теории. Эквивалентно, для строк, проходящих базовые синтаксические проверки (то есть предложение использует правильные символы, имеет правильный синтаксис и не имеет переменных без кванторов), является задачей проверки, что утверждение является верным утверждением над вещественными числами. Множество n-кортежей вещественных чисел (X1,…Xn), для которых F(X1,…Xn) верно, называется полуалгебраическое множество, так что задача разрешимости для экзистенциальной теории вещественных чисел может эквивалентно быть перефразирована как проверка, что заданное полуалгебраическое множество не пустоШаблон:Sfn.

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

Примеры

Золотое сечение φ можно определить как корень многочлена x2−x−1. Этот многочлен имеет два корня, из которых только один (золотое сечение) превосходит единицу. Таким образом, существование золотого сечения можно выразить предложением

∃X1(X1>1∧X1×X1−X1−1=0).

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

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

x+y2≥xy.

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

∃X1∃X2(X1≥0∧X2≥0∧(X1+X2)×(X1+X2)<(1+1+1+1)×X1×X2).

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

Алгоритмы

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

L3(md)2O(n)

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

L(md)n2

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

Llog⁡Llog⁡log⁡L(md)O(n).

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

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

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

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

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

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

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

Шаблон:Sfn;

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

Примечания

Шаблон:Примечания

Литература

Шаблон:Refbegin

Шаблон:Refend

Шаблон:Rq

Источник — https://ru.wiki.beta.math.wmflabs.org/w/index.php?title=Экзистенциальная_теория_вещественных_чисел&oldid=18767