Ponteiros para aplicativos CS da lógica

Eu sou um estudante de graduação em matemática com uma sólida formação em lógica. Eu fiz um curso de graduação de um ano em lógica, juntamente com cursos de teoria dos modelos finitos e outro sobre forçar e definir teoria. A maioria dos textos de CS parece assumir apenas um fundo muito modesto da lógica, que cobre principalmente os fundamentos da lógica proposicional e da lógica de primeira ordem.

Gostaria de obter algumas dicas sobre onde ir para aplicativos de CS em que materiais mais pesados ​​da lógica estão sendo usados. Um dos meus interesses seria a teoria dos tipos e métodos formais em geral. Alguém poderia sugerir algumas boas leituras além dos livros introdutórios sobre verificação de modelos e linguagens de programação?

Revisei brevemente algumas áreas aqui, tentando me concentrar em idéias que atrairiam alguém com experiência em lógica matemática avançada.

Teoria do Modelo Finito

A restrição mais simples da teoria clássica dos modelos do ponto de vista da ciência da computação é estudar estruturas sobre um universo finito. Essas estruturas ocorrem na forma de bancos de dados relacionais, gráficos e outros objetos combinatórios que surgem em toda parte na ciência da computação. A primeira observação é que vários teoremas fundamentais da teoria dos modelos de primeira ordem falham quando restritos a modelos finitos. Isso inclui o teorema da compactação, o teorema da completude de Godel e construções de ultraprodutos. Trakhtenbrot mostrou que, diferentemente da lógica clássica de primeira ordem, a satisfação em relação aos modelos finitos é indecidível.

As ferramentas fundamentais nessa área são a localidade de Hanf, a localidade de Gaifman e inúmeras variações nos jogos de Ehrenfeucht-Fraisse. Os tópicos estudados incluem lógicas infinitárias, lógicas com contagem, lógicas de ponto fixo, etc. sempre com foco em modelos finitos. Há trabalhos focando a expressividade em fragmentos de variável finita da lógica de primeira ordem e essas lógicas têm caracterizações por meio de jogos de seixos. Outra direção de investigação é identificar propriedades da lógica clássica que sobrevivem à restrição de modelos finitos. Um resultado recente nessa direção de Rossman mostra que certos teoremas de preservação de homomorfismos ainda se mantêm sobre modelos finitos.

1. Teoria dos Modelos Finitos , Ebbinghaus e Flum
2. Elementos da teoria finita do modelo , Libkin
3. Sobre estratégias de vitória nos jogos de Ehrenfeucht-Fraisse , Arora e Fagin, 1997.
4. Teoremas da preservação do homomorfismo , Rossman

O cálculo proposicional$\mu$

Uma linha de trabalho do final dos anos 60 mostrou que inúmeras propriedades dos programas podiam ser expressas em extensões da lógica proposicional que suportavam o raciocínio sobre pontos fixos. O modal- cálculo é uma lógica desenvolvida neste período que tem encontrado uma ampla gama de aplicações em métodos formais automatizados. Muitos métodos formais estão conectados à lógica temporal, ou lógica do estilo Hoare, e muito disso pode ser visto em termos do cálculo de µ . De fato, ouvi dizer que o µ- cálcio é a linguagem assembly da lógica temporal.$\mu$$\mu$$\mu$

$\mu$$\mu$$\mu$$\mu$$\mu$

1. $\mu$
2. $\mu$
3. $\mu$
4. $\mu$
5. A hierarquia de alternância modal do mu-cálculo é estrita , Bradfield, 1996
6. A hierarquia variável do mu-calculus é estrita , Berwanger, E. Grädel e G. Lenzi, 2005

Lógica Temporal Linear

A lógica temporal linear foi adotada da lógica filosófica na ciência da computação para raciocinar sobre o comportamento dos programas de computador. Foi considerada uma boa lógica, pois podia expressar propriedades como invariância (ausência de erros) e finalização. A teoria da prova da lógica temporal foi desenvolvida por Manna e Pnueli (e outros, posteriormente) em seus artigos e livros. A verificação do modelo e o problema de satisfação do LTL podem ser resolvidos em termos de autômatos em infinitas palavras.

