Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics

Resumo Técnico: Jogos, Processos Móveis e Funções

Enunciado do Problema
O artigo aborda a falta de uma correspondência formal e rigorosa entre dois quadros semânticos proeminentes para linguagens de ordem superior: Semântica de Jogos Operacional (OGS) e o cálculo $\pi$ (especificamente o Cálculo $\pi$ Interno, $I\pi$). Embora ambos os modelos sejam utilizados para caracterizar o comportamento de termos do $\lambda$-cálculo, eles diferem significativamente em sua construção. A OGS fornece modelos intensionais onde as denotações de programas são derivadas composicionalmente a partir de configurações que representam interações com um ambiente, enfatizando frequentemente propriedades como alternância e correta estruturação de parênteses (well-bracketing). Em contraste, o cálculo $\pi$ modela funções como processos por meio das codificações de Milner, aproveitando estruturas algébricas e equivalências de processos como a bisimilaridade. Os autores visam estabelecer uma correspondência operacional precisa entre esses modelos para o $\lambda$-cálculo não tipado por chamada por valor ($\Lambda_V$) e por chamada por nome, demonstrando que eles induzem as mesmas equivalências comportamentais e que técnicas de um podem ser transferidas para o outro.

Metodologia
Os autores empregam uma análise comparativa da semântica operacional de $\Lambda_V$ sob três variantes distintas de OGS e duas variantes de $I\pi$:

1. Variantes de OGS:
   • OGS Alternante (A-OGS): Impõe alternância estrita entre o programa (Jogador) e o ambiente (Oponente).
   • OGS Concorrente (C-OGS): Permite que múltiplos termos sejam executados em paralelo dentro de uma configuração.
   • OGS de Estrutura Correta (WB-OGS): Impõe uma disciplina de pilha em continuação, restringindo o Oponente a responder em ordem último-a-sair-primeiro-a-entrar.
2. Variantes de $I\pi$:
   • Sistema de Transição Rotulada (LTS) Padrão de $I\pi$: O sistema de transição rotulada padrão para o Cálculo $\pi$ Interno.
   • LTS de $I\pi$ com Prioridade de Saída (opLTS): Um LTS restrito onde ações de entrada são visíveis apenas se nenhuma ação de saída ou interna estiver pendente, impondo restrições de sequencialidade.

A metodologia central envolve definir uma mapeamento ($\mathcal{V}$) de configurações de OGS (incluindo ambientes e termos em execução) para processos de $I\pi$. Este mapeamento estende a codificação de Milner de termos $\lambda$. Os autores então provam teoremas de correspondência operacional mostrando que transições em OGS correspondem a transições em $I\pi$ (e vice-versa) sob condições específicas. Crucialmente, eles utilizam técnicas "até" (up-to) (especificamente até contexto e até composição) importadas de $I\pi$ para simplificar provas de bisimilaridade em OGS. Eles também introduzem um produto tensorial para configurações de OGS para modelar o entrelaçamento de traços, análogo à composição paralela em cálculos de processos.

Principais Contribuições

1. Correspondência Operacional: O artigo estabelece correspondências operacionais rigorosas entre:

   • A-OGS e $I\pi$ sob o LTS com prioridade de saída (opLTS).
   • C-OGS e $I\pi$ sob o LTS padrão.
     Essas correspondências valem tanto para transições fortes quanto fracas, utilizando a relação de expansão ($\lesssim$) para contabilizar reduções internas.

2. Coincidência de Equivalências: Os autores provam que as equivalências comportamentais induzidas em termos $\lambda$ por todos esses modelos coincidem. Especificamente:

   • A equivalência de traços e a bisimilaridade em A-OGS, C-OGS e $I\pi$ (tanto padrão quanto opLTS) definem todas a mesma relação sobre termos de $\Lambda_V$.
   • Essa equivalência induzida é identificada como a bisimilaridade de forma normal ansiosa de Lassen (frequentemente visualizada como árvores de Lassen).
   • Para traços completos (traços descrevendo interações terminais), a semântica de OGS Alternante, Concorrente e de Estrutura Correta também coincide.

3. Transferência de Técnicas:

   • Até Composição: Os autores importam as técnicas "até contexto" e "expansão" de $I\pi$ para OGS. Eles definem uma técnica novel chamada "até composição" para OGS, que permite que provas de bisimilaridade dividam uma configuração complexa em componentes elementares (configurações unitárias) e raciocinem sobre elas independentemente.
   • Congruência e Composicionalidade: Ao aproveitar a correspondência com $I\pi$, o artigo deriva propriedades de congruência para OGS (por exemplo, se $M \sim N$, então $C[M] \sim C[N]$) e define um produto tensorial para configurações que calcula entrelaçamentos de traços.

4. Abstração Total para Armazenamento: O estudo de traços completos na OGS de Estrutura Correta está ligado à equivalência contextual para $\lambda$-cálculos com armazenamento mutável. O artigo mostra que a codificação de termos $\lambda$ em $I\pi$ produz um resultado de abstração total em relação a contextos escritos em um $\lambda$-cálculo estendido com armazenamento.

5. Extensão para Chamada por Nome: O artigo esboça uma correspondência similar para o $\lambda$-cálculo não tipado por chamada por nome, mostrando que a equivalência induzida coincide com as Árvores de Lévy-Longo.

Resultados

• Teorema 6.7 & 7.3: Estabelecem a correspondência operacional entre configurações de OGS e processos de $I\pi$ sob os respectivos LTSs.
• Corolário 6.12 & 7.7: Demonstram que a equivalência de traços e a bisimilaridade em A-OGS, C-OGS e $I\pi$ são idênticas para termos $\lambda$.
• Teorema 8.1: Prova diretamente que a bisimilaridade de C-OGS coincide com a bisimilaridade de forma normal ansiosa de Lassen usando a técnica "até composição".
• Teorema 12.2: Prova que a equivalência de traços completos é idêntica entre WB-OGS, A-OGS e C-OGS.
• Lema 7.16 & Teorema 7.17: Provam a correção da "bisimilaridade até redução e composição" para C-OGS, importada de $I\pi$.

Significado
O artigo afirma que sua principal significância reside em estabelecer uma "correspondência rigorosa e precisa" entre OGS e o cálculo $\pi$. Esta conexão permite a transferência de resultados e técnicas entre os dois modelos. Especificamente:

• Permite que a OGS beneficie-se da rica estrutura algébrica e de técnicas de prova poderosas (como técnicas "até") do cálculo $\pi$, que são frequentemente difíceis de desenvolver diretamente dentro do quadro teórico-jogo.
• Permite que o cálculo $\pi$ beneficie-se da proximidade da OGS com a linguagem fonte e sua flexibilidade em modelar efeitos computacionais específicos (como operadores de controle ou armazenamento).
• Proporciona uma visão unificada da semântica do $\lambda$-cálculo, mostrando que as condições do "Cubo Semântico" (alternância, estrutura correta) na OGS e as restrições de sequencialidade em $I\pi$ (via opLTS) são dois lados da mesma moeda, ambos caracterizando a mesma equivalência comportamental subjacente (árvores de Lassen para chamada por valor).

Os autores observam que, embora analogias entre semântica de jogos e cálculos de processos tenham sido exploradas anteriormente (por exemplo, traduzindo estratégias para processos), este trabalho distingue-se pela comparação direta da interpretação de funções e pela sua transferência sistemática de técnicas de prova para derivar novos resultados para a OGS.