Arithmétique de Presburger - Presburger arithmetic

L'arithmétique de Presburger est la théorie du premier ordre des nombres naturels avec addition , nommée en l'honneur de Mojżesz Presburger , qui l'a introduite en 1929. La signature de l'arithmétique de Presburger ne contient que l'opération d'addition et l' égalité , en omettant entièrement l'opération de multiplication . Les axiomes comportent un schéma d' induction .

L'arithmétique de Presburger est beaucoup plus faible que l'arithmétique de Peano , qui comprend à la fois des opérations d'addition et de multiplication. Contrairement à l'arithmétique de Peano, l'arithmétique de Presburger est une théorie décidable . Cela signifie qu'il est possible de déterminer algorithmiquement, pour toute phrase dans la langue de l'arithmétique de Presburger, si cette phrase est prouvable à partir des axiomes de l'arithmétique de Presburger. La complexité de calcul en temps d'exécution asymptotique de cet algorithme est cependant au moins doublement exponentielle , comme l'ont montré Fischer & Rabin (1974) .

Aperçu

Le langage de l'arithmétique de Presburger contient des constantes 0 et 1 et une fonction binaire +, interprétée comme une addition.

Dans cette langue, les axiomes de l'arithmétique de Presburger sont les fermetures universelles des éléments suivants :

1. (0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + ( y + 1) = ( x + y ) + 1
5. Soit P ( x ) une formule du premier ordre dans le langage de l'arithmétique de Presburger avec une variable libre x (et éventuellement d'autres variables libres). Alors la formule suivante est un axiome :
   ( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y ).

(5) est un schéma d'axiome d' induction , représentant une infinité d'axiomes. Ceux-ci ne peuvent pas être remplacés par un nombre fini d'axiomes, c'est-à-dire que l'arithmétique de Presburger n'est pas finiment axiomatisable en logique du premier ordre.

L'arithmétique de Presburger peut être considérée comme une théorie du premier ordre avec une égalité contenant précisément toutes les conséquences des axiomes ci-dessus. Alternativement, il peut être défini comme l'ensemble des phrases qui sont vraies dans l' interprétation envisagée : la structure des nombres entiers non négatifs avec des constantes 0, 1 et l'addition des nombres entiers non négatifs.

L'arithmétique Presburger est conçue pour être complète et décidable. Par conséquent, il ne peut formaliser des concepts tels que la divisibilité ou la primalité , ou, plus généralement, tout concept de nombre conduisant à la multiplication de variables. Cependant, il peut formuler des cas individuels de divisibilité ; par exemple, cela prouve "pour tout x , il existe y  : ( y + y = x ) ∨ ( y + y + 1 = x )". Cela indique que chaque nombre est pair ou impair.

Propriétés

Mojżesz Presburger a prouvé que l'arithmétique de Presburger était :

• cohérent : Il n'y a pas d'énoncé dans l'arithmétique de Presburger qui puisse être déduit des axiomes de telle sorte que sa négation puisse également être déduite.
• complet : Pour chaque énoncé dans le langage de l'arithmétique de Presburger, soit il est possible de le déduire des axiomes, soit il est possible d'en déduire sa négation.
• décidable : Il existe un algorithme qui décide si un énoncé donné en arithmétique de Presburger est un théorème ou un non-théorème.

La décidabilité de l'arithmétique de Presburger peut être démontrée en utilisant l'élimination par quantificateur , complétée par un raisonnement sur la congruence arithmétique ( Presburger (1929) , Nipkow (2010) , Enderton 2001, p. 188). Les étapes utilisées pour justifier un algorithme d'élimination de quantificateur peuvent être utilisées pour définir des axiomatisations récursives qui ne contiennent pas nécessairement le schéma d'axiome de l'induction ( Presburger (1929) , Stansifer (1984) ).

En revanche, l'arithmétique de Peano , qui est l'arithmétique de Presburger augmentée d'une multiplication, n'est pas décidable, en raison de la réponse négative au problème Entscheidungs . Par le théorème d'incomplétude de Gödel , l'arithmétique de Peano est incomplète et sa cohérence n'est pas prouvable en interne (mais voir la preuve de cohérence de Gentzen ).

