Aritmética de Presburger

Teoría decidible de primer orden de los números naturales con adición

La aritmética de Presburger es la teoría de primer orden de los números naturales con adición , llamada así en honor a Mojżesz Presburger , quien la introdujo en 1929. La signatura de la aritmética de Presburger contiene únicamente la operación de adición y la igualdad , omitiendo por completo la operación de multiplicación . La teoría es computablemente axiomatizable; los axiomas incluyen un esquema de inducción .

La aritmética de Presburger es mucho más débil que la aritmética de Peano , que incluye operaciones tanto de suma como de multiplicación. A diferencia de la aritmética de Peano, la aritmética de Presburger es una teoría decidible . Esto significa que es posible determinar algorítmicamente, para cualquier oración en el lenguaje de la aritmética de Presburger, si esa oración es demostrable a partir de los axiomas de la aritmética de Presburger. Sin embargo, la complejidad computacional asintótica en tiempo de ejecución de este algoritmo es al menos doblemente exponencial , como lo demostraron Fischer y Rabin (1974).

Descripción general

El lenguaje de la aritmética de Presburger contiene las constantes 0 y 1 y una función binaria +, interpretada como suma.

En este lenguaje, los axiomas de la aritmética de Presburger son los cierres universales de los siguientes:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + ( y + 1) = ( x + y ) + 1
5. Sea P ( x ) una fórmula de primer orden en el lenguaje de la aritmética de Presburger con una variable libre x (y posiblemente otras variables libres). Entonces la siguiente fórmula es un axioma:
   ( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y ).

(5) es un esquema axiomático de inducción que representa una cantidad infinita de axiomas. Estos no pueden ser reemplazados por ningún número finito de axiomas, es decir, la aritmética de Presburger no es finitamente axiomatizable en la lógica de primer orden. ^[1]

La aritmética de Presburger puede considerarse como una teoría de primer orden con igualdad que contiene precisamente todas las consecuencias de los axiomas anteriores. Alternativamente, puede definirse como el conjunto de aquellas oraciones que son verdaderas en la interpretación pretendida : la estructura de números enteros no negativos con constantes 0, 1 y la adición de números enteros no negativos.

La aritmética de Presburger está diseñada para ser completa y decidible. Por lo tanto, no puede formalizar conceptos como divisibilidad o primalidad o, de manera más general, ningún concepto numérico que conduzca a la multiplicación de variables. Sin embargo, puede formular casos individuales de divisibilidad; por ejemplo, demuestra "para todo x , existe y  : ( y + y = x ) ∨ ( y + y + 1 = x )". Esto establece que todo número es par o impar.

Propiedades

Presburger (1929) demostró que la aritmética de Presburger era:

• consistente : No hay ningún enunciado en la aritmética de Presburger que pueda deducirse de los axiomas de manera que también pueda deducirse su negación.
• completo : Para cada enunciado en el lenguaje de la aritmética de Presburger, es posible deducirlo de los axiomas o es posible deducir su negación.
• decidible : Existe un algoritmo que decide si cualquier enunciado dado en la aritmética de Presburger es un teorema o un no teorema.

La decidibilidad de la aritmética de Presburger se puede demostrar utilizando la eliminación de cuantificadores , complementada con un razonamiento sobre la congruencia aritmética . ^{[2] [3] [4] [5] [6]} Los pasos utilizados para justificar un algoritmo de eliminación de cuantificadores se pueden utilizar para definir axiomatizaciones computables que no necesariamente contienen el esquema axiomático de inducción. ^{[2] [7]}

Por el contrario, la aritmética de Peano , que es la aritmética de Presburger aumentada con la multiplicación, no es decidible, como lo demostró Church junto con la respuesta negativa al Entscheidungsproblem . Por el teorema de incompletitud de Gödel , la aritmética de Peano es incompleta y su consistencia no es demostrable internamente (pero véase la prueba de consistencia de Gentzen ).

Complejidad computacional