Pnueli também provou resultados fundamentais sobre LTL em seu artigo original, introduzindo a lógica para raciocinar sobre programas. Vardi e Wolper fizeram uma compilação muito mais simples de fórmulas LTL nos autômatos Buchi. A conexão com a lógica temporal levou a intenso estudo de algoritmos para derivar eficientemente autômatos de LTL e para determinação e complementação de autômatos Buchi. O teorema de Kamp mostra que LTL com desde e até$\omega$$\mu$$\mu$

1. A lógica temporal dos programas , Pnueli 1977
2. Da Igreja e antes da PSL , Vardi, 2008
3. Uma abordagem teórica de autômatos à lógica temporal linear , Vardi e Wolper, 1986
4. A Lógica Temporal de Sistemas Reativos e Concorrentes: Especificação , Maná e Pnueli
5. Uma hierarquia Até e outras aplicações de um jogo de Ehrenfeucht-Fraïssé para lógica temporal , Etessami e Wilke, 2000

Lógicas de Árvore Computacional

$\mu$

O problema de verificação de modelo para CTL sobre estruturas finitas ocorre em tempo polinomial. O problema de verificação do modelo para CTL * está EXPTIME completo. A axiomatização do CTL * foi um problema aberto desafiador que foi finalmente resolvido por Reynolds 2001. O análogo do teorema de van Benthem para lógica modal e o teorema de Kamp para LTL é dado para CTL * por um teorema de Hafer e Thomas mostrando que CTL * corresponde a um fragmento da lógica monádica de segunda ordem sobre árvores binárias. Uma caracterização posterior de Hirschfeld e Rabinovich é que CTL * é expressivamente equivalente ao fragmento invariante de bisimulação de MSO com quantificação de caminho.

1. "Às vezes" e "nunca" revisitado: em lógica temporal versus temporal linear , Emerson e Halpern, 1986
2. Sobre o poder expressivo da CTL , Moller, Rabinovich, 1999
3. Lógica da árvore de computação CTL * e quantificadores de caminho na teoria monádica da árvore binária , Hafer e Thomas, 1987
4. Uma axiomatização da lógica da árvore de computação completa , Reynolds, 2001

Línguas de palavras infinitas

$\omega$

$\omega$$\omega$$\omega$-palavras. Além disso, usando topologia elementar, eles mostraram que todas as propriedades de tempo linear podem ser expressas como a interseção de uma propriedade de segurança e de vivacidade. Esse resultado tem conseqüências práticas significativas porque significa que, em vez de construir verificadores complexos de propriedades, basta construir um verificador de segurança e de vivacidade. Uma redução adicional mostra que é suficiente construir um verificador de invariância e um verificador de finalização. A caracterização de segurança-vida foi estendida às árvores por Manolios e Trefler e, mais recentemente, a conjuntos de traços, na estrutura de hiperpropriedades, por Clarkson e Schneider.

1. Palavras Infinitas: Autômatos, Semigrupos, Lógica e Jogos , Perrin e Pin, 2004
2. $\omega$
3. $\omega$
4. Sobre congruências sintáticas para ω - línguas , Maler e Staiger, 1993

Autômatos em palavras infinitas

Onde houver idiomas, os cientistas da computação terão autômatos. Entre na teoria dos autômatos sobre palavras infinitas e árvores infinitas. É extremamente triste que, embora os autômatos sobre palavras infinitas apareçam dentro de dois anos de autómatos em palavras finitas, esse tópico fundamental raramente seja abordado nos currículos padrão de ciências da computação. Os autômatos sobre infinitas palavras e árvores fornecem uma abordagem muito robusta para provar a decidibilidade da satisfação de uma família muito rica de lógicas.

$\omega$

1. Decidibilidade de teorias de segunda ordem e autômatos em árvores infinitas , Rabin, 1969
2. Autômatos em objetos infinitos , Thomas, 1988
3. Autômatos: Da Lógica aos Algoritmos , Vardi, 2007

Infinite Games

