Пресбургерская арифметика

Пресбургера арифметика является теорией первого порядка из натуральных чисел с добавлением , названных в чести Мохзесса Пресбергера , который ввел его в 1929 годе подпись Пресбургер арифметики содержит только операцию сложения и равенство , опуская умножения операции полностью. Аксиомы включают схему индукции .

Арифметика Пресбургера намного слабее арифметики Пеано , которая включает в себя как операции сложения, так и умножения. В отличие от арифметики Пеано, арифметика Пресбургера - разрешимая теория . Это означает, что для любого предложения на языке арифметики Пресбургера можно алгоритмически определить, доказуемо ли это предложение с помощью аксиом арифметики Пресбургера. Однако асимптотическая вычислительная сложность этого алгоритма по крайней мере вдвое экспоненциальна , как показали Фишер и Рабин (1974) .

Обзор [ править ]

Язык арифметики Пресбургера содержит константы 0 и 1 и двоичную функцию +, интерпретируемую как сложение.

На этом языке аксиомы арифметики Пресбургера являются универсальным закрытием следующего:

1. ¬ (0 = х + 1)
2. х + 1 = у + 1 → х = у
3. х + 0 = х
4. х + ( у + 1) = ( х + у ) + 1
5. Пусть P ( x ) будет формулой первого порядка на языке арифметики Пресбургера со свободной переменной x (и, возможно, другими свободными переменными). Тогда следующая формула является аксиомой:

( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y ).

(5) является аксиомой схемы по индукции , представляющая бесконечное число аксиом. Они не могут быть заменены любым конечным числом аксиом, ^{[ править ]} , то есть, Пресбургер арифметический не является конечно аксиоматизируемым в логике первого порядка.

Арифметику Пресбургера можно рассматривать как теорию первого порядка с равенством, содержащую в точности все следствия вышеприведенных аксиом. В качестве альтернативы его можно определить как набор тех предложений, которые верны в предполагаемой интерпретации : структура неотрицательных целых чисел с константами 0, 1 и добавление неотрицательных целых чисел.

Арифметика Пресбургера должна быть полной и разрешимой. Следовательно, он не может формализовать такие понятия, как делимость или простота , или, в более общем плане, любое числовое понятие, ведущее к умножению переменных. Однако он может формулировать отдельные примеры делимости; например, это доказывает, что «для всех x существует y  : ( y + y = x ) ∨ ( y + y + 1 = x )». Это означает, что каждое число либо четное, либо нечетное.

Свойства [ править ]

Mojżesz Presburger доказал, что арифметика Presburger:

• непротиворечиво : в арифметике Пресбургера нет утверждения, которое можно было бы вывести из аксиом так, чтобы можно было вывести и его отрицание.
• Complete : для каждого утверждения на языке арифметики Пресбургера либо можно вывести его из аксиом, либо можно вывести его отрицание.
• разрешимый : существует алгоритм, который решает, является ли любое данное утверждение в арифметике Пресбургера теоремой или не теоремой.

Разрешимость арифметики Пресбургера может быть продемонстрирована с помощью исключения квантора , дополненного рассуждениями об арифметической конгруэнтности ( Presburger (1929) , Nipkow (2010) , Enderton 2001, p. 188). Шаги, используемые для обоснования алгоритма исключения квантора, можно использовать для определения рекурсивных аксиоматизаций, которые не обязательно содержат схему аксиом индукции ( Presburger (1929) , Stansifer (1984) ).

Напротив, арифметика Пеано , которая представляет собой арифметику Пресбургера, дополненную умножением, не разрешима из-за отрицательного ответа на проблему Entscheidungs . По теореме Гёделя о неполноте арифметика Пеано неполна, и ее непротиворечивость не доказуема внутренне (но см . Доказательство непротиворечивости Гентцена ).

Вычислительная сложность [ править ]

