La aritmética de Presburger es la teoría de primer orden de los números naturales con suma , nombrada en honor a Mojżesz Presburger , quien la introdujo en 1929. La firma de la aritmética de Presburger contiene solo la operación de suma y la igualdad , omitiendo la operación de multiplicación por completo. 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 de suma y 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 muestran Fischer y Rabin (1974) .
Descripción general
El lenguaje de la aritmética de Presburger contiene 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 lo siguiente:
- ¬ (0 = x + 1)
- x + 1 = y + 1 → x = y
- x + 0 = x
- x + ( y + 1) = ( x + y ) + 1
- 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 de axioma de inducción , que representa un número infinito de axiomas. Estos no pueden ser reemplazados por ningún número finito de axiomas, [ cita requerida ] es decir, la aritmética de Presburger no es finitamente axiomatizable en la lógica de primer orden.
La aritmética de Presburger puede verse como una teoría de primer orden en la que la igualdad contiene precisamente todas las consecuencias de los axiomas anteriores. Alternativamente, se puede definir como el conjunto de esas oraciones que son verdaderas en la interpretación pretendida : la estructura de enteros no negativos con constantes 0, 1 y la suma de 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 primordialidad o, de manera más general, cualquier concepto numérico que lleve a la multiplicación de variables. Sin embargo, puede formular instancias individuales de divisibilidad; por ejemplo, demuestra "para todo x , existe y : ( y + y = x ) ∨ ( y + y + 1 = x )". Esto establece que cada número es par o impar.
Propiedades
Mojżesz Presburger demostró que la aritmética de Presburger es:
- consistente : No hay enunciado en la aritmética de Presburger que pueda deducirse de los axiomas de manera que su negación también pueda deducirse.
- completo : Para cada enunciado en el lenguaje de la aritmética de Presburger, o es posible deducirlo de los axiomas o es posible deducir su negación.
- Decidible : existe un algoritmo que decide si una declaración dada en la aritmética de Presburger es un teorema o no.
La decidibilidad de la aritmética de Presburger se puede demostrar utilizando la eliminación de cuantificadores , complementada con el razonamiento sobre la congruencia aritmética ( Presburger (1929) , Nipkow (2010) , Enderton 2001, p. 188). Los pasos usados para justificar un algoritmo de eliminación de cuantificadores pueden usarse para definir axiomatizaciones recursivas que no necesariamente contienen el esquema de axioma de inducción ( Presburger (1929) , Stansifer (1984) ).
Por el contrario, la aritmética de Peano , que es la aritmética de Presburger aumentada con la multiplicación, no es decidible, como consecuencia de la respuesta negativa al problema de Entscheidung . Según el teorema de incompletitud de Gödel , la aritmética de Peano es incompleta y su consistencia no se puede demostrar internamente (pero vea 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 y el cálculo de la complejidad computacional . Sea n la longitud de un enunciado en 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 al menos una longitud, 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 precisamente en su artículo), existen teoremas de longitud n que tienen demostraciones de longitud doblemente exponenciales . Intuitivamente, esto sugiere que existen límites computacionales sobre lo que pueden probar los programas de computadora. El trabajo de Fischer y Rabin también implica que la aritmética de Presburger se puede usar 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 otro lado, Oppen (1978) demostró un límite superior triplemente exponencial en un procedimiento de decisión para la aritmética de Presburger.
Berman (1980) mostró un límite de complejidad más estrecho utilizando clases de complejidad alternas . El conjunto de afirmaciones verdaderas en la aritmética de Presburger (PA) se muestra completo para TimeAlternations (2 2 n O (1) , n). Así, 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 varios a uno en el 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 statements i PA verdaderas , y PA (i, j) el conjunto de declaraciones Σ i PA 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.
Para i> 0 y j> 2, PA (i + 1, j) es Σ i P -completo . El resultado de dureza solo necesita j> 2 (a diferencia de j = 1) en el último bloque cuantificador.
Para i> 0, PA (i + 1) es Σ i EXP -completo (y es TimeAlternations (2 n O (i) , i) -completo). [1]
Aplicaciones
Debido a que la aritmética de Presburger es decidible, existen probadores 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 de Isabelle contiene un procedimiento de eliminación de cuantificador verificado por Nipkow (2010) . La doble complejidad exponencial de la teoría hace que no sea factible usar los probadores de teoremas en fórmulas complicadas, pero este comportamiento ocurre solo en presencia de cuantificadores anidados: Oppen y Nelson (1980) describen un demostrador automático de teoremas que usa el algoritmo simplex en un extendido Aritmética de Presburger sin cuantificadores anidados para probar algunos de los casos de fórmulas aritméticas de Presburger sin cuantificadores. Los solucionadores de teorías de módulo de satisfacibilidad más recientes utilizan técnicas completas de programación de enteros para manejar fragmentos sin cuantificadores de la teoría aritmética de Presburger ( King, Barrett y Tinelli (2014) ).
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 de subíndices de matriz se encuentran dentro de la región de problemas decidibles. Este enfoque es la base de al menos cinco sistemas de prueba de corrección para programas de computadora , comenzando con Stanford Pascal Verifier a fines de la década de 1970 y continuando hasta el sistema Spec # de 2005 de Microsoft .
Relación entera predefinible por hamburguesa
Ahora se dan algunas propiedades sobre las relaciones enteras definibles en la aritmética de Presburger. En aras de la simplicidad, todas las relaciones consideradas en esta sección son enteros no negativos.
Una relación es definible por Presburger si y solo si es un conjunto semilineal . [2]
Una relación entera unaria , es decir, un conjunto de números enteros no negativos, es definible por Presburger si y solo si es, en última instancia, periódico. Es decir, si existe un umbral y un periodo positivo tal que, para todo entero tal que , si y solo si .
Según el teorema de Cobham-Semenov , una relación es definible por Presburger si y solo si es definible en la aritmética de base de Büchi para todos . [3] [4] Una relación definible en la aritmética Büchi de base y por y ser enteros multiplicativamente independientes es definible por Presburger.
Una relación entera es definible por Presburger si y solo si todos los conjuntos de enteros que son definibles en la lógica de primer orden con suma y (es decir, aritmética de Presburger más un predicado para ) son definibles por Presburger. [5] De manera equivalente, para cada relación que no es definible por Presburger, existe una fórmula de primer orden con adición y que define un conjunto de números enteros que no se puede definir utilizando solo la suma.
Caracterización de Muchnik
Las relaciones definibles por Presburger admiten otra caracterización: por el teorema de Muchnik. [6] Es más complicado de enunciar, pero condujo a la prueba de las dos caracterizaciones anteriores. Antes de que pueda establecerse el teorema de Muchnik, deben introducirse algunas definiciones adicionales.
Dejar ser un conjunto, la sección de , por y Se define como
Dados dos conjuntos y un -tupla de enteros , el conjunto se llama -periódico en si por todos tal que luego si y solo si . Para, el conjunto se ha dicho -periódico en si esto es -periódico para algunos tal que
Finalmente, para dejar
denotar el cubo de tamaño cuyo rincón menor es .
- Teorema de Muchnik. es definible por Presburger si y solo si:
- Si luego todas las secciones de son definibles por Presburger y
- existe tal que, por cada , existe tal que para todos con
- es -periódico en .
Intuitivamente, el entero representa la duración de un turno, el número entero es el tamaño de los cubos y es el umbral antes de la periodicidad. Este resultado sigue siendo cierto cuando la condición
es reemplazado por o por .
Esta caracterización condujo al llamado "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 -ariado predicado que se sostiene si y solo si se interpreta mediante una relación definible por Presburger. El teorema de Muchnik también permite probar que es decidible si una secuencia automática acepta un conjunto definible por Presburger.
Ver también
- Aritmética de Robinson
- Aritmética Skolem
Referencias
- ^ Haase, Christoph (2014). "Subclases de aritmética de Presburger y la jerarquía de EXP débil". Actas CSL-LICS . ACM. págs. 47: 1–47: 10. arXiv : 1401.5266 . doi : 10.1145 / 2603088.2603092 .
- ^ Ginsburg, Seymour; Spanier, Edwin Henry (1966). "Semigrupos, fórmulas de preburger y lenguajes" . Pacific Journal of Mathematics . 16 (2): 285-296. doi : 10.2140 / pjm.1966.16.285 .
- ^ Cobham, Alan (1969). "Sobre la base-dependencia 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 .
- ^ Semenov, AL (1977). "Presburgerness de predicados regulares en dos sistemas numéricos". Sibirsk. Estera. Z h. (en ruso). 18 : 403–418.
- ^ 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". Ana. Pure Appl. Lógica . 77 (3): 251-277. doi : 10.1016 / 0168-0072 (95) 00022-4 .
- ^ Muchnik, Andrei A. (2003). "El criterio definible para la definibilidad en la aritmética de Presburger y sus aplicaciones". Theor. Computación. Sci . 290 (3): 1433–1444. doi : 10.1016 / S0304-3975 (02) 00047-6 .
- Haase, Christoph (2018). "Una guía de supervivencia para la aritmética previa a la hamburguesa" . Noticias ACM SIGLOG . 5 (3): 67–82. doi : 10.1145 / 3242953.3242964 . S2CID 51847374 .
- Cooper, DC, 1972, "Demostración de teoremas en aritmética sin multiplicación" en B. Meltzer y D. Michie, eds., Machine Intelligence Vol. 7 . Editorial de la Universidad de Edimburgo: 91–99.
- Enderton, Herbert (2001). Una introducción matemática a la lógica (2ª ed.). Boston, MA: Prensa académica . ISBN 978-0-12-238452-3.
- Ferrante, Jeanne y Charles W. Rackoff, 1979. La complejidad computacional de las teorías lógicas . Notas de clase en matemáticas 718. Springer-Verlag .
- Fischer, Michael J .; Rabin, Michael O. (1974). "Complejidad superexponencial de la aritmética de Presburger" . Actas del Simposio SIAM-AMS en Matemática Aplicada . 7 : 27–41. Archivado desde el original el 15 de septiembre de 2006 . Consultado el 11 de junio de 2006 .
- G. Nelson y DC Oppen (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 .
- 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., ver Stansifer (1984) para una traducción al inglés
- Stansifer, Ryan (septiembre de 1984). Artículo de Presburger sobre aritmética de enteros: comentarios y traducción (PDF) (Informe técnico). TR84-639. Ithaca / NY: Departamento de Ciencias de la Computación, Universidad de Cornell.
- William Pugh , 1991, " La prueba Omega: un algoritmo de programación de enteros rápido y práctico para el análisis de dependencia ".
- Reddy, CR y DW Loveland, 1978, " Aritmética de Presburger con alternancia de cuantificadores acotados " . Simposio ACM sobre teoría de la computación : 320–325.
- 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, Recursion Theory, American Mathematical Society: 503-522.
- Oppen, Derek C. (1978). "Un límite superior de 2 2 2 pn sobre la complejidad de la aritmética de Presburger". J. Comput. Syst. Sci . 16 (3): 323–332. doi : 10.1016 / 0022-0000 (78) 90021-1 .
- Berman, L. (1980). "La complejidad de las teorías lógicas". Informática Teórica . 11 (1): 71–77. doi : 10.1016 / 0304-3975 (80) 90037-7 .
- Nipkow, T (2010). "Eliminación del cuantificador lineal" (PDF) . Revista de razonamiento automatizado . 45 (2): 189–212. doi : 10.1007 / s10817-010-9183-0 . S2CID 14279141 .
- Rey, Tim; Barrett, Clark W .; Tinelli, Cesare (2014). Aprovechamiento de la programación de enteros mixtos y lineales para SMT . FMCAD . 2014 . págs. 139-146. doi : 10.1109 / FMCAD.2014.6987606 . ISBN 978-0-9835-6784-4. S2CID 5542629 .
enlaces externos
- Un completo demostrador de teoremas para la aritmética de Presburger por Philipp Rümmer