FO (complexidade)

FO é uma classe de complexidade de estruturas que podem ser reconhecidas por fórmulas da lógica de primeira ordem. É a base do campo da teoria da complexidade descritiva e é equivalente à classe de complexidade AC⁰ FO-regulares. Várias extensões de FO, formadas pela adição de certos operadores, dão origem a outras classes de complexidade conhecidas , permitindo que a complexidade de certos problemas seja provada sem ter que recorrer ao nível algorítmico.

Definição e exemplos

A ideia

Quando usamos o formalismo lógico para descrever um problema computacional, a entrada é uma estrutura finita e os elementos dessa estrutura formam o domínio de discurso. Usualmente a entrada é ou uma string (de bits ou sobre um alfabeto) dos elementos que são posições da string, ou um grafo cujos elementos são vértices. O comprimento da entrada será dado pelo tamanho da respectiva estrutura. Qualquer que seja a estrutura, podemos assumir que há relações que podem ser testadas, por exemplo “$E(x,y)$ é verdadeiro se e somente se existe uma aresta de $x$ para $y$” ( no caso da estrutura estar em um grafo), ou “$P(n)$ é verdadeiro se e somente se o $n$-ésimo carácter da string é 1”. Essas relações são os predicados para a lógica de primeira ordem. Também há constantes, que são elementos especiais da respectiva estrutura. Um exemplo é verificar se um dado vértice é alcançável em um certo grafo. Para isso teremos que escolher duas constantes s(início) e t(fim).

Na teoria da complexidade descritiva temos quase sempre que supor que há uma ordem total sobre os elementos e que podemos checar a igualdade entre os elementos. Isso nos permite considerar elementos como números: o elemento $x$ representa o número $n$ se e somente se há $n-1$ elementos $y$ com $x<y$. Graças a isso podemos considerar a primitiva “bit”, onde $bit(x,k)$ é verdadeiro se e somente se o $k$-ésimo bit de $x$ é 1. Podemos substituir a adição e multiplicação por relações ternárias tal que adição$(x,y,z)$ é verdadeiro se e somente se $x+y=z$ e multiplicação$(x,y,z)$ se e somente se $x*y=z$).

Definição formal

A semântica das fórmulas em FO é direta, $\neg A$ é verdadeira se e somente se $A$ é falso, $A$ é verdadeiro e $B$ é verdadeiro se e somente se $A$ é verdadeiro e $B$ é verdadeiro, e $\forall xP(x)$ é verdadeiro se e somente se $P(v)$ é verdadeiro para todos os valores $v$ que $x$ pode ter no universo fundamental.

Propriedades

Justificativa

Dado que elementos computacionais são apenas ponteiros, i.e strings de bits, na complexidade descritiva as premissas que temos tem uma ordem sobre o elemento de uma estrutura faz sentido. Pela mesma razão comumente supomos que ou bit é um predicado ou +, e X, visto que essas funções primitivas podem ser calculadas na maioria das classes de complexidade menores.

FO sem essas primitivas é estudada com mais ênfase na teoria de modelos finitos, e seu equivalente para classes de complexidade menores; essas classes são as decidiveis pela máquina relacional.

Aviso

Um consulta FO irá então ser a avaliação de se uma formula na lógica de primeira ordem é verdadeira sobre uma estrutura representando a entrada para o problema. Não se deve confundir esse tipo de problema com o da checagem de se uma fórmula booleana é verdadeira, que é a definição de QBF, que é PSPACE-completo. A diferença entre esses dois problemas é que em QBF o tamanho do problema é o tamanho da fórmula e elementos são somente valores booleanos, enquanto no FO o tamanho do problema, isto é, o tamanho da estrutura e fórmula, são fixos.

Isso é similar a Complexidade parametrizada mas o tamanho da fórmula não é um parâmetro fixo.

Forma normal

Toda fórmula tem uma equivalente na forma normal prenex (onde todos os quantificadores são escritos primeiramente, seguidos de uma fórmula livre de quantificadores).

Operadores

FO quaisquer operadores

Na complexidade de circuitos, pode-se mostrar a equivalência entre FO e AC⁰, a primeira classe na hierarquia AC. De fato, há uma tradução natural de símbolos de FO a nós de um circuito, com $\forall ,\exists$ sendo $\land$ e $\lor$ de tamanho $n$.

