Presburger Arithmetik - Presburger arithmetic

Die Presburger Arithmetik ist die Theorie erster Ordnung der natürlichen Zahlen mit Addition , benannt nach Mojżesz Presburger , der sie 1929 einführte. Die Signatur der Presburger Arithmetik enthält nur die Additionsoperation und die Gleichheit , die Multiplikationsoperation ganz weggelassen . Die Axiome beinhalten ein Induktionsschema .

Die Presburger-Arithmetik ist viel schwächer als die Peano-Arithmetik , die sowohl Additions- als auch Multiplikationsoperationen umfasst. Im Gegensatz zur Peano-Arithmetik ist die Presburger-Arithmetik eine entscheidbare Theorie . Dies bedeutet, dass für jeden Satz in der Sprache der Presburger Arithmetik algorithmisch bestimmt werden kann, ob dieser Satz aus den Axiomen der Presburger Arithmetik beweisbar ist. Die asymptotische Laufzeit- Rechenkomplexität dieses Algorithmus ist jedoch mindestens doppelt exponentiell , wie von Fischer & Rabin (1974) gezeigt wurde .

Überblick

Die Sprache der Presburger Arithmetik enthält die Konstanten 0 und 1 und eine binäre Funktion +, interpretiert als Addition.

In dieser Sprache sind die Axiome der Presburger Arithmetik die universellen Abschlüsse des Folgenden:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + ( y + 1) = ( x + y ) + 1
5. Sei P ( x ) eine Formel erster Ordnung in der Sprache der Presburger Arithmetik mit einer freien Variablen x (und möglicherweise anderen freien Variablen). Dann ist die folgende Formel ein Axiom:
   ( P (0) x ( P ( x ) → P ( x + 1))) → y P ( y ).

(5) ist ein Axiomenschema der Induktion , das unendlich viele Axiome repräsentiert. Diese können durch keine endliche Anzahl von Axiomen ersetzt werden, dh die Presburger Arithmetik ist in der Logik erster Ordnung nicht endlich axiomatisierbar.

Die Presburger Arithmetik kann als Theorie erster Ordnung mit Gleichheit angesehen werden, die genau alle Konsequenzen der obigen Axiome enthält. Alternativ kann es als die Menge der Sätze definiert werden, die in der beabsichtigten Interpretation wahr sind : die Struktur von nicht-negativen ganzen Zahlen mit Konstanten 0, 1 und die Addition von nicht-negativen ganzen Zahlen.

Presburger Arithmetik ist vollständig und entscheidbar. Daher kann es keine Konzepte wie Teilbarkeit oder Primalität formalisieren oder allgemeiner irgendein Zahlenkonzept , das zur Multiplikation von Variablen führt. Sie kann jedoch einzelne Fälle der Teilbarkeit formulieren; zum Beispiel beweist es "für alle x existiert y  : ( y + y = x ) ∨ ( y + y + 1 = x )". Dies besagt, dass jede Zahl entweder gerade oder ungerade ist.

Eigenschaften

Mojżesz Presburger bewies Presburger Arithmetik:

• konsistent : Es gibt keine Aussage in der Presburger Arithmetik, die aus den Axiomen abgeleitet werden kann, so dass auch ihre Negation abgeleitet werden kann.
• vollständig : Für jede Aussage in der Sprache der Presburger Arithmetik kann man sie entweder aus den Axiomen ableiten oder ihre Negation ableiten.
• entscheidbar : Es gibt einen Algorithmus, der entscheidet, ob eine gegebene Aussage in der Presburger Arithmetik ein Satz oder ein Nichtsatz ist.

Die Entscheidbarkeit der Presburger Arithmetik lässt sich durch die Quantoreneliminierung zeigen , ergänzt durch die Argumentation zur arithmetischen Kongruenz ( Presburger (1929) , Nipkow (2010) , Enderton 2001, S. 188). Die Schritte zur Begründung eines Quantoreneliminationsalgorithmus können verwendet werden, um rekursive Axiomatisierungen zu definieren, die nicht notwendigerweise das Axiomenschema der Induktion enthalten ( Presburger (1929) , Stansifer (1984) ).

