Lógica monádica de segunda ordem

Na lógica matemática e na ciência da computação teórica , a lógica monádica de segunda ordem (abreviada como MSO para monádica segunda ordem ) é a extensão da lógica de primeira ordem com variáveis denotando conjuntos. De forma equivalente, é o fragmento de lógica de segunda ordem em que os de segunda ordem quantificações referem-se apenas a unárias predicados (daí o termo monadic), isto é, em conjuntos . Por exemplo :

${\ displaystyle \ existe Z (\ existe u, u \ em Z) \ land \ forall x, (x \ in Z \ rightarrow \ existe y, ({\ text {filho}} (x, y) \ land y \ em Z))}$ é uma fórmula de MSO e diz "existe um conjunto Z tal que existe um elemento u que pertence a Z e para todo x, se x está em Z, então existe y tal que y é um filho de xe é lá em Z ”. Não é uma fórmula de lógica de primeira ordem porque há uma quantização de segunda ordem em Z;
Todas as fórmulas da lógica de primeira ordem são fórmulas MSO;
A fórmula não é uma fórmula MSO porque há uma quantização em um predicado binário R. ${\ displaystyle \ existe R, \ existe x, \ forall y, R (x, y)}$

Uma vez que o problema de satisfatibilidade da lógica de primeira ordem é indecidível, uma vez que MSO é uma extensão conservadora da lógica de primeira ordem, o problema de satisfatibilidade da MSO também é indecidível. Mas de acordo com Yuri Gurevich , MSO é uma fonte de teorias lógicas que são expressivas e decidíveis.

Exemplos de fórmulas

A fórmula que define a recorrência, e que lê "para qualquer conjunto X, se 0 pertence a X, e se para todo y, y pertence a X implica y + 1 pertence a X então para todo z, z pertence a X" é uma fórmula de MSO. As quantificações “para todo y” e “para todo z” são quantificações de primeira ordem. A quantização "para todo X" é uma quantização de segunda ordem. ${\ displaystyle \ forall X, (X (0) \ land (\ forall y, X (y) \ rightarrow X (y + 1))) \ rightarrow (\ forall z, X (z))}$

Todas as fórmulas na lógica de primeira ordem são fórmulas MSO.

MSO e gráficos

MSO foi definido em classes de gráficos (por exemplo, não direcionado). Por exemplo, podemos expressar em MSO que um gráfico não está conectado : que diz "existe um conjunto de vértices Z tal que existe um vértice x contido em Z e um vértice y fora de Z e de modo que se dois vértices u e v estão conectados por uma aresta, então u está em Z se e somente se v estiver em Z ”(veja a figura à direita). A conectividade não é definível na lógica de primeira ordem (é uma consequência do teorema de compactação da lógica de primeira ordem ). Portanto, MSO é estritamente mais expressivo do que a lógica de primeira ordem em gráficos. ${\ displaystyle \ existe Z, (\ existe x, x \ em Z \ land \ existe y, y \ não \ em Z) \ land (\ forall u, v, {\ text {edge}} (u, v) \ rightarrow (u \ in Z \ leftrightarrow v \ in Z))}$

Em uma classe finita, o MSO e a lógica de primeira ordem têm expressividade equivalente. Existem infinitas classes onde MSO e lógica de primeira ordem têm expressividade equivalente.

O teorema de Courcelle é um resultado algorítmico em MSO e gráficos: qualquer propriedade MSO é decidível em tempo linear na classe de gráficos com largura de árvore limitada. Por exemplo, de acordo com o teorema de Courcelle, saber se um gráfico pode ser colorido com 3 cores é decidível em tempo linear na classe de gráficos com largura de árvore limitada. Com efeito, pode-se expressar MSO num gráfico é colorível com três cores com a seguinte fórmula: . A fórmula diz “há conjuntos de vértices C1, C2, C3 que formam uma partição do gráfico e de forma que dois vértices adjacentes não estão no mesmo Ci”. Por outro lado, o problema de decisão que consiste em saber se algum gráfico pode ser colorido com 3 cores é um problema NP-completo . ${\ displaystyle \ existe C_ {1}, \ existe C_ {2}, \ existe C_ {3}, \ left (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ right) \ land \ left (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {j} (s)) \ right) \ land \ left (\ forall s, t, {\ text {edge}} (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ lnot C_ {i} (s) \ lor \ lnot C_ {i} (t)) \ right)}$

Teoria da linguagem

A estrutura na qual o MSO é definido muda muito os resultados de definibilidade , computabilidade e complexidade .

Palavras acabadas