Complexité de calcul

Le problème de décision pour l'arithmétique de Presburger est un exemple intéressant dans la théorie de la complexité computationnelle et le calcul . Soit n la longueur d'une instruction en arithmétique de Presburger. Ensuite, Fischer et Rabin (1974) ont prouvé que, dans le pire des cas, la preuve de l'énoncé en logique du premier ordre a une longueur d'au moins , pour une constante c >0. Par conséquent, leur algorithme de décision pour l'arithmétique de Presburger a un temps d'exécution au moins exponentiel. Fischer et Rabin ont également prouvé que pour toute axiomatisation raisonnable (définie précisément dans leur article), il existe des théorèmes de longueur n qui ont des preuves de longueur doublement exponentielles . Intuitivement, cela suggère qu'il existe des limites de calcul à ce qui peut être prouvé par des programmes informatiques. Les travaux de Fischer et Rabin impliquent également que l'arithmétique de Presburger peut être utilisée pour définir des formules qui calculent correctement n'importe quel algorithme tant que les entrées sont inférieures à des limites relativement grandes. Les bornes peuvent être augmentées, mais uniquement en utilisant de nouvelles formules. D'autre part, une borne supérieure triplement exponentielle sur une procédure de décision pour l'arithmétique de Presburger a été prouvée par Oppen (1978). ${\displaystyle 2^{2^{cn}}}$

Une borne de complexité plus étroite a été montrée en utilisant des classes de complexité alternées par Berman (1980) . L'ensemble des déclarations vraies dans l'arithmétique de Presburger (PA) est montré complet pour TimeAlternations (2 ^{2 n O(1)} , n). Ainsi, sa complexité se situe entre le temps non déterministe exponentiel double (2-NEXP) et l'espace exponentiel double (2-EXPSPACE). La complétude est soumise à des réductions plusieurs à un en temps polynomial. (En outre, notez que si l'arithmétique de Presburger est communément abrégée PA, en mathématiques en général PA signifie généralement arithmétique de Peano .)

Pour un résultat plus précis, soit PA(i) l'ensemble des vraies déclarations Σ _i PA, et PA(i, j) l'ensemble des vraies déclarations Σ _i PA avec chaque bloc quantificateur limité à j variables. '<' est considéré comme sans quantificateur ; ici, les quantificateurs bornés sont comptés comme des quantificateurs.
PA(1, j) est dans P, tandis que PA(1) est NP-complet.
Pour i > 0 et j > 2, PA(i + 1, j) est Σ _i ^P -complet . Le résultat de dureté n'a besoin que de j>2 (par opposition à j=1) dans le dernier bloc du quantificateur.
Pour i>0, PA(i+1) est Σ _i ^EXP -complet (et TimeAlternations(2 ^{n O(i)} , i)-complet).

Applications

Parce que l'arithmétique de Presburger est décidable, il existe des prouveurs de théorèmes automatiques pour l'arithmétique de Presburger. Par exemple, le système d'assistant de preuve Coq comprend la tactique oméga pour l'arithmétique de Presburger et l' assistant de preuve Isabelle contient une procédure d'élimination de quantificateur vérifiée par Nipkow (2010) . La double complexité exponentielle de la théorie rend infaisable l'utilisation des prouveurs de théorèmes sur des formules compliquées, mais ce comportement ne se produit qu'en présence de quantificateurs imbriqués : Oppen et Nelson (1980) décrivent un prouveur de théorèmes automatique qui utilise l' algorithme du simplexe sur un Arithmétique de Presburger sans quantificateurs imbriqués pour prouver certaines des instances de formules arithmétiques de Presburger sans quantificateur. Les solveurs de théories modulo de satisfiabilité plus récentes utilisent des techniques de programmation en nombres entiers complètes pour gérer un fragment sans quantificateur de la théorie arithmétique de Presburger ( King, Barrett & Tinelli (2014) ).