Im Gegensatz dazu ist Peano-Arithmetik , also Presburger-Arithmetik mit Multiplikation, nicht entscheidbar, als Folge der negativen Antwort auf das Entscheidungsproblem . Nach Gödels Unvollständigkeitssatz ist die Peano-Arithmetik unvollständig und ihre Konsistenz nicht intern beweisbar (siehe aber Gentzens Konsistenzbeweis ).

Rechenkomplexität

Das Entscheidungsproblem für die Presburger Arithmetik ist ein interessantes Beispiel in der Computational Complexity Theory and Computation . Sei n die Länge einer Aussage in der Presburger Arithmetik. Dann bewiesen Fischer und Rabin (1974), dass der Beweis der Aussage in der Logik erster Ordnung im schlimmsten Fall für eine Konstante c > 0 mindestens eine Länge hat . Daher hat ihr Entscheidungsalgorithmus für die Presburger-Arithmetik mindestens eine exponentielle Laufzeit. Fischer und Rabin haben auch bewiesen, dass es für jede vernünftige Axiomatisierung (in ihrer Arbeit genau definiert) Sätze der Länge n gibt , die doppelt exponentielle Längenbeweise haben. Intuitiv deutet dies darauf hin, dass es rechnerische Grenzen für das gibt, was durch Computerprogramme nachgewiesen werden kann. Die Arbeit von Fischer und Rabin impliziert auch, dass Presburger-Arithmetik verwendet werden kann, um Formeln zu definieren, die jeden Algorithmus korrekt berechnen, solange die Eingaben kleiner als relativ große Grenzen sind. Die Grenzen können erhöht werden, aber nur durch die Verwendung neuer Formeln. Andererseits wurde von Oppen (1978) eine dreifach exponentielle Obergrenze eines Entscheidungsverfahrens für die Presburger Arithmetik bewiesen. ${\displaystyle 2^{2^{cn}}}$

Eine engere Komplexitätsgrenze wurde von Berman (1980) unter Verwendung alternierender Komplexitätsklassen gezeigt . Die Menge der wahren Aussagen in der Presburger Arithmetik (PA) wird für TimeAlternations (2 ^{2 n O(1)} , n) vollständig gezeigt . Somit liegt seine Komplexität zwischen der doppelten exponentiellen nichtdeterministischen Zeit (2-NEXP) und dem doppelten exponentiellen Raum (2-EXPSPACE). Vollständigkeit ist unter polynomieller Zeit-viele-zu-eins-Reduktionen. (Beachten Sie auch, dass die Presburger-Arithmetik zwar allgemein mit PA abgekürzt wird, in der Mathematik jedoch im Allgemeinen PA normalerweise Peano-Arithmetik bedeutet .)

Für ein feineres Ergebnis sei PA(i) die Menge der wahren _i PA-Anweisungen und PA(i, j) die Menge der wahren Σ _i PA-Anweisungen, wobei jeder Quantifiziererblock auf j Variablen beschränkt ist. '<' gilt als quantifiziererfrei; hier werden beschränkte Quantoren als Quantoren gezählt.
PA(1, j) ist in P, während PA(1) NP-vollständig ist.
Für i > 0 und j > 2 ist PA(i + 1, j) Σ _i ^P -vollständig . Das Härteergebnis benötigt nur im letzten Quantorenblock j>2 (im Gegensatz zu j=1).
Für i>0 ist PA(i+1) Σ _i ^EXP -vollständig (und ist TimeAlternations(2 ^{n O(i)} , i)-vollständig).

Anwendungen

Da die Presburger Arithmetik entscheidbar ist, existieren automatische Theorembeweiser für die Presburger Arithmetik. Zum Beispiel enthält das Coq- Beweisassistentensystem das taktische Omega für die Presburger-Arithmetik und der Isabelle-Beweisassistent enthält ein verifiziertes Quantoren-Eliminationsverfahren von Nipkow (2010) . Die doppelte exponentielle Komplexität der Theorie macht es unmöglich, die Theorembeweiser auf komplizierte Formeln anzuwenden, aber dieses Verhalten tritt nur in Gegenwart von verschachtelten Quantoren auf: Oppen und Nelson (1980) beschreiben einen automatischen Theorembeweiser, der den Simplexalgorithmus auf einem erweiterten Presburger Arithmetik ohne verschachtelte Quantoren, um einige der Fälle von quantifiziererfreien Presburger arithmetischen Formeln zu beweisen. Neuere Erfüllbarkeits-Modulo-Theorien- Löser verwenden vollständige ganzzahlige Programmiertechniken , um ein quantifiziererfreies Fragment der Presburger Arithmetiktheorie zu handhaben ( King, Barrett & Tinelli (2014) ).