Проблема решения для арифметики Пресбургера - интересный пример в теории сложности вычислений и вычислениях . Пусть n - длина утверждения в арифметике Пресбургера. Затем Фишер и Рабин (1974) доказали, что в худшем случае доказательство утверждения в логике первого порядка имеет длину, по крайней мере , для некоторой константы c > 0. Следовательно, их алгоритм решения для арифметики Пресбургера имеет время выполнения, по крайней мере, экспоненциально. Фишер и Рабин также доказали, что для любой разумной аксиоматизации (определенной именно в их статье) существуют теоремы длины n, которые имеют дважды экспоненциальную${\ displaystyle 2 ^ {2 ^ {cn}}}$длина доказательства. Интуитивно это предполагает, что существуют вычислительные ограничения на то, что может быть доказано компьютерными программами. Работа Фишера и Рабина также подразумевает, что арифметика Пресбургера может использоваться для определения формул, которые правильно вычисляют любой алгоритм, если входные данные меньше относительно больших границ. Границы можно увеличить, но только с помощью новых формул. С другой стороны, тройная экспоненциальная верхняя граница процедуры принятия решения для арифметики Пресбургера была доказана Оппеном (1978).

Более жесткая граница сложности была показана с использованием классов переменной сложности Берманом (1980) . Набор истинных утверждений в арифметике Пресбургера (PA) показан полным для TimeAlternations (2 ^{2 n O (1)} , n). Таким образом, его сложность находится между двойным экспоненциальным недетерминированным временем (2-NEXP) и двойным экспоненциальным пространством (2-EXPSPACE). Полнота определяется при полиномиальном времени однозначных редукций. (Также обратите внимание, что в то время как арифметика Пресбургера обычно обозначается аббревиатурой 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) является Σ i P -полным . Для результата жесткости требуется только j> 2 (в отличие от j = 1) в последнем блоке квантификатора.
Для i> 0 PA (i + 1) является Σ i EXP -полным (и является TimeAlternations (2 ^{n O (i)} , i) -полным). ^[1]

Приложения [ править ]

Поскольку арифметика Пресбургера разрешима, существуют автоматические средства доказательства теорем для арифметики Пресбургера. Например, система помощника по доказательству Coq включает тактическую омега для арифметики Пресбургера, а помощник по доказательству Изабель содержит процедуру исключения проверенного квантора, выполненную Нипкоу (2010) . Двойная экспоненциальная сложность теории делает невозможным использование средств доказательства теорем для сложных формул, но такое поведение наблюдается только при наличии вложенных кванторов: Оппен и Нельсон (1980) описывают автоматическое средство доказательства теорем, которое использует симплекс-алгоритм.на расширенной арифметике Пресбургера без вложенных кванторов для доказательства некоторых примеров бескванторных арифметических формул Пресбургера. Более поздние решатели теорий выполнимости по модулю используют методы полного целочисленного программирования для обработки бескванторного фрагмента арифметической теории Пресбургера ( King, Barrett & Tinelli (2014) ).

Арифметику Пресбургера можно расширить, включив в нее умножение на константы, поскольку умножение - это повторное сложение. Большинство вычислений индексов массива тогда попадают в область решаемых проблем. Этот подход лежит в основе по крайней мере пяти систем проверки корректности компьютерных программ , начиная со Stanford Pascal Verifier в конце 1970-х и заканчивая системой Microsoft Spec # 2005 года.

Целочисленное отношение, определяемое Пресбургером [ править ]

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

Отношение определяется Пресбургером тогда и только тогда, когда оно является полулинейным множеством . ^[2]

Унарное целочисленное отношение , то есть набор неотрицательных целых чисел, определяется Пресбургером тогда и только тогда, когда оно в конечном итоге периодично. То есть, если существует такой порог и положительный период , что для всех целых чисел, таких что , если и только если .${\ displaystyle R}$${\ Displaystyle т \ в \ mathbb {N}}$${\ displaystyle p \ in \ mathbb {N} ^ {> 0}}$${\ displaystyle n}$${\ Displaystyle | п | \ geq t}$${\ displaystyle n \ in R}$${\ displaystyle n + p \ in R}$

