Existe uma lógica sem indução que captura muito de P?

38

O teorema de Immerman-Vardi afirma que PTIME (ou P) é precisamente a classe de idiomas que pode ser descrita por uma frase da Lógica de Primeira Ordem, juntamente com um operador de ponto fixo, sobre a classe de estruturas ordenadas. O operador de ponto fixo pode ser o ponto menos fixo (como considerado por Immerman e Vardi) ou o ponto fixo inflacionário. (Stephan Kreutzer, Equivalência expressiva da lógica de ponto fixo mínimo e inflacionário , Annals of Pure and Applic 130 130-78, 2004).

Yuri Gurevich conjeturou que não há lógica para capturar o PTIME ( Lógica e o Desafio da Ciência da Computação , nas Tendências Atuais da Ciência da Computação Teórica, ed. Egon Boerger, 1–57, Computer Science Press, 1988), enquanto Martin Grohe afirmou que é menos certo ( The Quest for a Logic Capture PTIME , FOCS 2008).

O operador de ponto fixo deve capturar o poder da recursão. Os pontos fixos são poderosos, mas não é óbvio para mim que eles são necessários.

Existe um operador X que não seja baseado em pontos fixos, de modo que o FOL + X capture um fragmento (grande) de PTIME?

Edit: Tanto quanto eu entendo, a lógica linear só pode expressar declarações sobre estruturas que têm forma bastante restritiva. Idealmente, gostaria de ver uma referência ou um esboço de uma lógica que possa expressar propriedades de conjuntos arbitrários de estruturas relacionais, evitando ainda pontos fixos. Se eu estiver errado sobre o poder expressivo da lógica linear, um ponteiro ou dica seria bem-vinda.

András Salamon
fonte
2
Com "lógica", quero dizer o que Grohe quer dizer: um conjunto decidível de sentenças sobre o vocabulário e uma relação "é um modelo de" entre estruturas finitas e sentenças, com a propriedade de que o conjunto de modelos de uma sentença é sempre fechado sob isomorfismo .
András Salamon
Consulte também cstheory.stackexchange.com/questions/174/… para saber se existe uma lógica que captura PTIME.
András Salamon
A lógica linear é uma lógica proposicional que contém lógica proposicional clássica. Pode ser estendido para permitir quantificadores. Mas se me lembro corretamente, a relação entre lógica linear (proposicional) e classes de complexidade é diferente da que Grohe tem em mente, pelo menos não vejo como relacionar lógica linear a consultas sobre estruturas finitas.
Kaveh
Existem teorias de conjuntos baseadas na lógica linear, como a Light Affine Set Theory de Terui, que possui a propriedade de que uma função pode ser provada total nela, se e somente se a função for computável em tempo polinomial. Veja citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730
Neel Krishnaswami
1
Kaveh, foi por isso que concedeu a recompensa a Slimton. Uma resposta mais detalhada ainda seria legal.
András Salamon

Respostas:

23

Você quer dar uma olhada no que algumas pessoas chamam de Teorema de Grädel. Você pode encontrá-lo no livro de Papadimitriou "Complexidade Computacional" (é Teorema 8.4 na página 176) ou no original de GRADEL papel .

Em poucas palavras, o Teorema de Grädel é P o que o Teorema de Fagin é para NP. Ele afirma que, na classe de estruturas finitas com uma relação sucessora, a coleção de propriedades decidíveis em tempo polinomial coincide com as expressáveis ​​no fragmento de Horn da lógica existencial de segunda ordem. Estas são as sentenças da lógica de segunda ordem da forma que R é uma sequência de variáveis ​​de segunda ordem, x é uma sequência de variáveis ​​de primeira ordem e ϕ é um quantificador fórmula livre que, quando escrita na forma CNF, é uma conjunção de R

(R)(x)(ϕ)
RxϕRCláusulas -Horn (ou seja, cláusulas que possuem no máximo um átomo não negado envolvendo as variáveis ​​em ).R
Slimton
fonte
3
Opa, agora que li sua pergunta novamente, percebo que ela é um pouco diferente da versão anterior. Agora você pede um operador X para que o FOL + X capture um grande fragmento de P. Nesse caso, você deve dar uma olhada no <a href=" logcom.oxfordjournals.org/content/5/2/…> de Dawar . mostra que, se existe uma lógica para P, então há um que se estende por FOL com quantificadores generalizadas.
slimton
3
Devo acrescentar que o fragmento de Horn da lógica existencial de segunda ordem em estruturas nuas é bastante fraco: um subconjunto adequado de LFP em estruturas nuas. Precisamos do sucessor para obter o teorema de Grädel. O resultado de Dawar é para estruturas nuas.
slimton 27/09/10
8
Tanto quanto eu entendo, a lógica linear só pode expressar afirmações sobre estruturas que têm forma bastante restritiva. Idealmente, gostaria de ver uma referência ou um esboço de uma lógica que possa expressar propriedades de conjuntos arbitrários de estruturas relacionais, evitando ainda pontos fixos. Se eu estiver errado sobre o poder expressivo da lógica linear, um ponteiro ou dica seria bem-vinda.

