When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions

Título: Quando a Igualdade Falha como Princípio de Reescrita: Proveniência e Definibilidade para Expressões com Medições

1. O Problema

O artigo aborda uma limitação fundamental na aplicação de igualdade algébrica padrão como princípio de reescrita (simplificação) para expressões que carregam medições (dados experimentais com incerteza). A igualdade algébrica tradicional falha em dois modos principais quando aplicada a este contexto:

1. Falha de Proveniência (Provenance):

   • Em expressões matemáticas puras, $x - x = 0$ é sempre válido. Em medições, se $x$ representa uma única observação (um "token" de medição), a subtração é válida. No entanto, se houver duas medições independentes ($x_1$ e $x_2$) com os mesmos valores e intervalos de incerteza, $x_1 - x_2$ não é necessariamente zero, pois os valores exatos subjacentes podem diferir.
   • Sistemas formais tradicionais (como análise dimensional ou aritmética intervalar clássica) são "cegos à proveniência": não conseguem distinguir entre o reuso do mesmo token de medição e o uso de duas medições distintas, levando a simplificações inseguras.

2. Falha de Definibilidade (Definedness):

   • A divisão introduz singularidades (divisão por zero). Expressões algebricamente equivalentes podem ter domínios de definição diferentes.
   • Exemplo: A expressão $x/x$ é igual a $1$ onde definida, mas possui uma singularidade em $x=0$, enquanto a constante $1$ é definida em todo lugar. Simplificar $1$ para $x/x$ introduz uma singularidade perigosa.
   • A direção da simplificação importa: remover uma singularidade é seguro, mas introduzi-la não é. Além disso, duas expressões podem ser "a mesma função" em seus domínios comuns, mas ter estruturas de singularidade incomparáveis, bloqueando a substituição em qualquer direção.

O objetivo do trabalho é desenvolver um framework unificado que trate simultaneamente a proveniência (identidade do token de medição) e a definibilidade (domínios onde a expressão é cientificamente válida) para classificar quando uma reescrita é segura.

2. Metodologia

Os autores desenvolveram uma semântica formal unificada implementada e verificada no assistente de prova Lean 4. A metodologia baseia-se em três camadas conceituais:

• Semântica de Enclosure Sensível a Tokens (Token-Sensitive Enclosure Semantics):

  • As expressões são avaliadas em relação a um ambiente de tokens ($\sigma$), onde cada token de medição mapeia para um valor racional exato dentro de um intervalo.
  • A Enclosure Garantida (Warranted Enclosure) de uma expressão é o conjunto de todos os valores possíveis resultantes de todos os ambientes consistentes com os tokens. Isso captura a dependência: se o mesmo token aparece duas vezes, ele deve ter o mesmo valor em ambas as ocorrências.
  • A semântica ignora, inicialmente, se a divisão por zero ocorre (usando a convenção totalizada do Lean, onde $x/0 = 0$), focando apenas na proveniência.

• Refinamento de Domínios Admissíveis (Admissible Domains):

  • Para lidar com a definibilidade, define-se um predicado AdmDom (Domínio Admissível), que restringe a avaliação apenas aos ambientes onde todas as divisões têm denominadores não nulos.
  • Introduz-se a Enclosure Definida (Defined Enclosure), que é o conjunto de valores gerados apenas dentro do domínio admissível.

• Julgamentos de Reescrita:

  • O paper define julgamentos de reescrita em três níveis:
    1. Baseado em Enclosure: Foca apenas na proveniência (ex: $e \rightsquigarrow e'$ se a enclosure de $e'$ está contida na de $e$).
    2. Consciente de Domínio (Domain-Aware): Exige que o domínio admissível do alvo contenha o do original e que os valores sejam consistentes. Isso torna a reescrita direcional (não simétrica).
    3. Relativo a Suporte (Support-Relative): Permite que reescritas sejam válidas em subconjuntos específicos de ambientes (útil para casos positivos como intervalos estritamente positivos).

3. Principais Contribuições