Jogos lógicos e infinitos são uma área ativa de pesquisa. Noções da teoria dos jogos aparecem na ciência da computação em todo o lugar na dualidade entre não-determinismo e paralelismo (alternância), um programa e seu ambiente, quantificação universal e existencial, modalidades de caixa e diamante, etc. Os jogos acabaram sendo um ótima maneira de estudar propriedades dos vários tipos de lógicas não clássicas listadas acima.

Assim como nos critérios de aceitação para autômatos, temos diferentes condições de vitória para os jogos e muitas podem ser equivalentes. Como você perguntou sobre os resultados clássicos, o teorema de Borel Determinacy e os jogos de Gale-Stewart geralmente ficam discretamente no fundo de vários modelos de jogos que estudamos. Uma questão premente de nossos tempos tem sido sobre a complexidade de resolver jogos de paridade. Jurdzinski deu um algoritmo de aprimoramento da estratégia e mostrou que a decisão do vencedor estava na interseção das classes de complexidade UP e coUP. A complexidade precisa do algoritmo de Jurdzinski ficou aberta até Friedmann atribuir a ele um limite inferior em tempo exponencial em 2009.

1. A decisão do vencedor em jogos de paridade está em UP ∩ co-UP , Jurdzinski, 1998
2. Jogos para o cálculo μ , Niwinski e Walukiewicz, 1996
3. Um limite inferior exponencial para o algoritmo de melhoria da estratégia de jogos de paridade como o conhecemos , Friedmann, 2009

Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Verificação de Modelos . MIT Press 1999, é um bom livro (para mim) sobre verificação de modelos.

Glynn Winskel: A Semântica Formal de Linguagens de Programação: uma introdução . O MIT Press 1994 é um dos livros-texto padrão sobre linguagens de programação.

Mordechai Ben-Ari: Lógica matemática para ciência da computação . Springer 2001, é talvez o que você está procurando.

A teoria do banco de dados é um campo amplo que fornece muitas aplicações de lógica. Complexidade descritiva e teoria de modelos finitos são campos intimamente associados. Tanto quanto posso dizer, todas essas áreas tendem a usar estilos algébricos de lógica (seguindo os passos de Birkhoff e Tarski) em vez de teóricos da prova. No entanto, alguns dos trabalhos de Peter Buneman , Leonid Libkin , Wenfei Fan , Susan Davidson , Limsoon Wong , Atsushi Ohori e outros pesquisadores que estavam trabalhando na UPenn nos anos 80-90, procuravam unir a teoria da linguagem de programação e os bancos de dados. Isso parece exigir que você se sinta confortável com os dois estilos de lógica. O mesmo vale para trabalhos mais recentes de James Cheneye Philip Wadler .

Em termos de referências específicas, o livro padrão está disponível on-line para uma referência conveniente:

• Serge Abiteboul, Richard Hull, Victor Vianu. Foundations of Databases , 1995. http://webdam.inria.fr/Alice/

Infelizmente, não conheço nenhum livro ou pesquisa geral atualizado que cubra esse campo veloz. Eu achei duas pesquisas antigas úteis. Primeiro,

• Jan Van den Bussche, Aplicações das idéias de Alfred Tarski na teoria dos bancos de dados , CSL 2001. doi: 10.1007 / 3-540-44802-0_2

mostra como conectar os pontos entre Tarski e um subcampo específico, bancos de dados de restrição. Segundo,

• Victor Vianu, Bases de Dados e Teoria de Modelos Finitos, Complexidade Descritiva e Modelos Finitos: Anais de um Workshop DIMACS, 1996. http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz

apresenta a teoria dos bancos de dados (estilo 1996) aos teóricos finitos dos modelos e, no processo, destaca muitas aplicações interessantes da lógica nos bancos de dados. Para trabalhos mais recentes (como a teoria do XML, proveniência, modelos de streaming ou bancos de dados de gráficos), a leitura de trabalhos de pesquisa altamente citados é uma abordagem razoável.

Michael Huth e Mark Ryan: Lógica em ciência da computação , Cambridge University Press, 2004.

Eu recomendo este livro como uma introdução geral sobre como a lógica desempenha um papel na ciência da computação.

Um uso importante da lógica no CS é a lógica do programa, também chamada de lógica do Hoare.

$2 \in \sqrt(\pi^{17})$

