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

Resumen Técnico: Juegos, Procesos Móviles y Funciones

Enunciado del Problema
El artículo aborda la falta de una correspondencia formal y estrecha entre dos marcos semánticos prominentes para lenguajes de orden superior: la Semántica de Juegos Operacional (OGS) y el cálculo $\pi$ (específicamente el Cálculo $\pi$ Interno, $I\pi$). Aunque ambos modelos se utilizan para caracterizar el comportamiento de términos del cálculo $\lambda$, difieren significativamente en su construcción. OGS proporciona modelos intensionales donde las denotaciones de los programas se derivan composicionalmente a partir de configuraciones que representan interacciones con un entorno, enfatizando a menudo propiedades como la alternancia y el buen acoplamiento (well-bracketing). En contraste, el cálculo $\pi$ modela las funciones como procesos mediante las codificaciones de Milner, aprovechando estructuras algebraicas y equivalencias de procesos como la bisimilitud. Los autores buscan establecer una correspondencia operacional precisa entre estos modelos para el cálculo $\lambda$ no tipado de llamada por valor ($\Lambda_V$) y de llamada por nombre, demostrando que inducen las mismas equivalencias comportamentales y que las técnicas de uno pueden transferirse al otro.

Metodología
Los autores emplean un análisis comparativo de la semántica operacional de $\Lambda_V$ bajo tres variantes distintas de OGS y dos variantes de $I\pi$:

1. Variantes de OGS:
   • OGS Alternante (A-OGS): Impone una alternancia estricta entre el programa (Jugador) y el entorno (Oponente).
   • OGS Concurrente (C-OGS): Permite que múltiples términos se ejecuten en paralelo dentro de una configuración.
   • OGS de Buen Acoplamiento (WB-OGS): Impone una disciplina de pila en las continuaciones, restringiendo al Oponente a responder en orden último en entrar, primero en salir.
2. Variantes de $I\pi$:
   • Sistema de Transiciones Etiquetadas (LTS) Estándar de $I\pi$: El sistema de transiciones etiquetadas estándar para el Cálculo $\pi$ Interno.
   • LTS de $I\pi$ con Prioridad de Salida (opLTS): Un LTS restringido donde las acciones de entrada son visibles solo si no hay ninguna acción de salida o interna pendiente, imponiendo restricciones de secuencialidad.

La metodología central implica definir una aplicación ($\mathcal{V}$) desde las configuraciones de OGS (incluyendo entornos y términos en ejecución) hacia procesos de $I\pi$. Esta aplicación extiende la codificación de términos $\lambda$ de Milner. Los autores demuestran luego teoremas de correspondencia operacional que muestran que las transiciones en OGS corresponden a transiciones en $I\pi$ (y viceversa) bajo condiciones específicas. Crucialmente, utilizan técnicas "up-to" (específicamente up-to context y up-to composition) importadas de $I\pi$ para simplificar las pruebas de bisimilitud en OGS. También introducen un producto tensorial para configuraciones de OGS para modelar el entrelazamiento de trazas, análogo a la composición paralela en los cálculos de procesos.

Contribuciones Clave

1. Correspondencia Operacional: El artículo establece correspondencias operacionales estrechas entre:

   • A-OGS y $I\pi$ bajo el LTS con prioridad de salida (opLTS).
   • C-OGS y $I\pi$ bajo el LTS estándar.
     Estas correspondencias se mantienen tanto para transiciones fuertes como débiles, utilizando la relación de expansión ($\lesssim$) para dar cuenta de las reducciones internas.

2. Coincidencia de Equivalencias: Los autores demuestran que las equivalencias comportamentales inducidas en los términos $\lambda$ por todos estos modelos coinciden. Específicamente:

   • La equivalencia de trazas y la bisimilitud en A-OGS, C-OGS y $I\pi$ (tanto estándar como opLTS) definen todas la misma relación sobre los términos de $\Lambda_V$.
   • Esta equivalencia inducida se identifica como la bisimilitud de forma normal ansiosa de Lassen (a menudo visualizada como los árboles de Lassen).
   • Para trazas completas (trazas que describen interacciones que terminan), la semántica de OGS Alternante, Concurrente y de Buen Acoplamiento también coincide.

