A pergunta que guia a nossa investigação é:

“Como compreender e explicar propriedades estruturais em um dataset massivo?”

Para responder a essa pergunta com explicabilidade formal, não basta determinar se uma propriedade é verdadeira ou falsa; é necessário inspecionar os certificados (testemunhas concretas) que justificam a sua satisfação. A abordagem categórica constrói o espaço de potenciais certificados via Espaço de Estratégias e isola as soluções na Variedade de Certificados.

1. O Espaço de Estratégias

Para uma fórmula de primeira ordem \(\phi\) sobre um grafo finito \(G\), o Espaço de Estratégias \(\operatorname{Strat}_\phi(G)\) é o objeto da categoria dos conjuntos e funções que codifica o espaço de potenciais atribuições para as variáveis da fórmula.

Para sentenças com alternância de quantificadores \(\forall x_n \exists y_n\), as escolhas para as variáveis existenciais dependem das variáveis universais precedentes. Na teoria das categorias, espaços de funções são formalizados por objetos exponenciais, então os espaços de estratégias são definidos recursivamente por:

\[ \operatorname{Strat}_{n}(G) = G[s_n]^{\operatorname{Strat}_{n-1}(G) \times G[t_n]}, \qquad \operatorname{Strat}_0(G) = 1, \]

em que:

• \(t_n\) é o tipo da variável universal \(x_n\) no modelo (como vértices ou arestas de \(G\));
• \(s_n\) é o tipo da variável existencial \(y_n\);
• \(\operatorname{Strat}_0(G) = 1\) é o objeto terminal da categoria, representando o contexto inicial vazio.

Para uma fórmula \(\phi\) com \(k\) blocos de alternância de quantificadores, o espaço total de estratégias corresponde ao estágio final da recursão: \(\operatorname{Strat}_\phi(G) = \operatorname{Strat}_k(G)\). Dessa forma, cada elemento de \(\operatorname{Strat}_\phi(G)\) corresponde a uma função de Skolem categórica, mapeando cada configuração universal em uma resposta existencial compatível.

Exemplo

Para ilustrar a construção dos exponenciais, considere o seguinte grafo \(G\) com dois vértices e duas arestas:

Sobre esse modelo, avalia-se uma sentença com apenas um par de alternância (\(k = 1\)): \[ \phi \equiv \forall v:\text{Vertex} \; \exists e:\text{Edge} \; (\operatorname{src}(e) = v), \] expressando que todo vértice possui ao menos uma aresta incidente de saída.

Nesta especificação:

• A variável universal \(v\) possui tipo \(t_1 = \text{Vertex}\), com domínio \(G[t_1] = \{v_1, v_2\}\);
• A variável existencial \(e\) possui tipo \(s_1 = \text{Edge}\), com domínio \(G[s_1] = \{e_1, e_2\}\).

O objeto exponencial de estratégias é obtido diretamente da recursão: \[ \operatorname{Strat}_\phi(G) = \operatorname{Strat}_1(G) = G[\text{Edge}]^{\operatorname{Strat}_0(G) \times G[\text{Vertex}]} \cong G[\text{Edge}]^{G[\text{Vertex}]}. \]

Substituindo os conjuntos concretos do modelo \(G\), escreve-se o objeto exponencial: \[ \operatorname{Strat}_\phi(G) = \{e_1, e_2\}^{\{v_1, v_2\}}. \]

O espaço \(\operatorname{Strat}_\phi(G)\) consiste em todas as funções de Skolem \(f: \{v_1, v_2\} \to \{e_1, e_2\}\), totalizando \(|E(G)|^{|V(G)|} = 2^2 = 4\) estratégias candidatas:

Cada elemento do objeto exponencial gera uma árvore de atribuição. A raiz representa o estágio inicial \(\operatorname{Strat}_0(G) = 1\), as ramificações de primeiro nível representam as escolhas universais \(v \in \{v_1, v_2\}\), e os ramos seguintes representam as respostas existenciais \(e = f(v)\) selecionadas pela estratégia.

