Экзистенциальная психология
- 1 year ago
- 0
- 0
Экзистенциальная теория вещественных чисел — это множество всех верных утверждений вида
где — это , в которую входят равенства и неравенства вещественных многочленов .
Задача разрешимости для экзистенциальной теории вещественных чисел — это задача нахождения алгоритма , который решает для каждой формулы, верна она или нет. Эквивалентно, это задача проверки, что заданное полуалгебраическое множество не пусто . Эта задача разрешимости является NP-трудной и лежит в PSPACE . Таким образом, задача имеет существенно меньшую сложность, чем процедура исключения кванторов Альфреда Тарского в теориях первого порядка вещественных . Однако, на практике, общие методы для теории первого порядка остаются предпочтительным выбором для решения такого рода задач .
Многие естественные задачи , особенно задачи распознавания геометрических графов пересечений и выпрямления рёбер рисунков графов с пересечениями , могут быть решены путём преобразования их в вариант экзистенциальной теории вещественных чисел и являются для этой теории. Для описания этих задач определяется класс сложности , находящийся между NP и PSPACE .
В математической логике «теория» — это формальный язык , состоящий из множества предложений , записанных с использованием фиксированного набора символов. имеет следующие символы :
Последовательность этих символов образует предложение, которое принадлежат теории первого порядка вещественных чисел, если грамматически правильно построено, все его переменные имеют соответствующие кванторы и (когда интерпретируется как математическое утверждение о вещественных числах ) является верным утверждением. Как показал Тарский, эта теория может быть описана схемой аксиом и процедурой принятия решений, которая является полной и эффективной, это: для любого грамматически верного утверждения с полным набором кванторов либо само утверждение, либо его отрицание (но не оба) может быть выведено из аксиом. Та же самая теория описывает любое , не просто вещественные числа . Существуют, однако, другие числовые системы, которые не описываются этими аксиомами точно. Теория, определённая тем же образом для целых чисел вместо вещественных чисел, согласно теореме Матиясевича , является неразрешимой даже для утверждений существования для диофантовых уравнений .
Экзистенциальная теория вещественных чисел является подмножеством теории первого порядка и состоит из утверждений, в которых каждый квантор является квантором существования и все они появляются до любого другого символа. То есть это множество верных утверждений вида
где — , содержащая равенства и неравенства с многочленами над вещественными числами . Задача разрешимости для экзистенциальной теории вещественных чисел — это алгоритмическая задача проверки, принадлежит ли данное предложение этой теории. Эквивалентно, для строк, проходящих базовые синтаксические проверки (то есть предложение использует правильные символы, имеет правильный синтаксис и не имеет переменных без кванторов), является задачей проверки, что утверждение является верным утверждением над вещественными числами. Множество n -кортежей вещественных чисел , для которых верно, называется полуалгебраическое множество , так что задача разрешимости для экзистенциальной теории вещественных чисел может эквивалентно быть перефразирована как проверка, что заданное полуалгебраическое множество не пусто .
Для определения временно́й сложности алгоритмов для задачи разрешимости экзистенциальной теории вещественных чисел важно иметь способ измерения размера входа. Простейший способ измерения этого типа – длина предложения, то есть число символов, входящих в утверждение . Однако, чтобы получить более точный анализ поведения алгоритмов для этой задачи, удобно разбить размер входа на несколько переменных, выделяя число переменных с кванторами, число многочленов в предложении и степени этих многочленов .
Золотое сечение можно определить как корень многочлена . Этот многочлен имеет два корня, из которых только один (золотое сечение) превосходит единицу. Таким образом, существование золотого сечения можно выразить предложением
Поскольку золотое сечение существует, утверждение является истинным и принадлежит экзистенциальной теории вещественных чисел. Ответ задачи разрешимости для экзистенциальной теории вещественных чисел, если задать это предложение в качестве входа, является булевским значением true ( истина ).
Неравенство между средним арифметическим и средним геометрическим утверждает, что для любых двух неотрицательных чисел и выполняется следующее неравенство:
Утверждение является утверждением первого порядка над вещественными числами, но оно универсально (не содержит кванторов существования) и использует лишние символы деления, квадратного корня и числа 2, которые не позволены в теории первого порядка вещественных чисел. Тем не менее, после возведения обеих частей в квадрат предложение может быть преобразовано в следующее экзистенциальное утверждение, которое можно интерпретировать как вопрос о существовании контрпримера неравенству:
Ответом задачи разрешимости для экзистенциальной теории вещественных чисел, входом которой является это уравнение, является булевское значение false ( ложь ), то есть контрпримера не существует. Таким образом, это предложение не принадлежит экзистенциальной теории вещественных чисел, хотя и корректно с точки зрения грамматики.
Метод Альфреда Тарского исключения кванторов (1948) показывает, что экзистенциальная теория вещественных чисел (и, более обще, теория первого порядка вещественных чисел) алгоритмически разрешимы, но без элементарных границ на сложность . Метод (1975) улучшил зависимость от времени до двойной экспоненциальности , вида
где — число бит, требуемых для представления коэффициентов в утверждении, значение которого требуется определить, — число многочленов в утверждении, — их общая степень, а — число переменных В 1988 и Николай Воробьёв показали, что сложность экспоненциальна со степенью, являющейся многочленом от ,
и в последовательности статей, опубликованных в 1992, Джеймс Ренегар улучшил оценку до слегка превышающей экспоненту on .
Между тем, в 1988 описал другой алгоритм, который также экспоненциально зависит по времени, но имеет лишь полиномиальную сложность по памяти. То есть он показал, что задача может быть решена в классе PSPACE .
этих алгоритмов может ввести в заблуждение, поскольку алгоритмы могут работать с входом только очень малого размера. Сравнивая в 1991 алгоритмы, Хун Хонг оценил время работы процедуры Коллинза (с двойной экспоненциальной оценкой) для задачи, размер которой описывается установкой всех приведённых выше параметров в 2, в менее чем две секунды, в то время как алгоритмы Григорьева, Воробьёва и Ренегара потратили бы на решение задачи более миллиона лет . В 1993 Йос, Рой и Солерно высказали предположение, что должна существовать возможность небольшой модификации процедур с экспоненциальным временем, чтобы сделать их на практике быстрее цилиндрического алгебраического решения, что соответствовало бы теории . Однако, на момент 2009, общие методы для теории первого порядка вещественных чисел остаются лучшими на практике по сравнению с алгоритмами с простой экспоненциальной оценкой, специально разработанными для экзистенциальной теории вещественных чисел .
Некоторые задачи вычислительной сложности и могут быть классифицированы как для экзистенциальной теории вещественных чисел. То есть любая задача из экзистенциальной теории вещественных чисел имеет полиномиальное многозначное сведение к варианту одной из этих задач и, наоборот, эти задачи сводимы к экзистенциальной теории вещественных чисел .
Несколько задач этого типа касаются распознавания графов пересечений определённого вида. В этих задачах входом является неориентированный граф . Целью является определение, можно ли сопоставить геометрические формы определённого класса вершинам графа таким образом, что две вершины в графе смежны тогда и только тогда, когда ассоциированные геометрические формы имеют непустое пересечение. Полные задачи этого типа для экзистенциальной теории вещественных чисел включают
Для графов, нарисованных на плоскости без пересечений, теорема Фари утверждает, что мы получим тот же класс планарных графов независимо от того, должны ли рёбра графа быть нарисованы в виде отрезков, либо их можно рисовать в виде кривых. Но эта эквивалентность классов не верна для других типов вычерчивания графов. Например, хотя число пересечений графа (минимальное число пересечений рёбер при криволинейных рёбрах) может быть определено как принадлежащее классу NP, для экзистенциальной теории вещественных чисел задача определения, существуют ли рисунки, на которых достигается заданная граница прямолинейного числа пересечений (минимальное число пар рёбер, которые пересекаются в любом рисунке с рёбрами в виде прямолинейных отрезков на плоскости), является полной . Полной также является для экзистенциальной теории вещественных чисел задача проверки, можно ли данный граф нарисовать на плоскости с отрезками в виде прямолинейных рёбер и с заданным множеством пар пересекающихся рёбер или, эквивалентно, можно ли рисунок с криволинейными рёбрами с пересечениями выпрямить таким образом, что пересечения сохранятся .
Другие полные задачи для экзистенциальной теории вещественных чисел:
;
Опираясь на это, класс сложности определяется как множество задач, имеющих полиномиальное время сведения по Карпу к экзистенциальной теории вещественных чисел .