Die Presburger-Arithmetik kann um die Multiplikation mit Konstanten erweitert werden, da die Multiplikation eine wiederholte Addition ist. Die meisten Array-Indexberechnungen fallen dann in den Bereich entscheidbarer Probleme. Dieser Ansatz ist die Grundlage von mindestens fünf Korrektheitsnachweissystemen für Computerprogramme , beginnend mit dem Stanford Pascal Verifier in den späten 1970er Jahren bis hin zu Microsofts Spec#-System von 2005.

Presburger-definierbare Integer-Relation

Einige Eigenschaften über ganzzahlige Beziehungen, die in der Presburger Arithmetik definierbar sind, werden nun angegeben . Der Einfachheit halber sind alle in diesem Abschnitt betrachteten Beziehungen über nicht-negativen ganzen Zahlen.

Eine Relation ist genau dann Presburger-definierbar, wenn sie eine semilineare Menge ist .

Eine unäre ganzzahlige Relation , also eine Menge nicht-negativer ganzer Zahlen, ist genau dann Presburger-definierbar, wenn sie letztlich periodisch ist. Das heißt, wenn ein Schwellenwert existiert und eine positive Periode , so dass für alle integer , so dass , wenn und nur wenn . ${\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}$

Nach dem Cobham-Semenov-Theorem ist eine Relation genau dann Presburger-definierbar, wenn sie in der Büchi-Arithmetik der Basis für alle definierbar ist . Eine Beziehung in definierbaren Büchi Arithmetik der Basis und für und wobei multiplikativ unabhängige ganze Zahlen ist Presburger definierbar. ${\displaystyle k}$${\displaystyle k\geq 2}$${\displaystyle k}$${\displaystyle k'}$${\displaystyle k}$${\displaystyle k'}$

Eine ganzzahlige Relation ist genau dann Presburger-definierbar, wenn alle Mengen von ganzen Zahlen, die in der Logik erster Ordnung mit Addition definierbar sind und (d. h. Presburger Arithmetik plus ein Prädikat für ) Presburger-definierbar sind. Äquivalent existiert für jede Relation, die nicht Presburger-definierbar ist, eine Formel erster Ordnung mit Addition, die eine Menge von ganzen Zahlen definiert, die nicht nur durch Addition definierbar ist. ${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$

Muchniks Charakterisierung

Presburger-definierbare Relationen erlauben eine andere Charakterisierung: durch den Satz von Muchnik. Es ist komplizierter zu sagen, führte aber zum Beweis der beiden früheren Charakterisierungen. Bevor der Satz von Muchnik aufgestellt werden kann, müssen einige zusätzliche Definitionen eingeführt werden.

Sei eine Menge, der Abschnitt von , for und ist definiert als ${\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\}.}$

Gegeben seien zwei Sätze und eine tupel von ganzen Zahlen , die Menge wird als periodischer in , wenn für alle , so dass dann , wenn und nur wenn . Für die Menge wird gesagt, dass periodischer in , wenn es periodischer für einige , so dass ${\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.}$

Schließlich, für lass ${\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\}}$

bezeichnen den Würfel der Größe, dessen kleinere Ecke ist . ${\displaystyle k}$${\displaystyle (x_{0},\dots,x_{d-1})}$

Intuitiv repräsentiert die ganze Zahl die Länge einer Verschiebung, die ganze Zahl ist die Größe der Würfel und ist der Schwellenwert vor der Periodizität. Dieses Ergebnis bleibt wahr, wenn die Bedingung ${\displaystyle s}$${\displaystyle k}$${\displaystyle t}$

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