As 4 árvores de atribuição geradas pelo exponencial são ilustradas abaixo:

Podemos observar que uma árvore é um certificado para um problema apenas se todas as suas ramificações são válidas.

2. A Variedade de Certificados

Como nem todas as estratégias satisfazem a propriedade desejada, a fórmula \(\phi\) induz um morfismo característico:

\[ \phi_G : \operatorname{Strat}_\phi(G) \to 2, \]

onde \(2 = \{\top, \bot\}\) é o classificador de subobjetos da categoria dos conjuntos.

Para isolar apenas as estratégias que tornam a fórmula verdadeira, calcula-se o pullback de \(\phi_G\) ao longo da constante \(\top : 1 \rightarrowtail 2\), definindo a Variedade \(\mathbb{V}\phi_G\):

O subobjeto resultante \(\mathbb{V}\phi_G \rightarrowtail \operatorname{Strat}_\phi(G)\) reúne todos os certificados que atestam \(G \models \phi\).

3. Mapeamento de Certificados

Lema: Sejam \(\operatorname{Strat}_\phi(G)\) e \(\operatorname{Strat}_\psi(H)\) dois espaços de estratégias e \(r : \operatorname{Strat}_\phi(G) \to \operatorname{Strat}_\psi(H)\) uma função. Se o pullback do cospan \[ \operatorname{Strat}_\phi(G) \xrightarrow{r} \operatorname{Strat}_\psi(H) \leftarrowtail \mathbb{V}\psi_H \] coincide com a variedade \(\mathbb{V}\phi_G\), então:

1. Equivalência: A propriedade \(\phi\) é satisfeita em \(G\) se e somente se \(\psi\) é satisfeita em \(H\) (\(G \models \phi \iff H \models \psi\)).
2. Correspondência: Uma estratégia \(s \in \operatorname{Strat}_\phi(G)\) é um certificado para \(\phi\) sobre \(G\) se e somente se sua imagem \(r(s)\) é um certificado para \(\psi\) sobre \(H\): \[ s \in \mathbb{V}\phi_G \iff r(s) \in \mathbb{V}\psi_H. \]
3. Explicabilidade: Cada certificado simplificado \(s_H \in \mathbb{V}\psi_H\) particiona e explica uma família inteira de certificados originais dada pela pré-imagem \(r^{-1}(s_H) \subseteq \mathbb{V}\phi_G\).

Demonstração: Na categoria dos conjuntos, o pullback do monomorfismo \(\mathbb{V}\psi_H \rightarrowtail \operatorname{Strat}_\psi(H)\) ao longo de \(r\) é dado pela pré-imagem \(r^{-1}(\mathbb{V}\psi_H) = \{ s \in \operatorname{Strat}_\phi(G) \mid r(s) \in \mathbb{V}\psi_H \}\). Pela hipótese de que este objeto coincide com a variedade \(\mathbb{V}\phi_G\), temos a igualdade de conjuntos \(\mathbb{V}\phi_G = r^{-1}(\mathbb{V}\psi_H)\), estabelecendo diretamente (2). Como a variedade de certificados de um modelo é não-vazia se e somente se a propriedade é satisfeita, segue a equivalência (1). Por fim, cada elemento \(s_H \in \mathbb{V}\psi_H\) tem como pré-imagem o conjunto de certificados \(r^{-1}(s_H) \subseteq \mathbb{V}\phi_G\), estabelecendo (3). \(\blacksquare\)

Quando essa condição é satisfeita, as variedades e os espaços de estratégias formam o seguinte pullback:

Explicabilidade

Esse lema aprimora o procedimento booleano do sub_formula_search: enquanto a busca original garantia apenas uma implicação booleana trivial, o lema assegura a transferência efetiva dos certificados. Em um grafo massivo \(G\), onde inspecionar \(\operatorname{Strat}_\phi(G)\) diretamente é inviável, aplica-se o lema instanciando o modelo reduzido como o quociente \(H = G/P\):

