Arithmétique de Presburger

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Pressburger.

L'arithmétique de Presburger est la théorie du premier ordre des nombres entiers naturels munis de l'addition. Elle a été introduite en 1929 par Mojżesz Presburger.

Il s'agit de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition, en plus du zéro et de l'opération successeur.

Définition[modifier | modifier le code]

Le langage de l'arithmétique de Presburger contient les constantes 0 et 1, le symbole de fonction binaire +. L'arithmétique est définie par les axiomes suivants :

  1. x, ¬(0 = x + 1)
  2. x,∀y, x + 1 = y + 1 → x = y
  3. x, x + 0 = x
  4. x, ∀y, x + (y + 1) = (x + y) + 1
  5. Pour toute formule P(x, y1, …, yn) du premier-ordre sur le langage de l'arithmétique de Presburger avec x, y1, …, yn comme variables libres, la formule suivante est un axiome : ∀y1…∀yn [(P(0, y1, …, yn) ∧ ∀x(P(x, y1, …, yn) → P(x + 1, y1, …, yn))) → ∀y P(y, y1, …, yn)].

(5) est le schéma d'induction et c'est un ensemble infini d'axiomes. On peut montrer que l'arithmétique de Presburger n'est pas finiment axiomatisable en logique du premier ordre.

L'arithmétique de Peano est définie sur le langage de l'arithmétique de Presburger avec en plus un symbole de fonction binaire ×. L'arithmétique de Peano contient des axiomes supplémentaires.

Propriétés[modifier | modifier le code]

Mojżesz Presburger a démontré en 1929 que son arithmétique, qui est cohérente[1], est complète[2]. Comme une théorie axiomatique récursivement axiomatisable et complète est décidable, on en déduit l'existence d'un algorithme qui décide, au vu d'une proposition du langage de l'arithmétique de Presburger, si celle-ci est démontrable ou non.

Contrairement à l'arithmétique de Presburger, l'arithmétique de Peano n'est pas complète en vertu du théorème d'incomplétude de Gödel. L'arithmétique de Peano n'est pas décidable (voir problème de la décision).

Algorithmes[modifier | modifier le code]

En revanche, Michael J. Fisher et Michael O. Rabin ont démontré que le problème de décision a une complexité intrinsèque doublement exponentielle, c'est-à-dire que le problème de décision est 2EXPTIME-dur, ce qui devrait rendre tout algorithme inefficace[3].

Il existe une procédure de décision non élémentaire reposant sur la théorie des automates finis[4].

Oppen en 1978 a donné un algorithme triplement exponentiel[5]. Bergman en 1980 donne des résultats de complexité plus précis en utilisant des machines alternantes[6].

En pratique il existe des implémentations qui fonctionnent bien[réf. souhaitée]. Le solveur SMT Z3 implémente l'arithmétique de Presburger.

Notes et références[modifier | modifier le code]

  1. On ne peut démontrer l'absurde, ou encore il existe un modèle, en fait le modèle standard des entiers naturels.
  2. Toute proposition est démontrable ou sa négation est démontrable.
  3. Michael Jo Fischer, Michael J. Fischer, Michael O. Rabin et Michael O. Rabin, « Super-Exponential Complexity of Presburger Arithmetic », {{Article}} : paramètre « périodique » manquant,‎ , p. 27–41 (lire en ligne)
  4. Olivier Carton, Langages Formels, Calculabilité Et Complexité, Vuibert, , 236 p.
  5. Derek C. Oppen, « A 222pn upper bound on the complexity of Presburger Arithmetic », Journal of Computer and System Sciences, vol. 16,‎ , p. 323–332 (DOI 10.1016/0022-0000(78)90021-1, lire en ligne)
  6. Leonard Berman, « The complexity of logical theories », Theoretical Computer Science, vol. 11,‎ , p. 71–77 (DOI 10.1016/0304-3975(80)90037-7, lire en ligne)