El problema de decisión para la aritmética de Presburger es un ejemplo interesante en la teoría de la complejidad computacional y la computación . Sea n la longitud de un enunciado en la aritmética de Presburger. Luego, Fischer y Rabin (1974) demostraron que, en el peor de los casos, la prueba del enunciado en lógica de primer orden tiene una longitud de al menos , para alguna constante c > 0. Por lo tanto, su algoritmo de decisión para la aritmética de Presburger tiene un tiempo de ejecución al menos exponencial. Fischer y Rabin también demostraron que para cualquier axiomatización razonable (definida con precisión en su artículo), existen teoremas de longitud n que tienen pruebas de longitud doblemente exponencial . Intuitivamente, esto sugiere que hay límites computacionales sobre lo que se puede demostrar mediante programas de computadora. El trabajo de Fischer y Rabin también implica que la aritmética de Presburger se puede utilizar para definir fórmulas que calculen correctamente cualquier algoritmo siempre que las entradas sean menores que límites relativamente grandes. Los límites se pueden aumentar, pero solo mediante el uso de nuevas fórmulas. Por otra parte, Oppen (1978) demostró un límite superior triplemente exponencial en un procedimiento de decisión para la aritmética de Presburger. ${\displaystyle 2^{2^{cn}}}$

Berman (1980) demostró un límite de complejidad más estricto utilizando clases de complejidad alternadas. El conjunto de enunciados verdaderos en la aritmética de Presburger (PA) se muestra completo para TimeAlternations (2 ^{2 n O(1)} , n). Por lo tanto, su complejidad está entre el tiempo no determinista exponencial doble (2-NEXP) y el espacio exponencial doble (2-EXPSPACE). La completitud está bajo reducciones de muchos a uno en tiempo polinomial . (Además, tenga en cuenta que, si bien la aritmética de Presburger se abrevia comúnmente PA, en matemáticas en general PA generalmente significa aritmética de Peano ).

Para obtener un resultado más detallado, sea PA(i) el conjunto de declaraciones PA Σ _i verdaderas , y PA(i, j) el conjunto de declaraciones PA Σ _i verdaderas con cada bloque cuantificador limitado a j variables. '<' se considera libre de cuantificadores; aquí, los cuantificadores acotados se cuentan como cuantificadores.
PA(1, j) está en P, mientras que PA(1) es NP-completo. ^[8]
Para i > 0 y j > 2, PA(i + 1, j) es Σ _i ^P -completo . El resultado de dureza solo necesita j>2 (en lugar de j=1) en el último bloque cuantificador.
Para i>0, PA(i+1) es Σ _i ^EXP -completo . ^[9]

La aritmética de Presburger corta ( ) es completa (y por lo tanto NP-completa para ). Aquí, 'corta' requiere un tamaño de oración acotado (es decir, ) excepto que las constantes enteras no son acotadas (pero su número de bits en binario cuenta contra el tamaño de entrada). Además, la PA de dos variables (sin la restricción de ser 'corta') es NP-completa. ^[10] La PA corta (y por lo tanto ) está en P, y esto se extiende a la programación lineal entera paramétrica de dimensión fija. ^[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}}$

Aplicaciones

Debido a que la aritmética de Presburger es decidible, existen demostradores automáticos de teoremas para la aritmética de Presburger. Por ejemplo, el sistema de asistente de prueba Coq presenta la táctica omega para la aritmética de Presburger y el asistente de prueba Isabelle contiene un procedimiento de eliminación de cuantificadores verificado por Nipkow (2010). La complejidad exponencial doble de la teoría hace que sea inviable utilizar los demostradores de teoremas en fórmulas complicadas, pero este comportamiento ocurre solo en presencia de cuantificadores anidados: Nelson y Oppen (1978) describen un demostrador automático de teoremas que utiliza el algoritmo simplex en una aritmética de Presburger extendida sin cuantificadores anidados para demostrar algunas de las instancias de fórmulas aritméticas de Presburger sin cuantificadores. Los solucionadores de teorías de satisfacibilidad módulo más recientes utilizan técnicas de programación entera completa para manejar fragmentos sin cuantificadores de la teoría aritmética de Presburger. ^[12]

La aritmética de Presburger se puede ampliar para incluir la multiplicación por constantes, ya que la multiplicación es una suma repetida. La mayoría de los cálculos con subíndices de matrices caen entonces dentro de la región de los problemas decidibles. ^[13] Este enfoque es la base de al menos cinco sistemas de prueba de corrección para programas informáticos , comenzando con el Stanford Pascal Verifier a finales de los años 1970 y continuando hasta el sistema Spec# de Microsoft de 2005.