1. Identificar um subgrafo característico \(P \rightarrowtail G\).
2. Construir o grafo quociente \(G/P\) via pushout do span \(1 \xtwoheadleftarrow{!} P \rightarrowtail G\), comprimindo \(P\) a um vértice terminal.
3. Buscar uma fórmula \(\psi\) e um mapa \(r\) entre os espaços de estratégias (\(r : \operatorname{Strat}_\phi(G) \to \operatorname{Strat}_\psi(G/P)\)).
4. Validar o pullback: Quando a condição do lema é satisfeita, inspecionar a fórmula mais simples sobre o modelo reduzido \(G/P\) é suficiente para certificar e explicar as testemunhas originais em \(G\).

Esta seção detalha a arquitetura desenvolvida para operacionalizar a teoria. A implementação foi realizada na linguagem Julia com a biblioteca de matemática categórica Catlab.jl, operando sobre a categoria dos grafos direcionados.

1. Grounding Categórico

O núcleo da abordagem consiste na tradução de sentenças de primeira ordem \(\phi\) diretamente em subobjetos \(\mathrm{Subobject}(G)\), em que \(G\) é um grafo finito. Essa tradução é dada através da álgebra de subobjetos descrita nos pré-requisitos.

1.1. Pipeline

O processamento de uma fórmula é decomposto em três etapas:

• Lexer: Converte a fórmula textual em uma sequência de símbolos tipados.
• Parser: Constrói a Árvore Sintática Abstrata (AST) recursiva encapsulando os quantificadores, operadores e predicados.

Por exemplo, a propriedade de existência de um caminho de comprimento 2:

input = "∃v1:Vertex ∃v2:Vertex ∃v3:Vertex
         ∃e1:Edge ∃e2:Edge (
           ((src(e1) = v1) ∧ (tgt(e1) = v2)) ∧
           ((src(e2) = v2) ∧ (tgt(e2) = v3))
         )"

é mapeada em uma árvore na qual os quantificadores aninham o corpo lógico.

1.2. Avaliação Recursiva do Grounding

A função grounding(ϕ::Formula, G::Graph)::Subobject processa recursivamente a AST sobre o modelo \(G\), mantendo um ambiente de variáveis que vincula os identificadores da fórmula aos subobjetos elementares do modelo.

Quantificação Existencial \(\exists x:T \big( \psi \big)\)

A quantificação existencial sobre o domínio finito do modelo \(G\) é computada acumulando a disjunção lógica (join) de subobjetos:

1. Inicia-se com o subobjeto vazio \(\bot = \mathrm{Subobject}(G)\).
2. Caso \(T = \text{Vertex}\), itera-se sobre cada vértice \(v \in V(G)\), associando à variável \(x\) o subobjeto pontual \(\mathrm{Subobject}(G, V=[v])\).
3. Caso \(T = \text{Edge}\), itera-se sobre cada aresta \(e \in E(G)\), associando à variável \(x\) o subobjeto \(\mathrm{Subobject}(G, V=[\operatorname{src}(e), \operatorname{tgt}(e)], E=[e])\).
4. A cada elemento, acumula-se o join na álgebra de Heyting de subobjetos: \[\mathrm{aux} \leftarrow \mathrm{aux} \lor \mathrm{grounding}(\psi)\]

Quantificação Universal \(\forall x:T \big( \psi \big)\)

De forma dual, a quantificação universal acumula a conjunção lógica (meet) de subobjetos:

1. Inicia-se com o subobjeto total \(\top = G = \mathrm{Subobject}(G, V=V(G), E=E(G))\).
2. Itera-se sobre cada elemento do domínio correspondente, acumulando o meet da álgebra de subobjetos: \[\mathrm{aux} \leftarrow \mathrm{aux} \land \mathrm{grounding}(\psi)\]

Predicados \(\operatorname{src}\) e \(\operatorname{tgt}\)