По теореме Кобэма – Семенова отношение определимо по Пресбургеру тогда и только тогда, когда оно определимо в арифметике Базы Бюхи для всех . ^{[3] [4]} Отношение, определяемое в арифметике Бюхи с основанием и для и будучи мультипликативно независимыми целыми числами, определимо по Пресбургеру.${\ displaystyle k}$${\ Displaystyle к \ geq 2}$${\ displaystyle k}$${\ displaystyle k '}$${\ displaystyle k}$${\ displaystyle k '}$

Целочисленное отношение является определяемым Пресбургером тогда и только тогда, когда все наборы целых чисел, которые могут быть определены в логике первого порядка с добавлением и (то есть, арифметика Пресбургера плюс предикат для ), являются определяемыми Пресбургером. ^[5] Эквивалентно, для каждого отношения, которое не может быть определено Пресбургером, существует формула первого порядка с добавлением, которая определяет набор целых чисел, который не может быть определен с использованием только сложения.${\ displaystyle R}$${\ displaystyle R}$${\ displaystyle R}$${\ displaystyle R}$${\ displaystyle R}$

Характеристика Мучника [ править ]

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

Пусть будет множество, раздел о , для и определяется как ${\ Displaystyle R \ substeq \ mathbb {N} ^ {d}}$${\ displaystyle x_ {i} = j}$${\ displaystyle R}$${\ displaystyle i <d}$${\ displaystyle j \ in \ mathbb {N}}$

${\displaystyle \left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,x_{d-1})\in R\right\}.}$

Учитывая два набора и -набор целых чисел , набор называется -периодическим по if, для всех таких, что then тогда и только тогда . В самом деле, множество называется -периодическим в том случае, если оно является -периодическим для некоторых таких, что ${\displaystyle R,S\subseteq \mathbb {N} ^{d}}$${\displaystyle d}$${\displaystyle (p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}}$${\displaystyle R}$${\displaystyle (p_{0},\dots ,p_{d-1})}$${\displaystyle S}$${\displaystyle (x_{0},\ldots ,x_{d-1})\in S}$${\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,}$${\displaystyle (x_{0},\ldots ,x_{d-1})\in R}$${\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R}$${\displaystyle s\in \mathbb {N} }$${\displaystyle R}$${\displaystyle s}$${\displaystyle S}$${\displaystyle (p_{0},\ldots ,p_{d-1})}$${\displaystyle (p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}}$

${\displaystyle \sum _{i=0}^{d-1}|p_{i}|<s.}$

Наконец, пусть ${\displaystyle k,x_{0},\dots ,x_{d-1}\in \mathbb {N} }$

${\displaystyle C(k,(x_{0},\ldots ,x_{d-1}))=\left\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1})\mid 0\leqslant c_{i}<k\right\}}$

обозначают куб размером с меньшим углом .${\displaystyle k}$${\displaystyle (x_{0},\dots ,x_{d-1})}$

Теорема Мучника. определяется Пресбургером тогда и только тогда, когда:${\displaystyle R\subseteq \mathbb {N} ^{d}}$

• если тогда все секции являются определяемыми Пресбургером и${\displaystyle d>1}$${\displaystyle R}$
• существует такое, что для каждого существует такое, что для всех с${\displaystyle s\in \mathbb {N} }$${\displaystyle k\in \mathbb {N} }$${\displaystyle t\in \mathbb {N} }$${\displaystyle (x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}}$

${\displaystyle \sum _{i=0}^{d-1}x_{i}>t,}$

${\displaystyle R}$является -периодической в .${\displaystyle s}$${\displaystyle C(k,(x_{0},\dots ,x_{d-1}))}$

Интуитивно понятно, что целое число представляет длину сдвига, целое число - это размер кубиков и является порогом перед периодичностью. Этот результат остается верным, когда выполняется условие ${\displaystyle s}$${\displaystyle k}$${\displaystyle t}$

${\displaystyle \sum _{i=0}^{d-1}x_{i}>t}$

заменяется либо на, либо на .${\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}$${\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}$