Relación entera definible por Presburger

A continuación se dan algunas propiedades sobre relaciones entre números enteros definibles en la aritmética de Presburger. Para simplificar, todas las relaciones consideradas en esta sección se refieren a números enteros no negativos.

Una relación es definible según Presburger si y sólo si es un conjunto semilineal . ^[14]

Una relación entera unaria , es decir, un conjunto de números enteros no negativos, es definible según Presburger si y solo si es en última instancia periódica. Es decir, si existe un umbral y un período positivo tales que, para todo número entero tal que , si y solo si . ${\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}$

Por el teorema de Cobham-Semenov , una relación es definible según Presburger si y solo si es definible en aritmética de Büchi de base para todos los . ^{[15] [16]} Una relación definible en aritmética de Büchi de base y para y que sean enteros multiplicativamente independientes es definible según Presburger. ${\displaystyle k}$ ${\displaystyle k\geq 2}$ ${\displaystyle k}$ ${\displaystyle k'}$ ${\displaystyle k}$ ${\displaystyle k'}$

Una relación entera es definible según Presburger si y solo si todos los conjuntos de números enteros que son definibles en lógica de primer orden con adición y (es decir, aritmética de Presburger más un predicado para ) son definibles según Presburger. ^[17] De manera equivalente, para cada relación que no es definible según Presburger, existe una fórmula de primer orden con adición y que define un conjunto de números enteros que no es definible utilizando solo adición. ${\displaystyle R}$ ${\displaystyle R}$ ${\displaystyle R}$ ${\displaystyle R}$ ${\displaystyle R}$

Caracterización de Muchnik

Las relaciones definibles por Presburger admiten otra caracterización: mediante el teorema de Muchnik. ^[18] Es más complicado de enunciar, pero condujo a la demostración de las dos caracterizaciones anteriores. Antes de poder enunciar el teorema de Muchnik, deben introducirse algunas definiciones adicionales.

Sea un conjunto, la sección de , para y se define como ${\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\}.}$

Dados dos conjuntos y una -tupla de enteros , el conjunto se llama -periódico en si, para todos tales que entonces si y solo si . Para , se dice que el conjunto es -periódico en si es -periódico para algunos tales que ${\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.}$

Finalmente, para dejar ${\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\}}$

denota el cubo de tamaño cuyo ángulo menor es . ${\displaystyle k}$ ${\displaystyle (x_{0},\dots ,x_{d-1})}$

Teorema de Muchnik  : ¿  es definible por Presburger si y sólo si: ${\displaystyle R\subseteq \mathbb {N} ^{d}}$

• Si entonces todas las secciones de son definibles por Presburger y ${\displaystyle d>1}$ ${\displaystyle R}$
• existe tal que, para cada , existe tal que para todo con es -periódico en . ${\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}))}$

Intuitivamente, el entero representa la longitud de un desplazamiento, el entero es el tamaño de los cubos y es el umbral antes de la periodicidad. Este resultado sigue siendo cierto cuando se cumple la condición ${\displaystyle s}$ ${\displaystyle k}$ ${\displaystyle t}$

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

se reemplaza por o por . ${\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}$ ${\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}$

Esta caracterización dio lugar al denominado "criterio definible para la definibilidad en la aritmética de Presburger", es decir: existe una fórmula de primer orden con adición y un predicado -ario que se cumple si y sólo si se interpreta mediante una relación definible según Presburger. El teorema de Muchnik también permite demostrar que es decidible si una secuencia automática acepta un conjunto definible según Presburger. ${\displaystyle d}$ ${\displaystyle R}$ ${\displaystyle R}$

Véase también

• Aritmética de Robinson
• Aritmética de Skolem

Referencias