Os predicados de incidência utilizam os morfismos representáveis pré-computados. O grafo com uma aresta \(\Gamma_E\) possui dois morfismos canônicos \(\Gamma_{src}, \Gamma_{tgt} : \Gamma_V \to \Gamma_E\), onde \(\Gamma_V\) é o grafo de um vértice isolado. Dado o monomorfismo \(m_e : \mathrm{dom}(m_e) \rightarrowtail G\) da aresta vinculada à variável:

\[\operatorname{src}(e) = \mathrm{Subobject}(m_e \circ \Gamma_{src} : \Gamma_V \rightarrowtail G)\] \[\operatorname{tgt}(e) = \mathrm{Subobject}(m_e \circ \Gamma_{tgt} : \Gamma_V \rightarrowtail G)\]

1.3. Exemplo de uso

using Catlab, Pam

# 1. Definição do grafo modelo G (ciclo orientado C3)
G = Graph(3)
add_edges!(G, [1, 2, 3], [2, 3, 1])

# 2. Sentença: "Existe um ciclo direcionado de comprimento 3"
input = "∃v1:Vertex ∃v2:Vertex ∃v3:Vertex ∃e1:Edge ∃e2:Edge ∃e3:Edge " *
        "((((((src(e1) = v1) ∧ (tgt(e1) = v2)) ∧ (src(e2) = v2)) ∧ " *
        "(tgt(e2) = v3)) ∧ (src(e3) = v3)) ∧ (tgt(e3) = v1))"

# 3. Execução do pipeline: Lexer -> Parser -> Grounding
formula = parser(lexer(input))
χG = grounding(formula, G)

# Sendo a fórmula satisfeita em G, o subobjeto retornado coincide com o modelo total
println("Vértices no suporte: ", nv(dom(hom(χG)))) # 3
println("Arestas no suporte: ", ne(dom(hom(χG))))  # 3

2. O Algoritmo de Busca de Fórmulas

O procedimento sub_formula_search automatiza a descoberta de fórmulas \(\psi\) e dos quocientes \(G/P\) a partir do subobjeto \(\phi_G\).

Etapa 1: Extração de Padrões

O algoritmo calcula o conjunto de homomorfismos \(\{f \mid f: G \to \Omega\}\). Cada homomorfismo atua como uma função característica \(\chi_P: G \to \Omega\) para algum subgrafo \(P \rightarrowtail G\). O algoritmo extrai cada subgrafo \(P \subseteq G\) calculando o pullback de \(\chi_P\) ao longo do mapa \(\top: 1 \to \Omega\).

Etapa 2: Construção do Grafo Quociente

Para cada padrão \(P\) descoberto, o grafo quociente \(G/P\) é gerado via pushout do span \(1 \xtwoheadleftarrow{!} P \rightarrowtail G\):

Etapa 3: Enumeração de Fórmulas Candidatas

Sobre o modelo reduzido \(G/P\), geramos árvores sintáticas para fórmulas de primeira ordem \(\psi\) criando um domínio enumerável via generate_binary_trees e respectivo preenchimento de seus vértices.

Etapa 4: Validação por Pullback

Para cada fórmula candidata \(\psi\), calcula-se o pullback \(L\) da avaliação \(\psi_{G/P}\) ao longo do epimorfismo \(e: G \twoheadrightarrow G/P\):

A relação de implicação \((G \models \phi) \implies (G/P \models \psi)\) é verificada checando se \(\phi_G \subseteq L\) via is_subimage:

Essa estrutura corresponde à implementação da função:

