Endpoint Sufficiency Behavioral Quotients

Resumo Técnico: Quando o Esquecimento da Proveniência é Lícito?

Enunciado do Problema
Sistemas generativos frequentemente produzem objetos que podem ser representados em múltiplos níveis de abstração. Uma representação captura apenas o "ponto final visível" (o objeto final), enquanto outra retém a "proveniência" completa (ancestralidade, eventos de fusão, estruturas de dependência). Embora as representações de ponto final sejam menores, elas correm o risco de serem descrições falsas de estado se as leis de admissibilidade do sistema dependerem da linhagem. O problema central abordado é determinar exatamente quando a informação de proveniência pode ser esquecida com segurança sem alterar o comportamento futuro lícito do sistema. Especificamente, o artigo questiona: quando uma projeção de ponto final retém informação suficiente para determinar transições lícitas, e qual é a quantidade máxima de proveniência que pode ser descartada?

O artigo desafia a suposição informal de que a "suficiência do ponto final" é um conceito único e uniforme. Ele demonstra que essa noção varia dependendo do nível de observação: se um se preocupa apenas com regras imediatamente habilitadas, sequências finitas de rótulos de regras (traços) ou a estrutura de ramificação completa das possibilidades futuras.

Metodologia
O autor formaliza o problema utilizando Sistemas de Transição Generativa Lícitos (LGTS). Um LGTS é definido como uma tupla $T = (S, \Sigma, \to, U, X, \cong_X)$, onde:

• $S$ é um conjunto de ocorrências decoradas com proveniência.
• $\Sigma$ é um conjunto de rótulos de regras.
• $\to$ é a relação de transição rotulada lícita.
• $U: S \to X$ é uma projeção de ponto final que mapeia ocorrências para objetos visíveis.
• $\cong_X$ é uma relação de equivalência sobre os objetos visíveis.

O estudo analisa a relação entre a relação de equivalência de ponto final ($\equiv_U$, onde $s \equiv_U t \iff U(s) \cong_X U(t)$) e várias equivalências comportamentais. A análise procede através de três níveis distintos de observação:

1. Suficiência de Habilitação: Preservar o conjunto de rótulos de regras imediatamente disponíveis.
2. Suficiência de Traço: Preservar o conjunto de todos os traços finitos de rótulos de regras.
3. Suficiência de Quociente (Ramificação): Preservar a estrutura de transição de ramificação para o futuro modulo a equivalência de ponto final.

O artigo emprega ferramentas padrão de semântica de processos, incluindo equivalência de traço, bisimulação forte, coindução e refinamento de partição, aplicadas especificamente à fronteira entre o ponto final e a proveniência.

Principais Contribuições e Resultados

1. Uma Hierarquia Estrita de Três Níveis
O artigo estabelece que os três níveis de suficiência são distintos e formam uma hierarquia estrita:
$$\text{Suficiência de Quociente} \implies \text{Suficiência de Traço} \implies \text{Suficiência de Habilitação}$$

• Suficiência de Habilitação é a mais fraca; exige apenas que pontos finais equivalentes tenham o mesmo conjunto de próximos movimentos habilitados.
• Suficiência de Traço exige que pontos finais equivalentes gerem o mesmo conjunto de sequências finitas de rótulos de regras.
• Suficiência de Quociente é a mais forte; exige que o conjunto de classes de ponto final alcançáveis para qualquer rótulo dependa apenas da classe de ponto final atual, não da história específica da proveniência.

2. Critérios Exatos de Suficiência
O artigo fornece critérios matemáticos precisos para quando uma projeção de ponto final é suficiente em cada nível:

• Nível de Traço: A projeção é suficiente para o traço se, e somente se, a equivalência de ponto final for um subconjunto da equivalência de traço ($\equiv_U \subseteq \equiv_{tr}$).
• Nível de Ramificação: A projeção é suficiente para o quociente se, e somente se, a equivalência de ponto final for uma equivalência de bisimulação forte. Isso significa que, para quaisquer dois estados equivalentes por ponto final, toda transição de um pode ser correspondida por uma transição do outro para um estado que também seja equivalente por ponto final.