Uma situação semelhante ocorre no estudo de lógicas modais que (simplificando um pouco mais uma vez) não são tão expressivas quanto a lógica de primeira ordem, mas o que elas podem expressar, elas expressam com fórmulas e provas mais curtas.

Identificar fragmentos adequados de ZFC não é difícil para linguagens de programação simples, mas se torna rapidamente mais desafiador à medida que as linguagens de programação adquirem mais recursos. Nos últimos dois anos, houve um progresso substancial nesse empreendimento.

O artigo Uma base axiomática para programação de computadores, de T. Hoare, é visto com frequência como fundador do estudo das lógicas dos programas, é fácil de ler e provavelmente uma boa maneira de começar a se aventurar no campo. A mesma lógica é estudada em mais detalhes no livro de Winskel, "Semântica Formal de Linguagens de Programação", mencionada por @vb le.

A teoria dos tipos pode ser vista sob uma luz semelhante. O principal ponto de venda da teoria de tipos é a identificação de provas com programas (puramente funcionais), levando a uma grande economia de conceitos e a uma poderosa automação (na forma de inferência de tipos e provadores de teoremas interativos). O preço da teoria dos tipos por ser uma maneira elegante de organizar provas é que ela não parece funcionar muito bem com linguagens de programação que não são puramente funcionais.

Um texto recente e completamente moderno que introduz a lógica do programa de maneira tingida na teoria dos tipos é Software Foundations by Pierce et al. Isso o levará bem perto da (a) ponta da pesquisa em verificação de programas e, como livro didático, provavelmente dará uma idéia de como as ciências da computação e matemática serão ensinadas no futuro.

Depois que uma lógica de programa é desenvolvida para uma linguagem, o próximo passo é a automação ou automação parcial: a construção de provas para programas não triviais exige muito trabalho, e gostaríamos que as máquinas fizessem o máximo possível. Muitas pesquisas atuais sobre métodos formais relacionadas a essa automação.

Existe uma tradição muito forte de lógica na ciência da computação. Os problemas que estudamos e a estética da comunidade da lógica computacional não são idênticos aos da comunidade da lógica matemática. Você está absolutamente certo de que desenvolvimentos significativos na teoria dos modelos, na meta-teoria da lógica de primeira ordem e na teoria dos conjuntos não são comumente usados ​​na lógica computacional. Pode-se pesquisar com sucesso logi computacional sem ver ou usar ultrafiltros, análises não padronizadas, forçantes, o teorema de Paris-Harrington e uma série de outros conceitos fascinantes que são considerados importantes na lógica clássica.

Assim como se aplica idéias matemáticas para estudar lógica, assim como idéias lógicas para estudar matemática, aplicamos lógica para estudar ciência da computação e também aplicamos perspectivas computacionais para estudar lógica. Esse foco diferente tem consequências bastante dramáticas para os tipos de resultados que são importantes para nós.

Aqui está uma citação de John Baez sobre lógica e ciência da computação. Não tenho exatamente a mesma visão, porque não estou familiarizado com a lógica matemática avançada.

Quando eu estava na graduação, eu estava bastante interessado na lógica e nos fundamentos da matemática - eu estava sempre procurando os conceitos mais impressionantes que consegui conhecer, e o teorema de Goedel, o teorema de Loewenheim-Skolem e assim por diante. lá em cima, com mecânica quântica e relatividade geral, no que me dizia respeito. [...] Lembro-me de sentir na época que a lógica se tornara menos revolucionária do que era no início do século. Pareceu-me que a lógica se tornara um ramo da matemática como qualquer outro, estudando propriedades obscuras de modelos dos axiomas de Zermelo-Fraenkel, em vez de questionar as suposições básicas implícitas nesses axiomas e ousando buscar novas abordagens diferentes. [...]

De qualquer forma, agora está bem claro para mim que eu simplesmente não estava lendo as coisas certas. Acho que Rota disse que o trabalho realmente interessante em lógica agora está sob o nome de "ciência da computação", [...] - Semana 40, John Baez, desta semana , [...]