function sub_formula_search(G::Graph, ϕG::Subobject, max_n::Int=nv(G);
                            take_patterns::Int=typemax(Int), take_formulas::Int=typemax(Int))
    # 1. Extração de padrões estruturais via subobjetos de G
    pattern_pool = collect(subobjects(G))
    sort!(pattern_pool, by=subP -> nv(dom(hom(subP))) + ne(dom(hom(subP))), rev=true)

    results = Tuple{ACSetTransformation, Vector{Formula}}[]

    for subP in pattern_pool
        m_P_G = hom(subP)
        P = dom(m_P_G)
        u_P_T = homomorphism(P, T)

        # 2. Grafo quociente Gp e epimorfismo e via pushout
        po_m_u = pushout[Grph](m_P_G, u_P_T)
        Gp = ob(po_m_u)
        e_G_Gp = legs(po_m_u)[1]

        # 3. Enumeração sistemática de fórmulas candidatas ψ
        # (espaço combinatorial gerado via generate_binary_trees e quantificadores)
        # ...
        for candidate_ψ in formula_pool
            # 4. Avaliação e validação categórica por pullback
            ψGp = grounding(candidate_ψ, Gp)
            m_SψGp_Gp = hom(ψGp)

            pb_m_e = pullback[Grph](m_SψGp_Gp, e_G_Gp)
            m_L_G = legs(pb_m_e)[2]

            # Verificação se ϕG ⊆ L via is_subimage
            if is_subimage(hom(ϕG), m_L_G)
                push!(pattern_formulas, candidate_ψ)
                # ...
            end
        end
        # ...
    end
    return results
end

Corretude Trivial do Algoritmo

Pela propriedade universal do pullback, a condição de inclusão \(\phi_G \subseteq L\) equivale à comutação no classificador de subobjetos com a desigualdade \(\chi_{\phi_G} \le \chi_{\psi_{G/P}} \circ e\). Como o epimorfismo \(e : G \twoheadrightarrow G/P\) preserva a estrutura, isso garante tautologicamente que:

\[ (G \models \phi) \implies (G/P \models \psi). \]

Limitação da Abordagem Booleana

Essa corretude é de certa forma trivial justamente porque opera apenas no nível booleano: o grounding de uma sentença fechada produz apenas dois subobjetos possíveis — o grafo total \(G\) (se satisfeita) ou o subobjeto vazio \(\emptyset\) (se insatisfeita):

• Se \(G \models \phi\), temos \(\phi_G = G\). Para qualquer fórmula \(\psi\) que seja satisfeita no quociente (\(G/P \models \psi\)), seu subobjeto é \(\psi_{G/P} = G/P\) e seu pullback ao longo do epimorfismo é \(L = G\). A condição \(G \subseteq G\) é sempre satisfeita (\(\top \implies \top\)).
• Se \(G \not\models \phi\), temos \(\phi_G = \emptyset\). Como o subobjeto vazio está contido em qualquer subobjeto (\(\emptyset \subseteq L\)), a condição é satisfeita para qualquer fórmula \(\psi\) (\(\bot \implies \top\) e \(\bot \implies \bot\)).

Dessa forma, o critério aceita qualquer fórmula verdadeira sobre \(G/P\), sem vincular os elementos que tornam \(\phi\) verdadeira em \(G\) aos que tornam \(\psi\) verdadeira no quociente, deixando de reter os certificados específicos da satisfação de \(\phi\).

Conexão com a Teoria das Estratégias

Essa limitação motivou a principal direção teórica deste projeto: para vincular testemunhas entre o grafo original e o modelo reduzido, é necessário abandonar a verificação booleana e construir espaços de certificados. Essa transição para os espaços de estratégias \(\operatorname{Strat}_\phi(G)\), as variedades \(\mathbb{V}\phi_G\) e o lema de levantamento de certificados é apresentada formalmente na aba Estratégias.

Ferramental Categórico

Lógica Proposicional em conjuntos

A teoria das categorias nos permite ver fórmulas proposicionais da lógica como morfismos e objetos de uma categoria através da construção de um equalizador. Na categoria dos conjuntos, dado um objeto \(A\) e um predicado \(\phi\) avaliado sobre ele, podemos enxergar esse predicado como uma função \(\phi : A \to 2\), em que \(2 = \{\top, \bot\}\) codifica a noção de verdade. Se calcularmos o equalizador \((E, e)\) de \(\phi\) com o mapa “verdade” (\(A \xrightarrow{!} 1 \xrightarrow{\top} 2\)), o objeto \(E\) vai representar exatamente a “variedade” da fórmula proposicional, ou seja, o subconjunto dos elementos de \(A\) que satisfazem a fórmula. Já o morfismo \(e : E \to A\) é um monomorfismo que injeta essa variedade no modelo.