Büchi demonstrou que uma linguagem de palavras finitas é regular se, e somente se, for descrita por uma fórmula MSO sobre palavras. MSO é estritamente mais expressivo do que a lógica de primeira ordem em palavras finitas: a classe das linguagens de palavras finitas definidas pela lógica de primeira ordem é a classe das linguagens sem estrelas .

Palavras infinitas

Büchi também demonstrou que uma linguagem é regular se e somente se for descrita por uma fórmula MSO em palavras.

S1S (para segunda ordem com 1 sucessor ) é uma variante do MSO interpretada no domínio de inteiros, com um predicado para o sucessor e outro para a ordem. Büchi demonstrou em 1962 que S1S é decidível estabelecendo uma correspondência entre a satisfatibilidade de uma fórmula de S1S e o vazio de um autômato de Büchi. Elgot e Rabin demonstraram que podemos adicionar a S1S o predicado unário “ser um número fatorial ” ou “ser uma potência de $k$ ” enquanto permanecemos decidíveis. Por outro lado, se somarmos a função "vezes 2" à linguagem, obtemos toda a aritmética dos inteiros com adição e multiplicação e obtemos uma lógica indecidível.

Árvores binárias

Chamamos S2S (para segunda ordem com 2 sucessores ) a variante de MSO para falar de propriedades no modelo da árvore binária infinita. Rabin mostrou que podemos imergir MSOs em árvores de aridade 3, 4 e até em árvores de infinito aridade contável em S2S. Rabin demonstrou a decidibilidade de S2S por redução ao vazio de um autômato de árvore infinita. Por outro lado, a lógica monádica de segunda ordem na árvore binária infinita com ademais a relação "mesmo nível" é indecidível.

Versão fraca

Uma variante do MSO, chamada fraca (e denotada WMSO para MSO fraco ), foi considerada onde a quantização de segunda ordem se relaciona a subconjuntos finitos.

WS1S

WS1S (para segunda ordem fraca com 1 sucessor ) é uma variante de S1S onde a quantização de segunda ordem se relaciona apenas a subconjuntos finitos. A decidibilidade de WS1S foi demonstrada antes de S1S, por Büchi em 1960 e Algot em 1961. A prova de decidibilidade de WS1S é obtida diretamente daquela de S1S, uma vez que WS1S pode ser visto como um fragmento sintático de S1S (podemos expressar a finitude de um conjunto em S1S). A aritmética de Presburger pode ser considerada decidível transformando uma fórmula aritmética de Presburger em uma fórmula WS1S.

Büchi mostrou que existe equivalência, para qualquer linguagem de infinitas palavras L, entre:

L pode ser definido por uma propriedade S1S;
L pode ser definido por uma propriedade WS1S;
L é reconhecível por um autômato Büchi.

As equivalências são eficazes: transformamos uma fórmula S1S em um autômato de Büchi. Assim, a lógica S1S (e WS1S) é decidível. A lógica S1S é de complexidade não elementar.

WS2S

WS2S (para segunda ordem fraca com 2 sucessores ) é uma variante de S2S onde a quantização de segunda ordem ocorre apenas em subconjuntos finitos. WS2S é decidível. WS2S é estritamente mais fraco que S2S. A inclusão WS2S ⊆ S2S é estrita, de fato: para qualquer linguagem L de árvores binárias infinitas, temos equivalência entre:

L e seu complemento são reconhecíveis por um autômato de árvore com condição de Büchi;
L é definível em WS2S.

Mais precisamente, a linguagem definida por “há um caminho contendo um infinito de b” é reconhecível por um autômato de Büchi, enquanto seu complemento não. Portanto, essa linguagem é definível em S2S, mas não em WS2S.

Teoria do grupo

MSO em grupos abelianos ordenados onde a quantização de segunda ordem é restrita a subgrupos convexos é decidível.

Invariância por bisimulação

Como o teorema de Van Benthem que diz que qualquer fórmula invariante de bisimulação de primeira ordem é equivalente a (a tradução padrão de) uma fórmula lógica modal , Janin e Walukiewicz mostraram que qualquer fórmula MSO invariante de bisimulação é equivalente a uma fórmula de cálculo mu . $\ phi (x)$

É folclore (ver) ter a seguinte variante do teorema de Van Benthem para WMSO em árvores com aridade fixa: qualquer fórmula de WMSO em árvores de aridade k invariante por bisimulação é equivalente a uma fórmula do fragmento mu-cálculo sem alternância (Arnold e Niwinski deu a prova completa no caso de árvores binárias, ou seja, para WS2S).

