Aritmética Presburger - Presburger arithmetic

A aritmética de Presburger é a teoria de primeira ordem dos números naturais com adição , nomeada em homenagem a Mojżesz Presburger , que a introduziu em 1929. A assinatura da aritmética de Presburger contém apenas a operação de adição e igualdade , omitindo inteiramente a operação de multiplicação . Os axiomas incluem um esquema de indução .

A aritmética de presburger é muito mais fraca do que a aritmética de Peano , que inclui operações de adição e multiplicação. Ao contrário da aritmética de Peano, a aritmética de Presburger é uma teoria decidível . Isso significa que é possível determinar algoritmicamente, para qualquer sentença na linguagem da aritmética de Presburger, se essa sentença pode ser demonstrada a partir dos axiomas da aritmética de Presburger. A complexidade computacional de tempo de execução assintótica desse algoritmo é pelo menos duplamente exponencial , no entanto, como mostrado por Fischer & Rabin (1974) .

Visão geral

A linguagem da aritmética Presburger contém constantes 0 e 1 e uma função binária +, interpretada como adição.

Nessa linguagem, os axiomas da aritmética Presburger são os fechamentos universais do seguinte:

¬ (0 = x + 1)
x + 1 = y + 1 → x = y
x + 0 = x
x + ( y + 1) = ( x + y ) + 1
Seja P ( x ) uma fórmula de primeira ordem na linguagem da aritmética de Presburger com uma variável livre x (e possivelmente outras variáveis livres). Então, a seguinte fórmula é um axioma:
( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y ).

(5) é um esquema de axioma de indução , representando infinitos axiomas. Estes não podem ser substituídos por nenhum número finito de axiomas, isto é, a aritmética de Presburger não é finitamente axiomatizável na lógica de primeira ordem.

A aritmética Presburger pode ser vista como uma teoria de primeira ordem com igualdade contendo precisamente todas as consequências dos axiomas acima. Alternativamente, pode ser definido como o conjunto das sentenças que são verdadeiras na interpretação pretendida : a estrutura de inteiros não negativos com constantes 0, 1 e a adição de inteiros não negativos.

A aritmética do Presburger é projetada para ser completa e decidível. Portanto, ele não pode formalizar conceitos como divisibilidade ou primalidade , ou, mais geralmente, qualquer conceito de número levando à multiplicação de variáveis. No entanto, pode formular instâncias individuais de divisibilidade; por exemplo, prova "para todo x , existe y : ( y + y = x ) ∨ ( y + y + 1 = x )". Isso afirma que todo número é par ou ímpar.

Propriedades

Mojżesz Presburger provou que a aritmética de Presburger é:

consistente : Não há nenhuma afirmação na aritmética de Presburger que possa ser deduzida dos axiomas de forma que sua negação também possa ser deduzida.
completo : para cada afirmação na linguagem da aritmética de Presburger, ou é possível deduzi-la dos axiomas ou é possível deduzir sua negação.
decidível : existe um algoritmo que decide se qualquer afirmação dada na aritmética de Presburger é um teorema ou um não teorema.

A decidibilidade da aritmética de Presburger pode ser demonstrada usando a eliminação do quantificador , complementada pelo raciocínio sobre a congruência aritmética ( Presburger (1929) , Nipkow (2010) , Enderton 2001, p. 188). As etapas usadas para justificar um algoritmo de eliminação de quantificador podem ser usadas para definir axiomatizações recursivas que não contêm necessariamente o esquema de axioma de indução ( Presburger (1929) , Stansifer (1984) ).

Em contraste, a aritmética de Peano , que é a aritmética de Presburger aumentada com a multiplicação, não é decidível, como consequência da resposta negativa ao Entscheidungsproblem . Pelo teorema da incompletude de Gödel , a aritmética de Peano é incompleta e sua consistência não pode ser provada internamente (mas veja a prova de consistência de Gentzen ).

Complexidade computacional

O problema de decisão para a aritmética de Presburger é um exemplo interessante na teoria e computação da complexidade computacional . Seja n o comprimento de uma declaração na aritmética de Presburger. Então Fischer e Rabin (1974) provaram que, no pior caso, a prova do enunciado na lógica de primeira ordem tem comprimento pelo menos , para alguma constante c > 0. Conseqüentemente, seu algoritmo de decisão para aritmética Presburger tem tempo de execução pelo menos exponencial. Fischer e Rabin também provaram que, para qualquer axiomatização razoável (definida precisamente em seu artigo), existem teoremas de comprimento n que têm provas de comprimento duplamente exponenciais . Intuitivamente, isso sugere que há limites computacionais sobre o que pode ser comprovado por programas de computador. O trabalho de Fischer e Rabin também implica que a aritmética de Presburger pode ser usada para definir fórmulas que calculam corretamente qualquer algoritmo, desde que as entradas sejam menores do que limites relativamente grandes. Os limites podem ser aumentados, mas apenas usando novas fórmulas. Por outro lado, um limite superior triplamente exponencial em um procedimento de decisão para Aritmética de Presburger foi provado por Oppen (1978). ${\ displaystyle 2 ^ {2 ^ {cn}}}$