A lógica da ciência da computação é um campo vasto e em rápido desenvolvimento. Acho que toda perspectiva da lógica clássica pode ser modificada para derivar alguma perspectiva da lógica computacional. A entrada da Wikipedia sobre lógica matemática divide o campo em teoria dos conjuntos, teoria dos modelos, teoria das provas e teoria da recursão. Você pode essencialmente pegar essas áreas e adicionar um sabor computacional a elas e obter um subcampo da lógica computacional.

Teoria dos Modelos Gostamos de estudar a teoria dos modelos de lógicas não clássicas e modelos não clássicos da lógica clássica. Com isso, quero dizer que estudamos lógicas modais, temporais e subestruturais e que estudamos lógicas sobre árvores, palavras e modelos finitos, em oposição a modelos clássicos como álgebras. Os dois problemas fundamentais são a satisfação e a verificação do modelo. Ambos têm imenso significado prático e teórico. Em contraste, esses problemas são menos centrais na lógica clássica.

Teoria da prova Estudamos a complexidade e a eficiência com as quais podemos gerar provas em sistemas clássicos de provas, bem como desenvolvemos novos sistemas de prova não clássicos que são sensíveis a considerações de complexidade e eficiência. A dedução automatizada estuda a geração de provas suportada por máquina, em termos gerais. O processo pode envolver interação humana ou ser completamente automático. Há muito trabalho no desenvolvimento de procedimentos de decisão para teorias lógicas. A complexidade da prova se concentra no tamanho das provas e na complexidade computacional da geração de provas. Existe uma linha fascinante de trabalho relacionando programas a provas, que combina com o trabalho descendente da lógica linear para desenvolver sistemas de prova e, consequentemente, linguagens de programação que são sensíveis a recursos.

Teoria da recursão Nossa teoria da recursão é a teoria da complexidade. Em vez de estudar o que é computável, estudamos com que eficiência podemos calcular. Existem muitos análogos da teoria da recursão na teoria da complexidade, mas os resultados e separações da teoria da recursão nem sempre são válidos por seus análogos teóricos da complexidade. Em vez de conjuntos computáveis ​​e uma hierarquia aritmética, temos o tempo polinomial, a hierarquia do tempo polinomial e o espaço polinomial que envolve a hierarquia. Em vez de quantificação limitada na hierarquia aritmética, temos fórmulas booleanas satisfatórias e quantificadas e quantificação limitada de fórmulas booleanas.

O artigo da pesquisa

Sobre a eficácia incomum da lógica na ciência da computação

é um bom ponto de partida para obter uma visão de alto nível da lógica computacional. Vou listar vários campos da ciência da computação, com orientação lógica. Espero que outras pessoas editem esta resposta e adicionem a essa lista aqui, e possivelmente adicionem um link para uma resposta nesta página.

1. Teoria dos modelos finitos
2. Complexidade de prova
3. Dedução algorítmica (procedimentos de decisão para teorias lógicas)
4. Lógica dos programas
5. Lógica dinâmica
6. Lógica temporal linear e suas variantes
7. Lógica de Árvore Computacional e suas variantes
8. Lógica epistêmica
9. Teoria do banco de dados
10. Teoria dos tipos
11. Automatize sobre infinitas palavras
12. Lógica categórica
13. Teoria da concorrência e álgebra de processos
14. Teoria do domínio
15. Lógica linear
16. Complexidade descritiva
17. Verificação de modelo
18. Cálculo de ponto fixo e lógica de fechamento transitivo

uma área de forte sobreposição entre lógica e ciência da computação é uma prova automatizada de teoremas , por exemplo [4]. também, por exemplo, ref [1] é o uso do provador do teorema de Boyer-Moore para verificar / verificar o teorema de Godels. outro resultado importante / impressionante recente é a conclusão recente da verificação de software do teorema das quatro cores (e outros como Odd Order e Feit-Thompson [3]) na pesquisa da Microsoft por Gonthier. [2]

[1] Metamatemática, Máquinas e Prova de Gödel (Tratados de Cambridge em Ciência da Computação Teórica por Shankar)

[2] Uma prova verificada por computador do teorema das quatro cores Georges Gonthier

[3] Algoritmos interessantes na formalização do teorema de Feit-Thompson? tcs.se

[4] Onde e como os computadores ajudaram a provar um teorema? tcs.se