Resumo Técnico: Teoria da Aproximação para o Cálculo Bang Distante

1. Enunciado do Problema

A teoria da aproximação serve como uma abordagem central para a semântica do $\lambda$-cálculo, caracterizando o comportamento de programas por meio de meios finitos ou infinitários. Embora bem estabelecida para Call-by-Name (CbN) via Árvores de Böhm e Expansão de Taylor, o cenário de Call-by-Value (CbV) historicamente ficou atrás. Desenvolvimentos recentes em árvores de Böhm para CbV (ex: Kerinec [29, 28]) revelaram que a redução CbV padrão ( $\beta_v$ de Plotkin) é "fraca demais", frequentemente fazendo com que a redução fique travada quando os argumentos estão em forma normal, mas não são valores. Isso necessitou de frameworks alternativos, como o $\lambda\sigma_v$-cálculo com regras de permutação ($\sigma$-regras) ou cálculos baseados em distância (dCbV).

O Bang-calculus (Bang) foi proposto como um framework unificador que subsume tanto CbN quanto CbV via traduções de Lógica Linear. No entanto, o Bang-calculus padrão herda o problema do CbV de redexes malformados bloqueando a avaliação. Embora as $\sigma$-regras pudessem teoricamente resolver isso, elas falham em preservar a confluência no cenário do Bang. O distant Bang-calculus (dBang) [15] oferece uma solução ao utilizar substituições explícitas e reduções "distantes", garantindo confluência sem o uso de $\sigma$-regras.

Apesar do progresso no dBang em relação à confluência e significância [30, 9, 15], uma teoria da aproximação abrangente para o dBang permaneceu subdesenvolvida. Especificamente, não havia um framework unificado definindo árvores de aproximação do tipo Böhm e expansões de Taylor para o dBang, nem uma prova do Teorema de Comutação relacionando-os. Além disso, embora existam abordagens genéricas recentes (Mazza & Dufour [19]), elas carecem de uma noção direta de significância e não relacionam claramente de volta às noções específicas de solvabilidade/escrutabilidade de CbN e CbV.

2. Metodologia

Os autores desenvolvem uma teoria da aproximação unificada para o dBang integrando dois paradigmas centrais: Expansão de Taylor (semântica sensível a recursos) e Árvores de Aproximação (tradição de Böhm).

2.1 O Cálculo de Recursos ($\delta$Bang)

Os autores definem um cálculo de recursos $\delta$Bang como o alvo para a expansão de Taylor. Este cálculo substitui exponenciais ($!M$) por multiconjuntos (bags) finitos de termos de recurso.

• Relação de Aproximação ($\triangleleft!$): Uma relação multilinear é definida entre termos de recurso e termos de dBang.
• Redução: A relação de redução $\Rightarrow_\delta$ é não-determinística devido a permutações de bags, mas é fortemente normalizante devido à linearidade.
• Taylor Normal Form (TNF): Definida como o conjunto de formas normais completas de todos os aproximantes de recurso de um termo.

2.2 Árvores de Aproximação

Os autores definem Árvores de Aproximação para o dBang estendendo o cálculo com um símbolo $\bot$ representando computação indefinida.

• Aproximantes: Uma gramática de termos contendo $\bot$ é definida, representando formas normais potencialmente contendo subtermos indefinidos.
• Conclusão Ideal: O conjunto de aproximantes para um termo $M$, denotado $A(M)$, forma um ideal sob uma preordenação contextual $\sqsubseteq$. A árvore de aproximação $AT!(M)$ é o supremo deste ideal, representando o limite do comportamento do termo.
• Distinção: Diferente das árvores de Böhm clássicas de CbN que restringem os aproximantes a formas normais de cabeça, os autores adotam uma definição mais ampla (semelhante às árvores de Lévy-Longo em CbN e árvores de Böhm CbV em CbV) para acomodar a semântica específica do dBang e suas imersões.

2.3 Traduções