Um limite de complexidade mais restrito foi mostrado usando classes de complexidade alternadas por Berman (1980) . O conjunto de afirmações verdadeiras na aritmética Presburger (PA) é mostrado completo para TimeAlternations (2 ^{2 ^{n ^{O (1)}}} , n). Assim, sua complexidade está entre o tempo exponencial duplo não determinístico (2-NEXP) e o espaço exponencial duplo (2-EXPSPACE). A completude está sob reduções de muitos para um no tempo polinomial. (Além disso, observe que, embora a aritmética de Presburger seja comumente abreviada como PA, em matemática em geral, PA geralmente significa aritmética de Peano .)

Para um resultado mais refinado, seja PA (i) o conjunto de declarações Σ _i PA verdadeiras e PA (i, j) o conjunto de declarações Σ _i PA verdadeiras com cada bloco quantificador limitado a j variáveis. '<' é considerado sem quantificador; aqui, os quantificadores limitados são contados como quantificadores.
PA (1, j) está em P, enquanto PA (1) é NP-completo.
Para i> 0 e j> 2, PA (i + 1, j) é Σ _i^P -completo . O resultado de dureza precisa apenas de j> 2 (em oposição a j = 1) no último bloco quantificador.
Para i> 0, PA (i + 1) é Σ _i^EXP -completo (e é TimeAlternations (2 ^{n ^{O (i)}} , i) -completo).

Formulários

Como a aritmética de Presburger é decidível, existem provadores automáticos de teoremas para a aritmética de Presburger. Por exemplo, o sistema de assistente de prova Coq apresenta o omega tático para aritmética Presburger e o assistente de prova Isabelle contém um procedimento de eliminação de quantificador verificado por Nipkow (2010) . A complexidade exponencial dupla da teoria torna inviável o uso de provadores de teoremas em fórmulas complicadas, mas esse comportamento ocorre apenas na presença de quantificadores aninhados: Oppen e Nelson (1980) descrevem um provador de teoremas automático que usa o algoritmo simplex em uma extensão Aritmética Presburger sem quantificadores aninhados para provar algumas das instâncias das fórmulas aritméticas Presburger sem quantificador. Solucionadores de teorias de módulo de satisfatibilidade mais recentes usam técnicas de programação inteiras completas para lidar com fragmentos livres de quantificadores da teoria aritmética de Presburger ( King, Barrett & Tinelli (2014) ).

A aritmética do Presburger pode ser estendida para incluir a multiplicação por constantes, uma vez que a multiplicação é uma adição repetida. A maioria dos cálculos de subscrito de array se enquadra na região de problemas decidíveis. Essa abordagem é a base de pelo menos cinco sistemas de prova de correção para programas de computador , começando com o Stanford Pascal Verifier no final dos anos 1970 e continuando até o sistema Spec # da Microsoft em 2005.

Relação inteira definível por presburger

Algumas propriedades agora são fornecidas sobre relações inteiras definíveis em Aritmética de Presburger. Para simplificar, todas as relações consideradas nesta seção são sobre números inteiros não negativos.

Uma relação é definível por Presburger se e somente se for um conjunto semilinear .

Uma relação de número inteiro unário , ou seja, um conjunto de números inteiros não negativos, é definível por Presburger se e somente se for finalmente periódica. Ou seja, se existe um limite e um período positivo tal que, para todos os inteiros tal que , se e somente se . ${\ 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}$

Pelo teorema de Cobham-Semenov , uma relação é definível por Presburger se, e somente se, for definível na aritmética de Büchi de base para todos . Um definível relação em Buchi aritmética da base e para e sendo multiplicativamente independentes inteiros é Presburger definível. ${\ displaystyle k}$ ${\ displaystyle k \ geq 2}$ ${\ displaystyle k}$ ${\ displaystyle k '}$ ${\ displaystyle k}$ ${\ displaystyle k '}$

Uma relação inteira é definida por Presburger se e somente se todos os conjuntos de inteiros que são definíveis na lógica de primeira ordem com adição e (isto é, Aritmética Presburger mais um predicado para ) são definíveis por Presburger. Equivalentemente, para cada relação que não é definível por Presburger, existe uma fórmula de primeira ordem com adição e que define um conjunto de inteiros que não é definível usando apenas adição. ${\ displaystyle R}$ ${\ displaystyle R}$ ${\ displaystyle R}$ ${\ displaystyle R}$ ${\ displaystyle R}$

Caracterização de Muchnik

As relações definíveis por presburger admitem outra caracterização: pelo teorema de Muchnik. É mais complicado afirmar, mas levou à prova das duas caracterizações anteriores. Antes que o teorema de Muchnik possa ser enunciado, algumas definições adicionais devem ser introduzidas.