Isso pode ser visualizado através do seguinte diagrama de equalizador:

Lógica Proposicional em um Topos

Na teoria dos topoi, generalizamos essa noção para construir o mesmo em qualquer topos. O conjunto de valores verdade \(2\) é generalizado pelo conceito de classificador de subobjetos, denotado por \(\Omega\). E a noção de subconjunto e de sua injeção no conjunto original é generalizada para a definição de um subobjeto. Um subobjeto, na teoria das categorias, é uma classe de equivalência de monomorfismos com o mesmo codomínio.

Da mesma forma que nos conjuntos, o equalizador com o morfismo verdade \(\top_X : X \to 1 \xrightarrow{\top} \Omega\) estabelece uma bijeção canônica entre subobjetos de \(X\) e morfismos \(\phi : X \to \Omega\). Assim, para cada monomorfismo \(e : V \rightarrowtail X\), o morfismo associado \(\chi_e : X \to \Omega\) é denominado seu morfismo característico.

Álgebra de subobjetos (proposições) em um Topos

Os subobjetos de um dado objeto \(X\) formam um reticulado fechado por operações elementares como meet, join e pseudocomplemento. Isso garante que os subobjetos são fechados por conectivos lógicos.

Dessa forma, se \(f_1\) e \(f_2\) são proposições (representadas por seus respectivos subobjetos) sobre \(X\), a composição lógica delas, como \(f_1 \land f_2\) ou \(f_1 \lor f_2\), resulta naturalmente em novos subobjetos válidos.

Grounding na lógica de primeira ordem

O grounding é uma técnica que permite traduzir uma fórmula de primeira ordem (FO) para uma fórmula proposicional quando o domínio é finito.

Para isso, as variáveis são substituídas pelos elementos do domínio e os quantificadores são eliminados por meio de operações finitas: uma quantificação existencial é transformada em uma disjunção sobre todos os possíveis valores da variável, enquanto uma quantificação universal é transformada em uma conjunção.

Por exemplo, se queremos quantificar sobre o conjunto \(A = \{a, b, c\}\) na fórmula

\[ \forall x, \exists y \Big( \phi(x, y) \Big), \]

podemos transformar primeiramente a quantificação existencial em uma disjunção sobre todos os elementos de \(A\)

\[ \forall x \Big( \phi(x,a) \lor \phi(x,b) \lor \phi(x,c) \Big). \]

Em seguida, transformamos a quantificação universal em uma conjunção sobre todos os valores possíveis de \(x\):

\[ \begin{aligned} & \Big( \phi(a,a) \lor \phi(a,b) \lor \phi(a,c) \Big) \land \\ & \Big( \phi(b,a) \lor \phi(b,b) \lor \phi(b,c) \Big) \land \\ & \Big( \phi(c,a) \lor \phi(c,b) \lor \phi(c,c) \Big). \end{aligned} \]

Grounding em Topoi

Em um topos, o grounding é computado diretamente na álgebra de Heyting dos subobjetos do modelo. O subobjeto resultante corresponde ao morfismo característico \(\chi_{\phi} : X \to \Omega\), permitindo manipular sentenças de primeira ordem na linguagem interna do topos.

Complexidade Descritiva e Teorema de Fagin

O teorema de Fagin, da complexidade descritiva, estabelece que as propriedades de estruturas finitas expressas por sentenças da lógica existencial de segunda ordem (\(\exists\text{SO}\)) são precisamente aquelas decidíveis em tempo polinomial não determinístico (NP).

Neste trabalho, restringimo-nos aos problemas da classe NP descritíveis por sentenças de primeira ordem sobre grafos finitos.