Para validar o framework, os autores utilizam traduções existentes de distant Call-by-Name (dCbN) e distant Call-by-Value (dCbV) para o dBang. Eles provam que estas traduções preservam passos de redução e a significância, permitindo que resultados derivados no dBang sejam projetados de volta para dCbN e dCbV.

3. Contribuições Principais e Resultados

3.1 Simulação e Comutação

O artigo estabelece um elo rigoroso entre a redução operacional do dBang e suas aproximações:

• Teorema de Simulação (Teorema 21): A expansão de Taylor de um termo de dBang simula sua redução. Especificamente, se $M \to! N$, então o conjunto de expansões de Taylor $T(M)$ reduz-se a $T(N)$ via redução de recurso paralela.
• Teorema de Comutação (Teorema 46): Este é o resultado central. Ele afirma que a expansão de Taylor da árvore de aproximação de um termo é igual à Taylor normal form do próprio termo:
  $$T(AT!(M)) = TNF(M)$$
  Isso confirma que a semântica infinitária (árvores) e a semântica sensível a recursos (expansão de Taylor) são consistentes dentro do framework dBang.

3.2 Recuperação dos Casos CbN e CbV

Ao traduzir dCbN e dCbV para o dBang, os autores recuperam as teorias de aproximação para esses cálculos específicos:

• Teorema 59: A árvore de aproximação de um termo traduzido no dBang corresponde exatamente à tradução da árvore de aproximação no cálculo de origem.
• Teorema 60: O Teorema de Comutação mantém-se para ambos, dCbN e dCbV, como uma consequência direta do resultado do dBang.

3.3 Significância e Expansão de Taylor

O artigo investiga a relação entre significância (a capacidade de um termo reduzir a um valor sob um contexto de teste) e a não-vacuidade da Taylor normal form.

• Teorema 61: Se um termo de dBang é significativo, sua Taylor normal form é não-vazia ($TNF(M) \neq \emptyset$).
• O Reverso: O inverso não se sustenta para o cálculo generalizado de dBang; existem termos sem significado com Taylor normal forms não-vazias (ex: termos envolvendo "clashes" como $xx$).
• Fragmentos: No entanto, para os fragmentos específicos correspondentes a dCbN ($dBang_N$) e dCbV ($dBang_V$), a equivalência é restaurada:
  • Corolário 68 (dCbN): $M$ é significativo se, e somente se, $TNF(M) \neq \emptyset$.
  • Corolário 73 (dCbV): $M$ é significativo se, e somente se, $TNF(M) \neq \emptyset$.

4. Significância e Alegações

O artigo alega fornecer um framework unificador para a teoria da aproximação que captura tanto a semântica infinitária quanto a semântica sensível a recursos para CbN e CbV dentro de um único sistema (dBang).

• Unificação: Demonstra que os desenvolvimentos distintos para CbN e CbV podem ser subsumidos pelo cálculo dBang, resolvendo a necessidade histórica de teorias semânticas separadas.
• Robustez: Ao utilizar a variante distante (dBang), os autores evitam os problemas de confluência associados às $\sigma$-regras no cálculo Bang padrão, fornecendo um ambiente mais limpo para a teoria da aproximação.
• Ponte Semântica: O Teorema de Comutação estabelece uma ponte profunda entre a semântica infinitária baseada em "forma" (Árvores de Aproximação) e a semântica diferencial baseada em "recursos" (Expansão de Taylor) em um ambiente unificado.
• Caracterização da Significância: O trabalho fornece uma caracterização sintática da significância para dCbN e dCbV via Taylor normal forms não-vazias, estendendo resultados conhecidos do CbN/CbV padrão para suas variantes distantes.

Os autores observam modestamente que, embora a equivalência entre significância e Taylor normal forms não-vazias se aplique aos fragmentos traduzidos, permanece uma questão em aberto se um fragmento maior e genérico de dBang (além das traduções) pode ser caracterizado de forma semelhante. Eles também sugerem trabalhos futuros estendendo estas noções para estruturas de prova, baseando-se no trabalho de Mazza e Dufour.