Ponto fixo parcial pertence a PSPACE

FO(PFP) é o conjunto de consultas booleanas definível em FO onde adicionamos um operador de ponto fixo parcial.

Seja um inteiro $k$, $x,y$ de $k$ variáveis, $P$ uma variável de segunda ordem com aridade k e $\phi$ uma função FO(PFP) que usa $k$ e $P$ como variáveis. Podemos iterativamente definir $(P_{i})_{i\in N}$ tal que $P_{0}(x)=falso$ e $P_{i}(x)=\phi (P_{i-1},x)$ (significando $\phi$ com $P_{i-1}$ substituído pela variável de sugunda ordem $P$). Assim, ou há um ponto fixo ou a lista de $(P_{i})$s é cíclica.

PFP($\phi _{P,x})(y)$ é definida como o valor de um ponto fixo de $(P_{i})$ em $y$ se há um ponto fixo, caso contrário falso. Desde que Since $P$s são propriedades de aridade k, há no máximo $2^{n^{k}}$ valores para $P_{i}$s, então com um countador de espaço polinomial podemos checar se há um loop ou não.

É provado que FO(PFP) pertence a PSPACE. Essa definição é equivalente a ($2^{n^{O(1)}}$).

Menor ponto fixo é P

FO(LFP) é o conjunto de consultas booleanas definíveis in FO(PFP) onde o ponto fixo parcial é limitado para ser monótono. Isso é, se a variável de segunda ordem é $P$, então $P_{i}(x)$ sempre implica $P_{i+1}(x)$.

Podemos garantir a monoticidade restringindo a fórmula $\phi$ para as únicas ocorrências positivas de $P$ ( isso é, ocorrências precedidas por um número par de negações). Nós podemos alternativamente descrever LFP($\phi _{P,x}$) como PFP($\psi _{P,x}$) onde $\psi (P,x)=\phi (P,x)\vee P(x)$.

Devido à monoticidade, somente adicionamos vetores para a tabela verdade de $P$, e uma vez que há somente $n^{k}$ vetores possíveis sempre encontraremos um ponto fixo antes $n^{k}$ iterações. Assim sendo, pode ser visto que FO(LFP) = P. Essa definição é equivalente a FO($n^{O(1)}$).

Fecho transitivo é NL

FO(TC) é o conjunto de consultas booleanas definíveis in FO com um operador de fecho transitivo (TC).

TC é definido da seguinte maneira: seja $k$ um inteiro positivo e $u,v,x,y$ um vetor de $k$ variáveis. Então TC($\phi _{u,v})(x,y)$ é verdadeiro se existe $n$ vetores de variáveis $(z_{i})$ tal que z$z_{1}=x,z_{n}=y$, e para todos $i<n$, $\phi (z_{i},z_{i+1})$ é verdadeiro. Aqui, $\phi$ é uma fórmula escrita no FO(TC) e $\phi (x,y)$ significa que as variáveis $u$ e $v$ são substituídas por $x$ e $y$.

Essa classe é equivalente a NL.

Fecho transitivo determinístico é L

FO(DTC) é definido como FO(TC) onde o operador do fecho transitivo é determinístico. Isso significa que quando nós aplicamos DTC($\phi _{u,v}$), nós sabemos que para todo $u$, existe no máximo um $v$ tal que $\phi (u,v)$.

Podemos supor que DTC($\phi _{u,v}$) é açúcar sintático para TC($\psi _{u,v}$)) onde $\psi (u,v)=\phi (u,v)\wedge \forall x,(x=v\vee \neg \psi (u,x))$

Isso mostra que essa classe é equivalente a L.

Forma normal

Qualquer forma normal com um operador de ponto fixo (correspondendo o fecho transitivo) pode, sem perda de generalidade, ser escrito com apenas um operador dos operadores aplicados a 0 (correspondendo $0,(n-1)$).

Iteração

Definimos primeira ordem com iteração, 'FO[$t(n)$]'; onde $t(n)$ aqui é uma classe de funções que mapeiam inteiros em inteiros e, para classes diferentes de funções $t(n)$ obteremos diferentes classes de complexidade FO[$t(n)$].