1. Zoethout 2015, pag. 8, Teorema 1.2.4..
2. Presburger 1929.
3. Libro 1962.
4. Monje 2012, pág. 240.
5. Nipkow 2010.
6. Enderton 2001, pág. 188.
7. Stansifer 1984.
8. Nguyen Luu 2018, capítulo 3.
9. Haase 2014, págs. 47:1-47:10.
10. Nguyen y Pak 2017.
11. Eisenbrand y Shmonin 2008.
12. Rey, Barrett y Tinelli 2014.
13. Por ejemplo, en el lenguaje de programación C , si aes una matriz con un tamaño de elemento de 4 bytes, la expresión a[i]se puede traducir a , que se ajusta a las restricciones de la aritmética de Presburger.abaseadr+i+i+i+i
14. Ginsburg y Spanier 1966, págs. 285-296.
15. Cobham 1969, págs. 186-192.
16. Semenov 1977, págs. 403–418.
17. Michaux y Villemaire 1996, págs. 251-277.
18. Muchnik 2003, págs. 1433–1444.

Bibliografía

• Berman, L. (1980). "La complejidad de las teorías lógicas". Theoretical Computer Science . 11 (1): 71–77. doi : 10.1016/0304-3975(80)90037-7 .

• Büchi, J. Richard (1962). "Sobre un método de decisión en aritmética restringida de segundo orden". En Nagel, Ernest ; Suppes, Patrick ; Tarski, Alfred (eds.). Lógica, metodología y filosofía de la ciencia . Actas del Congreso Internacional de Lógica. Stanford: Stanford University Press . págs. 1–11.

• Cobham, Alan (1969). "Sobre la dependencia de bases de conjuntos de números reconocibles por autómatas finitos". Matemáticas. Teoría de sistemas . 3 (2): 186–192. doi :10.1007/BF01746527. S2CID  19792434.

• Cooper, DC (1972). Meltzer, B.; Michie, D. (eds.). "Demostración de teoremas en aritmética sin multiplicación" (PDF) . Inteligencia artificial . 7 . Edinburgh University Press : 91–99.

• Eisenbrand, Friedrich ; Shmonin, Gennady (2008). "Programación entera paramétrica en dimensión fija". Matemáticas de la investigación de operaciones . 33 (4): 839–850. arXiv : 0801.4336 . doi :10.1287/moor.1080.0320. S2CID  15698556.

• Enderton, Herbert (2001). Una introducción matemática a la lógica (2.ª ed.). Boston, MA: Academic Press . ISBN 978-0-12-238452-3.

• Ferrante, Jeanne ; Rackoff, Charles W. (1979). La complejidad computacional de las teorías lógicas . Apuntes de clase en matemáticas. Vol. 718. Springer-Verlag . doi :10.1007/BFb0062837. ISBN 978-3-540-09501-9.Sr .  0537764.

• Fischer, Michael J. ; Rabin, Michael O. (1974). "Complejidad superexponencial de la aritmética de Presburger". En Karp, Richard M. (ed.). Complejidad de la computación . Actas de SIAM-AMS. Vol. 7. American Mathematical Society . págs. 27–41. ISBN 978-0-8218-1327-0. OCLC  1205569621. Archivado desde el original el 15 de septiembre de 2006. Consultado el 11 de junio de 2006 .

• Ginsburg, Seymour ; Spanier, Edwin Henry (1966). "Semigrupos, fórmulas de Presburger y lenguajes". Revista del Pacífico de Matemáticas . 16 (2): 285–296. doi : 10.2140/pjm.1966.16.285 .

• Haase, Christoph (2014). "Subclases de la aritmética de Presburger y la jerarquía EXP débil". Actas CSL- LICS . ACM. págs. 47:1–47:10. arXiv : 1401.5266 . doi :10.1145/2603088.2603092.

• Haase, Christoph (2018). "Una guía de supervivencia para la aritmética de Presburger" (PDF) . ACM SIGLOG News . 5 (3): 67–82. doi :10.1145/3242953.3242964. S2CID  51847374.

• Hoang, Nhat Minh. "Aritmética de Presburger" (PDF) . Technische Universität München . Consultado el 22 de marzo de 2024 . En este artículo se explica un procedimiento para construir un autómata que resuelve la aritmética de Presburger.

• King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). "Aprovechamiento de la programación lineal y entera mixta para SMT". 2014 Métodos formales en diseño asistido por computadora (FMCAD) . Vol. 2014. págs. 139–146. doi :10.1109/FMCAD.2014.6987606. ISBN . 978-0-9835-6784-4. Número de identificación del sujeto  5542629.