Эта характеризация привела к так называемому «определяемому критерию определимости в арифметике Пресбургера», то есть: существует формула первого порядка с сложением и -аричным предикатом, которая выполняется тогда и только тогда, когда она интерпретируется определяемым Пресбургером отношением. Теорема Мучника также позволяет доказать разрешимость автоматической последовательности, допускающей определение Пресбургера.${\displaystyle d}$${\displaystyle R}$${\displaystyle R}$

См. Также [ править ]

• Арифметика Робинсона
• Сколемская арифметика

Ссылки [ править ]

• Хаазе, Кристоф (2018). «Руководство по выживанию по пресбургской арифметике» . Новости ACM SIGLOG . 5 (3): 67–82. DOI : 10.1145 / 3242953.3242964 . S2CID  51847374 .
• Купер, округ Колумбия, 1972, «Доказательство теорем в арифметике без умножения» в Б. Мельцере и Д. Мичи, ред., Machine Intelligence Vol. 7 . Издательство Эдинбургского университета: 91–99.
• Эндертон, Герберт (2001). Математическое введение в логику (2-е изд.). Бостон, Массачусетс: Academic Press . ISBN 978-0-12-238452-3.
• Ферранте, Жанна и Чарльз В. Ракофф, 1979. Вычислительная сложность логических теорий . Конспект лекций по математике 718. Springer-Verlag .
• Фишер, Майкл Дж .; Рабин, Майкл О. (1974). "Суперэкспоненциальная сложность арифметики Пресбургера" . Материалы симпозиума SIAM-AMS по прикладной математике . 7 : 27–41. Архивировано из оригинала на 2006-09-15 . Проверено 11 июня 2006 .
• Г. Нельсон и О.К. Оппен (апрель 1978 г.). «Упроститель, основанный на эффективных алгоритмах принятия решений». Proc. 5-й симпозиум ACM SIGACT-SIGPLAN по принципам языков программирования : 141–150. DOI : 10.1145 / 512760.512775 . S2CID  6342372 .
• Пресбургер, Mojżesz (1929). "Uber die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem ​​die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa : 92–101.английский перевод см. в Stansifer (1984).
• Стэнсифер, Райан (сентябрь 1984 г.). Статья Пресбургера о целочисленной арифметике: примечания и перевод (PDF) (Технический отчет). TR84-639. Итака / Нью-Йорк: факультет компьютерных наук Корнельского университета.
• Уильям Пью , 1991, « Омега-тест: быстрый и практичный алгоритм целочисленного программирования для анализа зависимостей ».
• Reddy, CR и DW Ловеланд, 1978, " Пресбургера Арифметика Bounded квантор Alternation. " ACM симпозиум по теории вычислений : 320-325.
• Янг П., 1985, "Теоремы Гёделя, экспоненциальная сложность и неразрешимость арифметических теорий: описание" в A. Nerode и R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Оппен, Дерек С. (1978). « Верхняя граница 2 ^{2 2 pn} сложности пресбургеровской арифметики». J. Comput. Syst. Sci . 16 (3): 323–332. DOI : 10.1016 / 0022-0000 (78) 90021-1 .
• Берман, Л. (1980). «Сложность логических теорий». Теоретическая информатика . 11 (1): 71–77. DOI : 10.1016 / 0304-3975 (80) 90037-7 .
• Нипков, Т. (2010). «Исключение линейного квантора» (PDF) . Журнал автоматизированных рассуждений . 45 (2): 189–212. DOI : 10.1007 / s10817-010-9183-0 . S2CID  14279141 .
• Король, Тим; Барретт, Кларк У .; Тинелли, Чезаре (2014). Использование линейного и смешанного целочисленного программирования для SMT . FMCAD . 2014 . С. 139–146. DOI : 10.1109 / FMCAD.2014.6987606 . ISBN 978-0-9835-6784-4. S2CID  5542629 .

Внешние ссылки [ править ]

• Полный инструмент доказательства теорем для арифметики Пресбургера Филиппа Рюммера