L'arithmétique de Presburger peut être étendue pour inclure la multiplication par des constantes, puisque la multiplication est une addition répétée. La plupart des calculs d'indice de tableau tombent alors dans la région des problèmes décidables. Cette approche est à la base d'au moins cinq systèmes de preuve d' exactitude pour les programmes informatiques , en commençant par le Stanford Pascal Verifier à la fin des années 1970 et en continuant jusqu'au système Spec# de Microsoft de 2005.

Relation entière définissable par Presburger

Certaines propriétés sont maintenant données sur les relations entières définissables dans l'arithmétique de Presburger. Par souci de simplicité, toutes les relations considérées dans cette section sont sur des entiers non négatifs.

Une relation est définissable par Presburger si et seulement si c'est un ensemble semi - linéaire .

Une relation entière unaire , c'est-à-dire un ensemble d'entiers non négatifs, est définissable par Presburger si et seulement si elle est finalement périodique. C'est-à-dire s'il existe un seuil et une période positive tels que, pour tout entier tel que , si et seulement si . ${\style d'affichage R}$${\displaystyle t\in \mathbb {N} }$${\displaystyle p\in \mathbb {N} ^{>0}}$${\style d'affichage n}$${\style d'affichage |n|\geq t}$${\style d'affichage n\dans R}$${\style d'affichage n+p\dans R}$

D'après le théorème de Cobham-Semenov , une relation est définissable par Presburger si et seulement si elle est définissable dans l'arithmétique de Büchi de base pour tout . Une relation définissable dans l'arithmétique de Büchi de base et pour et étant des nombres entiers multiplicativement indépendants est définissable de Presburger. ${\style d'affichage k}$${\displaystyle k\geq 2}$${\style d'affichage k}$${\style d'affichage k'}$${\style d'affichage k}$${\style d'affichage k'}$