O resultado é mais complicado para árvores de aridade arbitrária não fixa. Por um lado, existe uma outra variante de MSO que corresponde ao fragmento não alternado de mu-cálculo. Por outro lado, existe um fragmento do fragmento mu-cálculo não alternado que corresponde a WMSO invariante de bisimulação.

Axiomatização

MSO em palavras infinitas pode ser completamente axiomatizado . Partindo do sistema de axiomatização da lógica de primeira ordem, é suficiente adicionar o esquema de axiomas de compreensão , bem como uma versão de segunda ordem do axioma de recorrência de Peano .

Número de alternâncias entre quantificadores

Dependendo da estrutura em que MSO é interpretado, o número de alternâncias entre quantificadores existenciais e universais de segunda ordem necessários para obter a expressividade máxima da lógica varia. Na interpretação de MSO em árvores infinitas, qualquer fórmula MSO é equivalente a uma fórmula usando duas alternâncias de quantificadores monádicos. Na interpretação de modelos bidimensionais e coloridos acabados ( modelo de fotos ), apenas uma alternância é suficiente. Já no caso de estruturas finitas , não é possível restringir o número de alternâncias.

Compacidade de MSO

A lógica monádica de segunda ordem é compacta .

Discussões sobre a aritmética de Peano

Veja também

Lógica monádica de primeira ordem

Mu-cálculo

Notas e referências