Isso não está certo: todas as redes monoidais comutativas residuais são modelos de lógica linear. Aqui está uma maneira fácil de criar essa estrutura a partir de gráficos finitos. Comece com o conjunto

M={(g,n)|g is a finite graph and nnodes(g)}

(g,n)ϕnϕ():M×MM

(g,n)(g,n)={(g,nn)when g=gnn=undefinedotherwise

Isso combina dois elementos, mesclando seus conjuntos de propriedade, se os gráficos forem iguais e os conjuntos de propriedade forem separados.

Agora, podemos dar um modelo de lógica linear da seguinte maneira:

(g,n)In=(g,n)ϕψn1,n2.n=n1n2 and (g,n1)ϕ and (g,n2)ψ(g,n)ϕψn.if nn= and (g,n)ϕ then (g,nn)ψ(g,n)always(g,n)ϕψ(g,n)ϕ and (g,n)ψ

Esse modelo é na verdade uma variante dos usados ​​na lógica de separação, amplamente usada na verificação de programas de manipulação de heap. (Se quiser, pense no gráfico como a estrutura do ponteiro da pilha, e a analogia é exata!)

Porém, essa não é a maneira correta de pensar sobre a lógica linear: suas reais intuições são teóricas da prova e a conexão com a complexidade vem da complexidade computacional do teorema da eliminação de cortes. A teoria modelo da lógica linear é a sombra projetada por sua teoria da prova.

Neel Krishnaswami
fonte
Qual o papel da estrutura gráfica no modelo acima? A definição acima parece funcionar bem se dissermos que g varia sobre os gráficos discretos.
Charles Stewart
Como qualquer monóide comutativo (parcial) pode ser usado para fornecer um modelo de lógica linear / BI, a estrutura do gráfico não é usada para interpretar os e - apenas importa para as proposições atômicas. Por exemplo, na lógica de separação, existe uma proposição atômica de "pontos a" , que usamos a estrutura do ponteiro para interpretar. n n 'nn
Neel Krishnaswami
8

Há resultados interessantes recentes sobre a busca de uma lógica que captura PTIME. O famoso exemplo de Cai, Fürer e Immerman, mostrando que o LFP + C não captura o PTIME, foi baseado em uma classe de gráficos aparentemente artificial. Obviamente, foi construído para a tarefa específica de demonstrar as restrições do LFP + C. Apenas recentemente foi demonstrado por Dawar que a classe não é artificial. Pode ser visto como um exemplo do fato de que o LFP + C não pode resolver sistemas de equações lineares!

Portanto , Dawar, Grohe, Holm e Laubner estenderam lógicas por operadores de álgebra linear, por exemplo, por um operador para definir a classificação de uma matriz definível. A classificação LFP + lógica resultante pode expressar estritamente mais do que LFP + C; na verdade, não há propriedade PTIME conhecida que a classificação LFP + não possa expressar.

Mesmo o FO + rk é surpreendentemente poderoso, pode expressar um fechamento transitivo determinístico e simétrico. Ainda está em aberto se ele pode expressar o fechamento transitivo geral de um gráfico.

Sebastian Siebertz
fonte
1
Observe que Anderson / Dawar / Holm mostrou recentemente que FP + C pode expressar programação linear ( arxiv.org/abs/1304.6870 ). Isso prejudica uma interpretação do resultado anterior de Dawar, na linha de "FP + C não pode resolver sistemas de equações lineares"; Dawar afirmou apenas que alguns "problemas naturais que envolvem sistemas de equações lineares não são definíveis nessa lógica" com os quais ele parece ter significado cálculos de classificação.
András Salamon
7

Dependendo do que você quer dizer com "captura", a Lógica Linear Suave e o Tempo Polinomial de Yves Lafont podem ser interessantes. Existe uma correspondência de 1 a 1 para provas nessa lógica e nos algoritmos PTIME que usam uma string como entrada e saída 0 ou 1.

O artigo da Wikipedia sobre lógica linear está aqui . Não é uma lógica de ponto fixo. A intuição da "lógica clássica sobre álgebras vez de álgebras booleanas" é a mais fácil de entender.C

Aaron Sterling
fonte
1
Eu acho que András quer uma lógica no sentido de complexidade descritiva.
Kaveh
7

Alguns trabalhos mais antigos sobre esse problema, novamente na veia da Lógica Linear, são Jean-Yves Girard, Andre Scedrov e Philip Scott. Lógica linear limitada: uma abordagem modular à computabilidade em tempo polinomial. Teoria da Ciência da Computação, 97 (1): 1–66, 1992.

Trabalhos mais recentes incluem Lógica Linear Limitada, revisitada por Ugo Dal Lago e Martin Hofmann.

Dave Clarke
fonte