Une relation entière est définissable par Presburger si et seulement si tous les ensembles d'entiers définissables dans la logique du premier ordre avec addition et (c'est-à-dire, l'arithmétique Presburger plus un prédicat pour ) sont définissables par Presburger. De manière équivalente, pour chaque relation qui n'est pas définissable par Presburger, il existe une formule du premier ordre avec addition et qui définit un ensemble d'entiers qui n'est pas définissable par la seule addition. ${\style d'affichage R}$${\style d'affichage R}$${\style d'affichage R}$${\style d'affichage R}$${\style d'affichage R}$

Caractérisation de Muchnik

Les relations définissables par Presburger admettent une autre caractérisation : par le théorème de Muchnik. Elle est plus compliquée à énoncer, mais a conduit à la preuve des deux caractérisations précédentes. Avant de pouvoir énoncer le théorème de Muchnik, quelques définitions supplémentaires doivent être introduites.

Soit un ensemble, la section de , pour et est définie comme ${\displaystyle R\subseteq \mathbb {N} ^{d}}$${\style d'affichage x_{i}=j}$${\style d'affichage R}$${\style d'affichage 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\}.}$

Étant donné deux ensembles et un -uplet d'entiers , l'ensemble est appelé -périodique dans si, pour tout tel que alors si et seulement si . Pour , l'ensemble est dit -périodique dans s'il est -périodique pour certains tels que ${\displaystyle R,S\subseteq \mathbb {N} ^{d}}$${\style d'affichage d}$${\displaystyle (p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}}$${\style d'affichage R}$${\style d'affichage (p_{0},\dots ,p_{d-1})}$${\style d'affichage S}$${\displaystyle (x_{0},\dots ,x_{d-1})\in S}$${\style d'affichage (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,}$${\displaystyle (x_{0},\ldots ,x_{d-1})\in R}$${\style d'affichage (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R}$${\displaystyle s\in \mathbb {N} }$${\style d'affichage R}$${\style d'affichage s}$${\style d'affichage S}$${\style d'affichage (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.}$

Enfin, pour laisser ${\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\}}$

désigne le cube de taille dont le petit coin est . ${\style d'affichage k}$${\style d'affichage (x_{0},\dots ,x_{d-1})}$

Intuitivement, l'entier représente la longueur d'un décalage, l'entier est la taille des cubes et est le seuil avant la périodicité. Ce résultat reste vrai lorsque la condition ${\style d'affichage s}$${\style d'affichage k}$${\style d'affichage t}$

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

est remplacé par ou par . ${\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}$${\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}$

Cette caractérisation a conduit à ce que l'on appelle le « critère définissable de définissabilité en arithmétique de Presburger », c'est-à-dire qu'il existe une formule du premier ordre avec addition et un prédicat -aire qui est valable si et seulement si est interprété par une relation définissable de Presburger. Le théorème de Muchnik permet également de prouver qu'il est décidable si une séquence automatique accepte un ensemble définissable par Presburger. ${\style d'affichage d}$${\style d'affichage R}$${\style d'affichage R}$

Voir également

• arithmétique de Robinson
• Arithmétique Skolem

Les références

• Haase, Christoph (2018). "Un guide de survie à l'arithmétique presburger" . Actualités ACM SIGLOG . 5 (3) : 67-82. doi : 10.1145/3242953.3242964 . S2CID  51847374 .
• Cooper, DC, 1972, "Theorem Proving in Arithmetic without Multiplication" dans B. Meltzer et D. Michie, eds., Machine Intelligence Vol. 7 . Presse universitaire d'Édimbourg : 91-99.
• Enderton, Herbert (2001). Une introduction mathématique à la logique (2e éd.). Boston, MA : Presse académique . ISBN 978-0-12-238452-3.
• Ferrante, Jeanne et Charles W. Rackoff, 1979. La complexité computationnelle des théories logiques . Notes de cours en mathématiques 718. Springer-Verlag .
• Fischer, Michael J. ; Rabin, Michael O. (1974). « Complexité super-exponentielle de l'arithmétique de Presburger » . Actes du Symposium SIAM-AMS en Mathématiques Appliquées . 7 : 27-41. Archivé de l'original le 2006-09-15 . Récupéré le 2006-06-11 .
• G. Nelson et DC Oppen (avril 1978). « Un simplificateur basé sur des algorithmes de décision efficaces ». Proc. 5ème Symposium ACM SIGACT-SIGPLAN sur les principes des langages de programmation : 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 welchem ​​die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Esclaves, Varsovie : 92-101., voir Stansifer (1984) pour une traduction anglaise
• Stansifer, Ryan (septembre 1984). Article de Presburger sur l'arithmétique des entiers : remarques et traduction (PDF) (rapport technique). TR84-639. Ithaca/NY : Département d'informatique, Université Cornell.
• William Pugh , 1991, " Le test Omega : un algorithme de programmation en nombres entiers rapide et pratique pour l'analyse de dépendance ".
• Reddy, CR et DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation. " Symposium ACM sur la théorie de l'informatique : 320-325.
• Young, P., 1985, "Théorèmes de Gödel, difficulté exponentielle et indécidabilité des théories arithmétiques: une exposition" dans A. Nerode et R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Oppen, Derek C. (1978). "Une ^borne supérieure 2 ^{2 2 pn} sur la complexité de l'arithmétique de Presburger" . J. Informatique. Syst. Sci . 16 (3) : 323-332. doi : 10.1016/0022-0000(78)90021-1 .
• Berman, L. (1980). "La complexité des théories logiques" . Informatique théorique . 11 (1) : 71-77. doi : 10.1016/0304-3975(80)90037-7 .
• Nipkow, T (2010). « Élimination du quantificateur linéaire » (PDF) . Journal de raisonnement automatisé . 45 (2) : 189-212. doi : 10.1007/s10817-010-9183-0 . S2CID  14279141 .
• Roi, Tim; Barrett, Clark W.; Tinelli, César (2014). « Tirer parti de la programmation en nombres entiers linéaires et mixtes pour SMT ». 2014 Méthodes Formelles en Conception Assistée par Ordinateur (FMCAD) . 2014 . pp. 139-146. doi : 10.1109/FMCAD.2014.6987606 . ISBN 978-0-9835-6784-4. S2CID  5542629 .

Liens externes

• Un prouveur de théorème complet pour l'arithmétique de Presburger par Philipp Rümmer