• Michaux, Christian; Villemaire, Roger (1996). "Aritmética de Presburger y reconocibilidad de conjuntos de números naturales por autómatas: nuevas pruebas de los teoremas de Cobham y Semenov". Anales de lógica pura y aplicada . 77 (3): 251–277. doi :10.1016/0168-0072(95)00022-4.

• Monk, J. Donald (2012). Lógica matemática (Textos de posgrado en matemáticas (37)) (Reimpresión en tapa blanda de la primera edición original, 1976). Springer. ISBN 9781468494549.

• Muchnik, Andrei A. (2003). "El criterio definible para la definibilidad en la aritmética de Presburger y sus aplicaciones". Theor. Comput. Sci . 290 (3): 1433–1444. doi : 10.1016/S0304-3975(02)00047-6 .

• Nelson, Greg; Oppen, Derek C. (abril de 1978). "Un simplificador basado en algoritmos de decisión eficientes". Proc. 5.º Simposio ACM SIGACT-SIGPLAN sobre principios de lenguajes de programación : 141–150. doi :10.1145/512760.512775. S2CID  6342372.

• Nguyen, Danny; Pak, Igor (2017). "La aritmética breve de Presburger es difícil" (PDF) . 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS) . pp. 37–48. arXiv : 1708.08179 . doi :10.1109/FOCS.2017.13. ISBN . 978-1-5386-3464-6. S2CID  3425421 . Consultado el 4 de septiembre de 2022 .

• Nguyen Luu, Dahn (2018). La complejidad computacional de la aritmética de Presburger (tesis). Los Ángeles: Tesis y disertaciones electrónicas de la UCLA . Consultado el 8 de septiembre de 2022 .

• Nipkow, T (2010). "Eliminación de cuantificadores lineales" (PDF) . Revista de razonamiento automatizado . 45 (2): 189–212. doi :10.1007/s10817-010-9183-0. S2CID  14279141.

• Oppen, Derek C. (1978). "Un límite superior de 222pn en la complejidad de la aritmética de Presburger". J. Comput. Syst. Sci. 16 (3): 323–332. doi : 10.1016/0022-0000(78)90021-1 .

• 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 Slaves, Warszawa : 92–101., véase Stansifer (1984) para una traducción al inglés

• Pugh, William (1991). "La prueba Omega: Un algoritmo rápido y práctico de programación entera para el análisis de dependencia". Actas de la conferencia ACM/IEEE de 1991 sobre supercomputación - Supercomputing '91 . Nueva York, NY, EE. UU.: Association for Computing Machinery. pp. 4–13. CiteSeerX  10.1.1.37.1995 . doi :10.1145/125826.125848. ISBN 0897914597. Número de identificación del sujeto  3174094.

• Reddy, CR; Loveland, DW (1978). "Aritmética de Presburger con alternancia de cuantificadores acotados". Actas del décimo simposio anual de la ACM sobre teoría de la computación - STOC '78 . págs. 320–325. doi :10.1145/800133.804361. S2CID  13966721.

• Semenov, AL (1977). "Presburgerness de predicados regulares en dos sistemas numéricos". Sibirsk. Mat. Zh. (en ruso). 18 : 403–418.

• Stansifer, Ryan (septiembre de 1984). Artículo de Presburger sobre aritmética de números enteros: observaciones y traducción (PDF) (Informe técnico). Vol. TR84-639. Ithaca/NY: Departamento de Ciencias de la Computación, Universidad de Cornell.

• Young, P. (1985). "Teoremas de Gödel, dificultad exponencial e indecidibilidad de las teorías aritméticas: una exposición". En A. Nerode y R. Shore (ed.). Teoría de la recursión, American Mathematical Society . págs. 503–522.

• Zoethout, Jetze (1 de febrero de 2015). Interpretaciones en aritmética de Presburger (tesis de licenciatura) (PDF) (tesis) . Consultado el 25 de agosto de 2023 .

Enlaces externos

• Un demostrador de teoremas completo para la aritmética de Presburger por Philipp Rümmer