3. Reparos Canônicos e Esquecimento Máximo
Quando a equivalência bruta de ponto final falha em ser suficiente, o artigo propõe dois "reparos canônicos" que identificam o refinamento mais grosseiro possível de estados que preserva o comportamento desejado enquanto respeita os pontos finais visíveis:

• Para Tempo Linear (Traços): A relação $E^U_{tr} = \equiv_U \cap \equiv_{tr}$ é a maior relação de equivalência que respeita os pontos finais e preserva traços finitos. Ela identifica exatamente aquelas ocorrências equivalentes por ponto final cujos futuros são indistinguíveis como traços de rótulos de regras.
• Para Tempo de Ramificação (Quocientes Exatos): A relação $\approx_U$, definida como a união de todas as bisimulações fortes que respeitam o ponto final, é a maior bisimulação forte que respeita o ponto final. O sistema quociente $T / \approx_U$ é o quociente de ramificação exato maximamente grosseiro.
  • Propriedade Universal: Todo outro quociente de ponto final exato refina este quociente canônico. Assim, $\approx_U$ representa a quantidade máxima de proveniência que pode ser esquecida mantendo uma semântica de ramificação exata.

4. Computação Algorítmica
Para sistemas finitos, o artigo descreve um procedimento de refinamento de partição terminável para computar $\approx_U$. O algoritmo inicializa com a partição das classes de equivalência de ponto final e a refina iterativamente com base nas "assinaturas" dos blocos sucessores (os conjuntos de blocos alcançáveis para cada rótulo). O procedimento estabiliza na partição correspondente a $\approx_U$.

5. Aplicação à Geração Recursiva-Recombinante Aninhada (NRRG)
O artigo aplica estes resultados a um framework específico de NRRG decorado com proveniência. Apresenta um testemunho onde duas ocorrências ($e_G$ e $e_H$) compartilham o mesmo ponto final de grafo visível ($I \to A \to B$), mas diferem em sua ancestralidade recombinante.

• Em $e_G$, a ancestralidade permite uma regra de reescrita de toque de fronteira ($R_B$).
• Em $e_H$, a ancestralidade proíbe $R_B$.
• Resultado: O algoritmo de refinamento de partição separa $e_G$ e $e_H$ na primeira rodada, porque seus conjuntos de sucessores habilitados diferem. Isso demonstra que o isomorfismo de ponto final não implica equivalência comportamental, mesmo no nível de habilitação, e que o procedimento de refinamento proposto identifica corretamente a distinção necessária.

Significância e Alegações
O artigo afirma substituir a demanda de "tudo ou nada" de reter toda a proveniência ou descartá-la inteiramente por um critério exato para o esquecimento lícito.

• Resíduo Operacional: A diferença entre as classes de ponto final brutas e as classes refinadas ($\approx_U$ ou $E^U_{tr}$) constitui o "resíduo operacional" da proveniência — informação histórica que permanece ativa no espaço de transição futura.
• Exatidão da Abstração: O trabalho reformula o problema da abstração não apenas como soundess (sobre-aproximação), mas como exatidão para uma semântica escolhida. Um quociente bruto que funde estados sem verificar a bisimulação pode criar comportamentos (inflação) que não são lícitos para ocorrências específicas.
• Agnosticismo de Domínio: Os resultados são apresentados como critérios formais aplicáveis a qualquer sistema onde a admissibilidade dependa da linhagem (ex: estados de software, instrumentos legais, reivindicações científicas), desde que o sistema possa ser modelado como um sistema de transição rotulada com uma projeção de ponto final.

O artigo conclui que a proveniência pode ser apagada exatamente através daquelas distinções de ocorrência que não alteram a semântica futura lícita escolhida. O que resta após o apagamento seguro máximo não é uma decoração histórica, mas o verdadeiro estado generativo.