1. Semântica Unificada: Uma estrutura que integra proveniência e definibilidade, mostrando que são eixos ortogonais e ambos necessários.
2. Julgamentos de Reescrita Direcionais: A introdução de julgamentos como DomainSafeRewrite ($e \rightsquigarrow_d e'$), que impõem restrições de domínio. Diferente da igualdade algébrica, a reescrita segura não é transitiva e depende da direção (remover singularidades é seguro; adicionar não é).
3. Teoremas de Redução e Recuperação:
   • Mostram que, em fragmentos onde todas as expressões são universalmente admissíveis (sem divisões problemáticas), a teoria unificada colapsa para a teoria baseada apenas em proveniência.
   • Recuperam casos clássicos de simplificação (como cancelamento de tokens iguais e subtração de fundo compartilhado) como teoremas contextuais dentro do framework unificado.
4. Resultados de Rigor (Strictness Results):
   • Demonstram que a presença de singularidades alcançáveis torna a simplificação estritamente unidirecional.
   • Provam que a igualdade de domínio comum (onde ambas as expressões são definidas) é insuficiente para garantir substituição segura se as estruturas de singularidade forem incomparáveis.
5. Teorema de Insuficiência:
   • Um resultado negativo crucial: apagar a identidade dos tokens (tornando a semântica cega à proveniência) colapsa distinções que a definibilidade sozinha não consegue recuperar, e vice-versa. Nenhuma das duas dimensões isoladamente é suficiente para uma classificação segura de reescrita.
6. Formalização Completa em Lean 4:
   • Todo o trabalho (143 teoremas e 45 definições em ~2.700 linhas de código) foi formalizado sem o uso de sorry (sem lacunas de prova), garantindo a correção mecânica dos resultados.

4. Resultados Chave e Exemplos

• Cancelamento de Tokens:
  • $Meas(t, I) - Meas(t, I) \Leftrightarrow 0$ (Reescrita segura e bidirecional, pois o mesmo token garante o mesmo valor).
  • $Meas(t_1, I) - Meas(t_2, I) \to 0$ (Reescrita apenas unidirecional ou inválida, pois $t_1$ e $t_2$ podem ter valores diferentes).
• Subtração de Fundo (Background Subtraction):
  • $(s + b) - b \Leftrightarrow s$ é válido apenas se o token de fundo $b$ for reutilizado. Se forem duas medições de fundo distintas, a simplificação é insegura.
• Divisão por Si Mesmo (Self-Division):
  • Se o intervalo é estritamente positivo ($0 < I.lo$),$x/x \Leftrightarrow 1$ é seguro.
  • Se o intervalo inclui zero ($I = [0, 1]$), $x/x \to 1$ é seguro (remove singularidade), mas $1 \to x/x$ é inseguro (introduz singularidade).
• Não-Colapso (Non-Collapse):
  • Existem pares de expressões que são iguais em seus domínios comuns, mas onde nenhum pode substituir o outro porque seus domínios admissíveis são incomparáveis (um é definido onde o outro não é, e vice-versa).

5. Significado e Impacto

O artigo demonstra que a igualdade algébrica padrão é um princípio de reescrita falho para expressões de medição. Para que um simplificador simbólico ou um sistema de verificação seja seguro em contextos científicos (como análise de dados experimentais), ele deve:

1. Rastrear a proveniência (identidade da observação) para evitar a suposição falsa de independência entre medições repetidas.
2. Rastrear a definibilidade para evitar a introdução acidental de singularidades (divisão por zero) durante a simplificação.

A conclusão central é que nenhuma semântica baseada apenas em valores, apenas em proveniência ou apenas em acordo de domínio comum é suficiente. A combinação de ambos é necessária. O trabalho fornece a base teórica e formal (verificada mecanicamente) para construir futuros otimizadores de código científico e sistemas de álgebra computacional que lidem corretamente com incertezas e dados parciais.

O estudo também destaca que a reescrita segura não é transitiva: uma cadeia de simplificações localmente seguras pode falhar globalmente se não for re-verificada passo a passo em relação aos domínios atuais.