wird entweder durch oder durch ersetzt . ${\displaystyle \min(x_{0},\ldots,x_{d-1})>t}$${\displaystyle \max(x_{0},\ldots,x_{d-1})>t}$

Diese Charakterisierung führte zu dem sogenannten "definierbaren Kriterium für Definierbarkeit in der Presburger Arithmetik", d. h.: es existiert eine Formel erster Ordnung mit Addition und ein -äres Prädikat, das genau dann gilt, wenn es durch eine Presburger-definierbare Relation interpretiert wird. Mit dem Satz von Muchnik kann man auch beweisen, dass es entscheidbar ist, ob eine automatische Folge eine Presburger-definierbare Menge akzeptiert. ${\displaystyle d}$${\displaystyle R}$${\displaystyle R}$

Siehe auch

• Robinson-Arithmetik
• Skolem-Arithmetik

Verweise

• Haase, Christoph (2018). "Ein Überlebensratgeber für die Presburger-Arithmetik" . ACM SIGLOG-Neuigkeiten . 5 (3): 67–82. doi : 10.1145/3242953.3242964 . S2CID  51847374 .
• Cooper, DC, 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer und D. Michie, Hrsg., Machine Intelligence Vol. 2 , No. 7 . Edinburgh University Press: 91-99.
• Enderton, Herbert (2001). Eine mathematische Einführung in die Logik (2. Aufl.). Boston, MA: Akademische Presse . ISBN 978-0-12-238452-3.
• Ferrante, Jeanne und Charles W. Rackoff, 1979. Die rechnerische Komplexität logischer Theorien . Skript zur Vorlesung Mathematik 718. Springer-Verlag .
• Fischer, Michael J. ; Rabin, Michael O. (1974). "Superexponentielle Komplexität der Presburger Arithmetik" . Tagungsband des SIAM-AMS Symposiums in Angewandter Mathematik . 7 : 27–41. Archiviert vom Original am 15.09.2006 . Abgerufen 2006-06-11 .
• G. Nelson und DC Oppen (April 1978). „Ein Vereinfacher basierend auf effizienten Entscheidungsalgorithmen“. Proz. 5. ACM SIGACT-SIGPLAN Symposium über Prinzipien der Programmiersprachen : 141–150. doi : 10.1145/512760.512775 . S2CID  6342372 .
• Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welcher die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa : 92–101., siehe Stansifer (1984) für eine englische Übersetzung
• Stansifer, Ryan (September 1984). Presburgers Artikel über Integer Arithmetic: Remarks and Translation (PDF) (Technical Report). TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.
• William Pugh , 1991, „ Der Omega-Test: ein schneller und praktischer ganzzahliger Programmieralgorithmus für die Abhängigkeitsanalyse “.
• Reddy, CR, und DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation ". ACM Symposium on Theory of Computing : 320–325.
• Young, P., 1985, "Gödel-Theorems, exponentielle Schwierigkeit und Unentscheidbarkeit von arithmetischen Theorien: eine Exposition" in A. Nerode und R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Oppen, Derek C. (1978). "A 2 ^{2 2 pn} Upper Bound on the Complexity of Presburger Arithmetic" . J. Computer. Syst. Sci . 16 (3): 323–332. doi : 10.1016/0022-0000(78)90021-1 .
• Berman, L. (1980). „Die Komplexität logischer Theorien“ . Theoretische Informatik . 11 (1): 71–77. doi : 10.1016/0304-3975(80)90037-7 .
• Nipkow, T (2010). "Eliminierung linearer Quantoren" (PDF) . Zeitschrift für automatisiertes Denken . 45 (2): 189–212. doi : 10.1007/s10817-010-9183-0 . S2CID  14279141 .
• König, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). „Nutzung der linearen und gemischten Integer-Programmierung für SMT“. 2014 Formale Methoden im Computer-Aided Design (FMCAD) . 2014 . S. 139–146. doi : 10.1109/FMCAD.2014.6987606 . ISBN 978-0-9835-6784-4. S2CID  5542629 .

Externe Links

• Ein vollständiger Theorembeweiser für Presburger Arithmetik von Philipp Rümmer