Введение

Пресбургерская арифметика — это теория первого порядка натуральных чисел с операцией сложения, названная в честь Мойжеша Пресбургера, который ввёл её в 1929 году. Сигнатура пресбургерской арифметики содержит только операции сложения и равенства, полностью исключая операцию умножения. Теория вычислительно аксиоматизируема; аксиомы включают схему индукции. Пресбургерская арифметика значительно слабее арифметики Пеано, которая включает в себя как сложение, так и умножение. В отличие от арифметики Пеано, пресбургерская арифметика является разрешимой теорией. Это означает, что для любого высказывания на языке пресбургерской арифметики можно алгоритмически определить, является ли оно доказуемым из аксиом пресбургерской арифметики. Однако асимптотическая вычислительная сложность времени работы этого алгоритма, как показано, не менее чем двойная экспонента.

Комплексность вычислений

Проблема решения для арифметики Пресбургера является интересным примером в теории вычислительной сложности и вычислений. Пусть n — длина утверждения в арифметике Пресбургера. Тогда было доказано, что в худшем случае доказательство утверждения в логике первого порядка имеет длину не менее , для некоторой константы c > 0. Следовательно, их алгоритм принятия решений для арифметики Пресбургера имеет время выполнения не менее экспоненциальное. Фишер и Рабин также доказали, что для любой разумной аксиоматизации (определенной точно в их статье) существуют теоремы длины n, имеющие доказательства двойной экспоненциальной длины. Интуитивно это говорит о том, что существуют вычислительные ограничения на то, что может быть доказано компьютерными программами. Работа Фишера и Рабина также подразумевает, что арифметика Пресбургера может использоваться для определения формул, которые правильно вычисляют любой алгоритм, при условии, что входные данные меньше относительно больших границ. Эти границы можно увеличить, но только с использованием новых формул. С другой стороны, тройная экспоненциальная верхняя граница для процедуры принятия решений по арифметике Пресбургера была доказана, а более точная граница сложности была показана с использованием чередующихся классов сложности. Множество истинных утверждений в арифметике Пресбургера (PA) является полным для TimeAlternations(22nO(1), n). Таким образом, его сложность находится между двойным экспоненциальным недетерминированным временем (2NEXP) и двойным экспоненциальным пространством (2EXPSPACE). Полнота доказывается с помощью полиномиальных преобразований many-to-one. (Также следует отметить, что хотя арифметика Пресбургера обычно обозначается PA, в математике в целом PA обычно означает арифметику Пеано.) Для более детального результата, пусть PA(i) будет множеством истинных Σi PA утверждений, а PA(i, j) — множеством истинных Σi PA утверждений, где каждый блок кванторов ограничен j переменными. '<' считается кванторно-свободным; здесь ограниченные кванторы считаются кванторами. PA(1, j) находится в классе P, в то время как PA(1) является NP-полной. Для i > 0 и j > 2, PA(i + 1, j) является ΣiP-полной. Результат о сложности требует только j > 2 (в отличие от j = 1) в последнем блоке кванторов. Для i > 0, PA(i + 1) является ΣiEXP-полной. Короткая арифметика Пресбургера является полной (и, следовательно, NP-полной). Здесь «короткая» требует ограниченного (т.е. ) размера предложения, за исключением того, что целые константы не ограничены (но их количество битов в двоичном представлении учитывается при определении размера входных данных). Кроме того, двухпеременная PA (без ограничения «короткая») является NP-полной. Короткая (и, следовательно, ) PA находится в классе P, и это распространяется на параметрическое целочисленное линейное программирование фиксированной размерности.

Приложения

Поскольку арифметика Пресбургера является разрешимой, существуют автоматические доказатели теорем для арифметики Пресбургера. Например, система поддержки доказательств Coq включает тактику omega для арифметики Пресбургера, а система поддержки доказательств Isabelle содержит верифицированную процедуру устранения кванторов. Двойная экспоненциальная сложность теории делает непрактичным использование этих доказателей теорем для сложных формул, однако такое поведение проявляется только при наличии вложенных кванторов: опишите автоматический доказатель теорем, использующий симплекс-алгоритм для расширенной арифметики Пресбургера без вложенных кванторов, чтобы доказать некоторые экземпляры формул арифметики Пресбургера без кванторов. Более современные решатели задач выполнимости по модулю теорий используют методы целочисленного программирования для обработки квантор-свободного фрагмента теории арифметики Пресбургера. Арифметику Пресбургера можно расширить, включив умножение на константы, поскольку умножение является повторным сложением. Большинство вычислений индексов массивов тогда попадают в область разрешимых задач. Этот подход лежит в основе как минимум пяти систем доказательства корректности компьютерных программ, начиная с верификатора Паскаля Стэнфорда в конце 1970-х годов и заканчивая системой Spec# от Microsoft в 2005 году.

Отношение Пресбургер-определяемое целое число

Некоторые свойства теперь приведены для целочисленных отношений, определяемых в арифметике Пресбургера. Для простоты все отношения, рассматриваемые в этом разделе, определены над неотрицательными целыми числами. Отношение является Пресбургер-определяемым тогда и только тогда, когда оно является полулинейным множеством. Униарное целочисленное отношение, то есть множество неотрицательных целых чисел, является Пресбургер-определяемым тогда и только тогда, когда оно в конечном итоге периодично. То есть, существует порог и положительный период такие, что для всех целых чисел , если и только если . По теореме Кобхама — Семенова, отношение является Пресбургер-определяемым тогда и только тогда, когда оно определимо в арифметике Бюхи с основанием для всех . Отношение, определимое в арифметике Бюхи с основанием и для и являющихся мультипликативно независимыми целыми числами, является Пресбургер-определяемым. Целочисленное отношение является Пресбургер-определяемым тогда и только тогда, когда все множества целых чисел, которые определимы в логике первого порядка с операцией сложения и (то есть, арифметика Пресбургера плюс предикат для ), являются Пресбургер-определяемыми. Эквивалентно, для каждого отношения, которое не является Пресбургер-определяемым, существует формула первого порядка с операцией сложения и , определяющая множество целых чисел, которое нельзя определить, используя только операцию сложения.