Nessa seção escreveremos $(\forall xP)Q$ como equivalente de $(\forall x(P\Rightarrow Q))$ e $(\exists xP)Q$ como equivalente a $(\exists x(P\vee Q))$. Primeiramente precisamos definir blocos quantificadores(QB do inglês) como uma lista $(Q_{1}x_{1},phi_{1})...(Q_{k}x_{k},phi_{k})$ onde $phi$is são quantificadores livres de fórmulas FO e $Q$is são ou $\forall$ ou $\exists$. Se $Q$ é um bloco quantificador então chamaremos $[Q]^{t(n)}$ o operador iteração que é definido como $Q$ escrito $t(n)$ vezes. Deve-se observar que aqui há $k*t(n)$ quantificadores na lista mas somente $k$ variáveis sendo cada uma dessas variáveis usadas $t(n)$ vezes.

Definimos ainda FO[$t(n)$] como as FO-fórmulas com um operador iteração cujo expoente está na classe $t(n)$, assim obtendo as seguintes igualdades:

• FO[$(\log n)^{i}$] é equivalente ao FO-Uniforme ACⁱ e de fato FO[t(n)] é FO-Uniforme AC em profundidade $t(n)$.
• FO[$(\log n)^{O(1)}$] é equivalente a NC.
• FO[$n^{O(1)}$] é equivalente a PTIME, o que também é uma moutra maneira de escrever |FO(LFP).
• FO[$2^{n^{O(1)}}$] é equivalente a PSPACE, uma outra forma de escrever FO(PFP).

Lógica sem relações aritméticas

Seja a relação sucessor, succ, uma relação binária tal que ${\rm {{succ}(x,y)}}$ é verdadeira se e somente se $x+1=y$. Sobre a lógica de primeira ordem, succ é estritamente menos expressiva que < que é menos expressiva que + que é menos expressiva que bit. + e X são menos expressivas que bit.

Usando sucessor para definir bit

É possível definir as relações adição e então bit com um fecho transitivo determinístico.

${\rm {{plus}(a,b,c)=({\rm {{DTC}_{v,x,y,z}{\rm {{succ}(v,y)\land {\rm {{succ}(z,x))(a,b,c,0)}}}}}}}}$ e

${\rm {{bit}(a,b)=({\rm {{DTC}_{a,b,a',b'}\psi )(a,b,1,0)}}}}$ com

$\psi ={\text{if }}b=0{\text{ então }}({\text{se }}\exists m(a=m+m+1){\text{ então }}(a'=1\land b'=0){\text{ se-não }}\bot ){\text{ se-não }}({\rm {{succ}(b',b)\land (a+a=a'\lor a+a+1=a')}}$

Isso significa que quando consultamos para o bit 0 checamos a paridade e vamos para (1,0) se $a$ é impar (que é um estado de aceitação), caso contrário rejeitamos. Se checarmos um bit $b>0$, dividimos a por 2 e checamos bit $b-1$.

Assim não faz sentido falar de apenas com sucessores, sem outros predicados.

Lógicas sem sucessores

Ná lógica sem succ, +, x, < ou bit, é formada a igualdade de FO(LFP) para p-relacional e FO(PFP) para PSPACE-relacional, com as classes P e PSPACE sobre máquinas relacionais. O teorema de Abiteboul-Vianu afirma que FO(LFP) = FO(PFP) se e somente se FO(<, LFP) = FO(PFP) e se somente se P = PSPACE. Esse resultado tem sido estendido a outros pontos fixos. Isso nos mostra que o problema de ordem na lógica de primeira ordem é muito mais um problema técnico que um problema fundamental.

Bibliografia

• Ronald Fagin, Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. Complexity of Computation, ed. R. Karp, SIAM-AMS Proceedings 7, pp. 27–41. 1974.
• Ronald Fagin, Finite model theory-a personal perspective. Theoretical Computer Science 116, 1993, pp. 3–31.
• Neil Immerman. Languages Which Capture Complexity Classes. 15th ACM STOC Symposium, pp. 347–354. 1983.

Ligações externas

• Neil Immerman's descriptive complexity page, including a diagram (inglês)
• zoo about FO, see the class under it also (inglês)