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

Разрешимая теория натуральных чисел первого порядка со сложением

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

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

Обзор

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

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

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

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

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

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

Характеристики

Пресбургер (1929) доказал, что арифметика Пресбургера следующая:

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

Разрешимость арифметики Пресбургера можно показать с помощью исключения кванторов , дополненного рассуждениями об арифметическом сравнении . ^{[2] [3] [4] [5] [6]} Шаги, используемые для обоснования алгоритма исключения кванторов, могут использоваться для определения вычислимых аксиоматизаций, которые не обязательно содержат схему аксиом индукции. ^{[2] [7]}

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

Вычислительная сложность

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

Более жесткая граница сложности была показана Берманом (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-полна. ^[8]
Для i > 0 и j > 2 PA(i + 1, j) является Σ _i ^P -полным . Для результата твердости требуется только j>2 (в отличие от j=1) в последнем блоке квантификатора.
Для i>0 PA(i+1) является Σ _i ^EXP -полным . ^[9]

Краткая арифметика Пресбургера ( ) полна (и, следовательно, NP полна для ). Здесь «короткий» требует ограниченного (т. е .) размера предложения, за исключением того, что целочисленные константы не ограничены (но их количество бит в двоичном формате учитывается в зависимости от размера ввода). Кроме того, две переменные PA (без ограничения на «короткость») являются NP-полными. ^[10] Короткий (и, следовательно , ) PA находится в P, и это распространяется на параметрическое целочисленное линейное программирование с фиксированной размерностью. ^[11] ${\displaystyle \Sigma _{n}}$ ${\displaystyle n>2}$ ${\displaystyle \Sigma _{n-2}^{P}}$ ${\displaystyle n=3}$ ${\displaystyle O(1)}$ ${\displaystyle \Sigma _{2}}$ ${\displaystyle \Pi _{2}}$ ${\displaystyle \Sigma _{2}}$

Приложения

Поскольку арифметика Пресбургера разрешима, существуют автоматические средства доказательства теорем для арифметики Пресбургера. Например, система помощника по доказательству Coq содержит тактическую омегу для арифметики Пресбургера, а помощник по доказательству Изабель содержит проверенную процедуру исключения квантора, предложенную Нипкоу (2010). Двойная экспоненциальная сложность теории делает невозможным использование средств доказательства теорем для сложных формул, но такое поведение происходит только при наличии вложенных кванторов: Нельсон и Оппен (1978) описывают автоматическое средство доказательства теорем, которое использует симплексный алгоритм на расширенном алгоритме. Арифметика Пресбургера без вложенных кванторов для доказательства некоторых примеров арифметических формул Пресбургера без кванторов. Более поздние решатели теорий выполнимости по модулю используют методы полного целочисленного программирования для обработки не кванторного фрагмента арифметической теории Пресбургера. ^[12]

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

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

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

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

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

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

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

Характеристика Мучника

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

Пусть множество, сечение , для и определяется как ${\displaystyle R\subseteq \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, для всех таких, что тогда тогда и только тогда, когда . При множество называется -периодическим в, если оно -периодично для некоторых таких, что ${\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},\dots ,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\leq 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}$

Смотрите также

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

Рекомендации

1. Zoethout 2015, с. 8, Теорема 1.2.4..
2. Пресбургер 1929.
3. Бючи 1962.
4. Монк 2012, с. 240.
5. Нипков 2010.
6. Эндертон 2001, с. 188.
7. Стэнсифер 1984.
8. Нгуен Луу 2018, глава 3.
9. Хаасе 2014, стр. 47:1-47:10.
10. Нгуен и Пак 2017.
11. Эйзенбранд и Шмонин 2008.
12. Кинг, Барретт и Тинелли 2014.
13. Например, в языке программирования C , если aэто массив размером 4 байта, выражение a[i]можно преобразовать в , что соответствует ограничениям арифметики Пресбургера.abaseadr+i+i+i+i
14. Гинзбург и Спэньер 1966, стр. 285–296.
15. Кобэм 1969, стр. 186–192.
16. Семенов 1977, стр. 403–418.
17. Мишо и Вильмер 1996, стр. 251–277.
18. Мучник 2003, стр. 1433–1444.

Библиография

• Берман, Л. (1980). «Сложность логических теорий». Теоретическая информатика . 11 (1): 71–77. дои : 10.1016/0304-3975(80)90037-7 .

• Бючи, Дж. Ричард (1962). «О методе принятия решения в ограниченной арифметике второго порядка». В Нагеле, Эрнест ; Суппес, Патрик ; Тарский, Альфред (ред.). Логика, методология и философия науки . Материалы Международного конгресса по логике. Стэнфорд: Издательство Стэнфордского университета . стр. 1–11.

• Кобэм, Алан (1969). «О зависимости от базы множеств чисел, распознаваемых конечными автоматами». Математика. Теория систем . 3 (2): 186–192. дои : 10.1007/BF01746527. S2CID  19792434.

• Купер, округ Колумбия (1972). Мельцер, Б.; Мичи, Д. (ред.). «Доказательство теоремы в арифметике без умножения» (PDF) . Машинный интеллект . Издательство Эдинбургского университета . 7 : 91–99.

• Эйзенбранд, Фридрих ; Шмонин, Геннадий (2008). «Параметрическое целочисленное программирование в фиксированном измерении». Математика исследования операций . 33 (4): 839–850. arXiv : 0801.4336 . дои : 10.1287/moor.1080.0320. S2CID  15698556.

• Эндертон, Герберт (2001). Математическое введение в логику (2-е изд.). Бостон, Массачусетс: Академическая пресса . ISBN 978-0-12-238452-3.

• Ферранте, Жанна ; Ракофф, Чарльз В. (1979). Вычислительная сложность логических теорий . Конспект лекций по математике. Том. 718. Шпрингер-Верлаг . дои : 10.1007/BFb0062837. ISBN 978-3-540-09501-9. МР  0537764.

• Фишер, Майкл Дж .; Рабин, Майкл О. (1974). «Суперэкспоненциальная сложность арифметики Пресбургера». В Карпе, Ричард М. (ред.). Сложность вычислений . Материалы SIAM-AMS. Том. 7. Американское математическое общество . стр. 27–41. ISBN 978-0-8218-1327-0. OCLC  1205569621. Архивировано из оригинала 15 сентября 2006 г. Проверено 11 июня 2006 г.

• Гинзбург, Сеймур ; Спаниер, Эдвин Генри (1966). «Полугруппы, формулы Пресбургера и языки». Тихоокеанский математический журнал . 16 (2): 285–296. дои : 10.2140/pjm.1966.16.285 .

• Хаазе, Кристоф (2014). «Подклассы арифметики Пресбургера и слабая иерархия опыта». Труды CSL- LICS . АКМ. стр. 47:1–47:10. arXiv : 1401.5266 . дои : 10.1145/2603088.2603092.

• Хаазе, Кристоф (2018). «Руководство по выживанию по арифметике Пресбургера» (PDF) . Новости ACM SIGLOG . 5 (3): 67–82. дои : 10.1145/3242953.3242964. S2CID  51847374.

• Кинг, Тим; Барретт, Кларк В.; Тинелли, Чезаре (2014). «Использование линейного и смешанного целочисленного программирования для SMT». 2014 Формальные методы в системе автоматизированного проектирования (FMCAD) . Том. 2014. С. 139–146. doi : 10.1109/FMCAD.2014.6987606. ISBN 978-0-9835-6784-4. S2CID  5542629.

• Мишо, Кристиан; Виллемайр, Роджер (1996). «Арифметика Пресбургера и распознаваемость множеств натуральных чисел автоматами: новые доказательства теорем Кобэма и Семенова». Анналы чистой и прикладной логики . 77 (3): 251–277. дои : 10.1016/0168-0072(95)00022-4.

• Монк, Дж. Дональд (2012). Математическая логика (Тексты для выпускников по математике (37)) (перепечатка оригинального 1-го издания 1976 г. в мягкой обложке). Спрингер. ISBN 9781468494549.

• Мучник, Андрей А. (2003). «Определимый критерий определимости в арифметике Пресбургера и ее приложениях». Теор. Вычислить. Наука . 290 (3): 1433–1444. дои : 10.1016/S0304-3975(02)00047-6 .

• Нельсон, Грег; Оппен, Дерек К. (апрель 1978 г.). «Упрощенец, основанный на эффективных алгоритмах принятия решений». Учеб. 5-й симпозиум ACM SIGACT-SIGPLAN по принципам языков программирования : 141–150. дои : 10.1145/512760.512775. S2CID  6342372.

• Нгуен, Дэнни; Пак, Игорь (2017). «Краткая арифметика Пресбургера сложна» (PDF) . 58-й ежегодный симпозиум IEEE по основам информатики (FOCS) , 2017 г. стр. 37–48. arXiv : 1708.08179 . дои : 10.1109/FOCS.2017.13. ISBN 978-1-5386-3464-6. S2CID  3425421 . Проверено 4 сентября 2022 г.

• Нгуен Луу, Дан (2018). Вычислительная сложность арифметики Пресбургера (Диссертация). Лос-Анджелес: Электронные диссертации и диссертации Калифорнийского университета в Лос-Анджелесе . Проверено 8 сентября 2022 г.

• Нипков, Т (2010). «Устранение линейного квантификатора» (PDF) . Журнал автоматизированного рассуждения . 45 (2): 189–212. дои : 10.1007/s10817-010-9183-0. S2CID  14279141.

• Оппен, Дерек К. (1978). «Верхняя граница сложности арифметики Пресбургера 222pn». Дж. Компьютер. Сист. наук. 16 (3): 323–332. дои : 10.1016/0022-0000(78)90021-1 .

• Пресбургер, Мойжес (1929). «Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, в welchem ​​die Additions als einzige Operation hervortritt». Comptes Rendus du I congrès de Mathématiciens de Pays Slaves, Варшава : 92–101.английский перевод см. в Stansifer (1984).

• Пью, Уильям (1991). «Тест Омега: быстрый и практичный алгоритм целочисленного программирования для анализа зависимостей». Материалы конференции ACM/IEEE 1991 года по суперкомпьютерам — Supercomputing '91 . Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 4–13. CiteSeerX  10.1.1.37.1995 . дои : 10.1145/125826.125848. ISBN 0897914597. S2CID  3174094.

• Редди, ЧР; Лавленд, Д.В. (1978). «Арифметика Пресбургера с ограниченным чередованием кванторов». Материалы десятого ежегодного симпозиума ACM по теории вычислений - STOC '78 . Симпозиум ACM по теории вычислений . стр. 320–325. дои : 10.1145/800133.804361. S2CID  13966721.

• Семенов А.Л. (1977). «Пресбургерность предикатов, регулярных в двух системах счисления». Сибирск. Мат. Ж. (на русском). 18 : 403–418.

• Стэнсифер, Райан (сентябрь 1984 г.). Статья Пресбургера о целочисленной арифметике: замечания и перевод (PDF) (технический отчет). Том. ТР84-639. Итака/Нью-Йорк: Факультет компьютерных наук Корнельского университета.

• Янг, П. (1985). «Теоремы Гёделя, экспоненциальная сложность и неразрешимость арифметических теорий: изложение». В А. Нероде и Р. Шоре (ред.). Теория рекурсии, Американское математическое общество . стр. 503–522.

• Зутаут, Джетце (1 февраля 2015 г.). Интерпретации в арифметике Пресбургера (бакалаврская диссертация) (PDF) (Диссертация) . Проверено 25 августа 2023 г.

Внешние ссылки

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