Professor Bruno Courcelle e Dr. Joost Engelfriet , Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach , Cambridge University Press ,1 ° de janeiro de 2012, 728 p. ( ISBN 978-0-521-89833-1 e 0-521-89833-1 , leia online ).
(en) Y. Gurevich, "Monadic Second-Order Theories" , em J. Barwise, S. Feferman, Model-Theoretic Logics , New York, Springer-Verlag,1985, 479-506 p. ( leia online ).
(en) de Bruno Courcelle , Autômatos, Linguagens e Programação , Springer Berlin Heidelberg, coll. "Notas de aula em ciência da computação",7 de julho de 2008( ISBN 978-3-540-70574-1 e 9783540705758 , DOI 10.1007 / 978-3-540-70575-8_1 # page-1 , ler online ) , p. 1-13.
(em) " Curso sobre o teorema da compactação do Sr. Vardi " [PDF] .
A. Dawar e L. Hella , " The Expressive Power of Finitely Many Generalized Quantifiers, " Information and Computation , vol. 123,1 ° de dezembro de 1995, p. 172–184 ( DOI 10.1006 / inco.1995.1166 , ler online , acessado em 20 de setembro de 2016 ).
Michael Elberfeld , Martin Grohe e Till Tantau , " Where First-Order and Monadic Second-Order Logic Coincide ", Proceedings of the 2012 27th Annual IEEE / ACM Symposium on Logic in Computer Science , IEEE Computer Society, lICS '12,1 ° de janeiro de 2012, p. 265-274 ( ISBN 9780769547695 , DOI 10.1109 / LICS.2012.37 , lido online , acessado em 20 de setembro de 2016 ).
Robert McNaughton e Seymour A. Papert , Counter-Free Automata (MIT Research Monograph No. 65) , The MIT Press ,1 st janeiro 1971, 163 p. ( ISBN 0-262-13076-9 , leia online ).
MP Schützenberger , “ On finite monoids have only trivial subgroups ”, Information and Control , vol. 8,1 r abr 1965, p. 190–194 ( DOI 10.1016 / S0019-9958 (65) 90108-7 , ler online , acessado em 20 de setembro de 2016 ).
(em) J. Richard Buchi, "Nós método de decisão na aritmética de segunda ordem restrita" em S. Mac Lane, D. Siefkes, The Collected Works of J. Richard Buchi , New York, Springer,1990( ISBN 978-1-4613-8930-9 ).
(em) Calvin C. Elgot e Michael O. Rabin , " Decidability and Undecidability of Extensions of Second (First) Order Theory of (Generalized) Successor " , Journal of Symbolic Logic , vol. 31,1 ° de junho de 1966, p. 169–181 ( ISSN 0022-4812 e 1943-5886 , ler online , acessado em 20 de setembro de 2016 ).
(em) Rabin MO, " Decidability of second order theories and automata are infinite trees " , Transactions of the American Mathematical Society , vol. 141,1969, p. 1-35.
Wolfgang Thomas , "Automata on infinite objects" , em Handbook of teórico ciência da computação (volume B) , MIT Press ,1991, 133-191 p. ( ISBN 0444880747 , leia online )
(em) J. Richard Buchi , " Weak Second-Order Arithmetic and Finite Automata " , Mathematical Logic Quarterly , vol. 6,1 ° de janeiro de 1960, p. 66-92 ( ISSN 1521-3870 , DOI 10.1002 / malq.19600060105 , ler online , acessado em 20 de setembro de 2016 ).
“ Problemas de decisão do projeto de autômatos finitos e aritmética relacionada no JSTOR, ” em www.jstor.org (acessado em 20 de setembro de 2016 ) .
“ Büchi, JR (1962). Temos um método de decisão em aritmética de segunda ordem restrita. Em E. Nagel, P. Suppes, & A. Tarski (Eds.), Lógica, metodologia e filosofia da ciência (pp. 1-11). Stanford Stanford University Press. - Referências - Publicação de pesquisa científica ” , em www.scirp.org (acessado em 12 de fevereiro de 2018 )
(em) " Luke Ong - Autômatos, Lógica e Jogos: Teoria e Aplicação 1. Buchi Automata e S1S " .
(em) Michael O. Rabin, " Weakly Definable Relations and Special Automata " , Mathematical Logic and Foundations of Set Theory, North-Holland , Vol. 59,1 r janeiro 1970, p. 1–23 ( ISSN 0049-237X , DOI 10.1016 / S0049-237X (08) 71929-3 , ler online , acessado em 12 de fevereiro de 2018 )
(em) Mark Weyer , Automata Logics, and Infinite Games , Springer, Berlin, Heidelberg, al. "Notas de aula em ciência da computação",2002( ISBN 3-540-36387-4 , DOI 10.1007 / 3-540-36387-4_12 , leitura online ) , p. 207-230, Teorema 12,25
(em) Frank Niessner , Automata Logics, and Infinite Games , Springer, Berlin, Heidelberg, al. "Notas de aula em ciência da computação",2002( ISBN 3-540-36387-4 , DOI 10.1007 / 3-540-36387-4_8 , leitura online ) , p. 135-152, Teorema 8.6
Yuri Gurevich , “ Teoria expandida de grupos Abelianos ordenados ”, Annals of Mathematical Logic , vol. 12,1 st dezembro 1977, p. 193-228 ( DOI 10.1016 / 0003-4843 (77) 90014-6 , lido online , acessado em 20 de setembro de 2016 ).
(em) David Janin e Igor Walukiewicz (1996) " On the Expressive Completness of the Mu-Calculus Propositional with Respect to Monadic Second Order Logic " in CONCUR '96 Concurrency Theory Lecture Lecture Notes in Computer Science 1119 , Springer. Acessado em 23 de julho de 2017 .
Facundo Carreiro , Alessandro Facchini , Yde Venema e Fabio Zanasi , “ Weak MSO: Autómatos e Expressividade Modulo Bisimilarity ”, Proceedings da Reunião Conjunta da Vigésima Terceira Conferência EACSL anual sobre Computer Logic Science (CSL) e da Vigésima -Nono Simpósio Anual ACM / IEEE em Lógica em Ciência da Computação (LICS) , ACM, cSL-LICS '14,1 ° de janeiro de 2014, p. 27: 1-27: 27 ( ISBN 9781450328869 , DOI 10.1145 / 2603088.2603101 , lido online , acessado em 20 de setembro de 2016 ).
“ Noções básicas de cálculo, 1ª edição | A. Arnold, D. Niwinski ” , em store.elsevier.com (acessado em 20 de setembro de 2016 ) .
A. Facchini , Y. Venema e F. Zanasi , " A Characterization Theorem for the Alternation-Free Fragment of the Modal # x00B5; -Calculus ", 2013 28º Simpósio Anual IEEE / ACM sobre Lógica em Ciência da Computação (LICS) ,1 ° de junho de 2013, p. 478-487 ( DOI 10.1109 / LICS.2013.54 , ler online , acessado em 20 de setembro de 2016 ).
C. Riba , " A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words ", FIP International Federation for Information Processing , Springer Berlin Heidelberg,1 ° de junho de 2013, p. 310-324 ( DOI 10.1007 / 978-3-642-33475-7_22 , ler online , acessado em 21 de setembro de 2016 ).
(em) Wolfgang Thomas, Manual de Linguagens Formais: Volume 3 Além das Palavras (Linguagens, autômatos e lógica) , Grzegorz Rozenberg, Arto Salomaa.
(em) O. Matz, " One will do in existential quantify monadic second-order logic over pictures " , Mathematical Foundations of Computer Science in 1998 , agosto 24-28, 1998, p. 751-759 ( ISSN 0302-9743 , ler online ).
(in) Otto, " Uma nota sobre o número de quantificadores monádicos monádicos em Σ ^ 1_1 " , Cartas de processamento de informações ,24 de março de 1995, p. 337-339 ( ler online ).