Seja um conjunto, a seção de , para e é definida 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 dois conjuntos e um -tuplo de inteiros , o conjunto é chamado -periódico em se, para todos os que então se e somente se . Para , o conjunto está a ser dito -periodic em se é -periodic por algum de tal forma 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 deixar ${\ 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 \}}

denotam o cubo de tamanho cujo canto inferior é . ${\ displaystyle k}$ ${\ displaystyle (x_ {0}, \ dots, x_ {d-1})}$

Teorema de Muchnik - é definível por Presburger se e somente se: ${\ displaystyle R \ subseteq \ mathbb {N} ^ {d}}$

se, então, todas as seções de são definíveis pelo Presburger e ${\ displaystyle d> 1}$ ${\ displaystyle R}$
existe tal que, para cada , existe tal que para todos com ${\ 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}$ é -periódico em . ${\ displaystyle s}$ ${\ displaystyle C (k, (x_ {0}, \ dots, x_ {d-1}))}$

Intuitivamente, o inteiro representa a duração de um turno, o inteiro é o tamanho dos cubos e é o limite antes da periodicidade. Este resultado permanece verdadeiro quando a condição ${\ displaystyle s}$ ${\ displaystyle k}$ ${\ displaystyle t}$

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

é substituído por ou por . ${\ displaystyle \ min (x_ {0}, \ ldots, x_ {d-1})> t}$ ${\ displaystyle \ max (x_ {0}, \ ldots, x_ {d-1})> t}$

Essa caracterização levou ao chamado "critério definível para definibilidade na aritmética de Presburger", ou seja: existe uma fórmula de primeira ordem com adição e um predicado -ary que se mantém se e somente se é interpretado por uma relação definível de Presburger. O teorema de Muchnik também permite provar que é decidível se uma sequência automática aceita um conjunto definível por Presburger. ${\ displaystyle d}$ ${\ displaystyle R}$ ${\ displaystyle R}$

Veja também

Referências

Haase, Christoph (2018). "Um guia de sobrevivência para aritmética presburger" . Notícias ACM SIGLOG . 5 (3): 67–82. doi : 10.1145 / 3242953.3242964 . S2CID 51847374 .
Cooper, DC, 1972, "Theorem Proving in Arithmetic without Multiplication" em B. Meltzer e D. Michie, eds., Machine Intelligence Vol. 7 . Editora da Universidade de Edimburgo: 91–99.
Enderton, Herbert (2001). Uma introdução matemática à lógica (2ª ed.). Boston, MA: Academic Press . ISBN 978-0-12-238452-3.
Ferrante, Jeanne e Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories . Notas de aula em matemática 718. Springer-Verlag .
Fischer, Michael J .; Rabin, Michael O. (1974). "Super-Exponential Complexity of Presburger Arithmetic" . Proceedings of the SIAM-AMS Symposium in Applied Mathematics . 7 : 27–41. Arquivado do original em 15/09/2006 . Página visitada em 2006-06-11 .
G. Nelson e DC Oppen (abril de 1978). “Um simplificador baseado em algoritmos de decisão eficientes”. Proc. 5º Simpósio ACM SIGACT-SIGPLAN sobre Princípios de Linguagens de Programação : 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., veja Stansifer (1984) para uma tradução em inglês
Stansifer, Ryan (setembro de 1984). Artigo de Presburger sobre Aritmética Integer: Observações e Tradução (PDF) (Relatório Técnico). TR84-639. Ithaca / NY: Dept. of Computer Science, Cornell University.
William Pugh , 1991, " O teste Omega: um algoritmo de programação inteira rápido e prático para análise de dependência ".
Reddy, CR e DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation. " ACM Symposium on Theory of Computing : 320-325.
Young, P., 1985, "Teoremas de Gödel, dificuldade exponencial e indecidibilidade das teorias aritméticas: uma exposição" em A. Nerode e R. Shore, Recursion Theory, American Mathematical Society: 503-522.
Oppen, Derek C. (1978). "Um limite superior de 2 ^{2 ^{2 ^pn}} na complexidade da aritmética do Presburger" . J. Comput. Syst. Sci . 16 (3): 323–332. doi : 10.1016 / 0022-0000 (78) 90021-1 .
Berman, L. (1980). "A complexidade das teorias lógicas" . Ciência da Computação Teórica . 11 (1): 71–77. doi : 10.1016 / 0304-3975 (80) 90037-7 .
Nipkow, T (2010). "Eliminação do quantificador linear" (PDF) . Journal of Automated Reasoning . 45 (2): 189–212. doi : 10.1007 / s10817-010-9183-0 . S2CID 14279141 .
King, Tim; Barrett, Clark W .; Tinelli, Cesare (2014). "Aproveitando a programação inteira linear e mista para SMT". 2014 Métodos Formais em Design Auxiliado por Computador (FMCAD) . 2014 . pp. 139–146. doi : 10.1109 / FMCAD.2014.6987606 . ISBN 978-0-9835-6784-4. S2CID 5542629 .

links externos

Um provador de teorema completo para aritmética de presburger por Philipp Rümmer

Languages

In other projects