3. Transferencia de Técnicas:

   • Up-to Composition: Los autores importan las técnicas "up-to context" y "expansion" de $I\pi$ a OGS. Definen una técnica novedosa llamada "up-to composition" para OGS, que permite dividir una configuración compleja en componentes elementales (configuraciones singleton) en las pruebas de bisimilitud y razonar sobre ellas de forma independiente.
   • Congruencia y Composicionalidad: Al aprovechar la correspondencia con $I\pi$, el artículo deriva propiedades de congruencia para OGS (por ejemplo, si $M \sim N$, entonces $C[M] \sim C[N]$) y define un producto tensorial para configuraciones que calcula los entrelazamientos de trazas.

4. Abstracción Completa para Almacén: El estudio de las trazas completas en la OGS de Buen Acoplamiento se vincula con la equivalencia contextual para el cálculo $\lambda$ con almacén mutable. El artículo muestra que la codificación de términos $\lambda$ en $I\pi$ produce un resultado de abstracción completa con respecto a contextos escritos en un cálculo $\lambda$ extendido con un almacén.

5. Extensión a Llamada por Nombre: El artículo esboza una correspondencia similar para el cálculo $\lambda$ no tipado de llamada por nombre, mostrando que la equivalencia inducida coincide con los Árboles de Lévy-Longo.

Resultados

• Teoremas 6.7 y 7.3: Establecen la correspondencia operacional entre configuraciones de OGS y procesos de $I\pi$ bajo los respectivos LTS.
• Corolarios 6.12 y 7.7: Demuestran que la equivalencia de trazas y la bisimilitud en A-OGS, C-OGS y $I\pi$ son idénticas para los términos $\lambda$.
• Teorema 8.1: Demuestra directamente que la bisimilitud de C-OGS coincide con la bisimilitud de forma normal ansiosa de Lassen utilizando la técnica "up-to composition".
• Teorema 12.2: Demuestra que la equivalencia de trazas completas es idéntica entre WB-OGS, A-OGS y C-OGS.
• Lema 7.16 y Teorema 7.17: Demuestran la solidez de la "bisimilitud up-to reducción y composición" para C-OGS, importada de $I\pi$.

Significado
El artículo afirma que su principal significado radica en establecer una "correspondencia estrecha y precisa" entre OGS y el cálculo $\pi$. Esta conexión permite la transferencia de resultados y técnicas entre los dos modelos. Específicamente:

• Permite que OGS se beneficie de la rica estructura algebraica y las poderosas técnicas de prueba (como las técnicas up-to) del cálculo $\pi$, que a menudo son difíciles de desarrollar directamente dentro del marco teórico de juegos.
• Permite que el cálculo $\pi$ se beneficie de la proximidad de OGS al lenguaje fuente y de su flexibilidad para modelar efectos computacionales específicos (como operadores de control o almacén).
• Proporciona una visión unificada de la semántica del cálculo $\lambda$, mostrando que las condiciones del "Cubo Semántico" (alternancia, buen acoplamiento) en OGS y las restricciones de secuencialidad en $I\pi$ (vía opLTS) son dos caras de la misma moneda, ambas caracterizando la misma equivalencia comportamental subyacente (los árboles de Lassen para llamada por valor).

Los autores señalan que, aunque las analogías entre la semántica de juegos y los cálculos de procesos han sido exploradas previamente (por ejemplo, traduciendo estrategias a procesos), este trabajo es distinto en su comparación directa de la interpretación de funciones y en su transferencia sistemática de técnicas de prueba para derivar nuevos resultados para OGS.