Well-Scoped Locally Nameless Representation of Syntax

Resumen Técnico: Representación Localmente Nombrada con Ámbito Bien Definido de la Sintaxis

Enunciado del Problema
Al formalizar lenguajes con construcciones de enlace (por ejemplo, el cálculo $\lambda$, sistemas de tipos) en demostradores de teoremas interactivos basados en teoría de tipos dependiente (como Agda, Lean o Rocq), un desafío central es gestionar el enlace de variables y la equivalencia $\alpha$. El enfoque "localmente nombrado", que representa las variables libres como nombres explícitos y las variables ligadas como índices de de Bruijn, ha demostrado satisfacer los criterios PoplMark en cuanto a bajo sobrecosto de infraestructura, transparencia y facilidad de entrada. Sin embargo, las representaciones localmente nombradas estándar adolecen de un defecto crítico: la definición inductiva de términos permite índices "colgantes" (índices que exceden el ámbito actual). Para garantizar la corrección, es necesario restringir el dominio a un subconjunto de términos "localmente cerrados". Esto exige pruebas manuales y repetitivas de que las operaciones (como la sustitución) preservan el cierre local, generando una carga significativa y una fuente de errores potenciales en desarrollos formales.

Metodología
El artículo propone una variante "con ámbito bien definido" de la representación localmente nombrada que aprovecha el sistema de tipos dependiente de Agda para imponer el cierre local intrínsecamente, en lugar de como un predicado separado.

1. Tipos Inductivos Indexados: En lugar de un único tipo de términos, la biblioteca define una familia de tipos Trm[n] indexada por un número natural $n$. Un "término-$n$" es un término donde todos los índices de de Bruijn se extraen del tipo finito Fin n (números naturales menores que $n$).
2. Términos Localmente Cerrados como Términos-0: En este marco, los términos "localmente cerrados" (aquellos sin índices colgantes) corresponden exactamente a Trm[0]. Los términos con variables libres se representan como Trm[n], donde $n$ corresponde al número de variables libres en el ámbito.
3. Parametrización por Firmas de Enlace: La biblioteca es genérica, parametrizada por una firma de enlace al estilo de Plotkin. Esto permite definir operadores, sus aridades y el número de nombres ligados en cada posición de argumento.
4. Operaciones mediante Tipos Dependientes:
   • Debilitación de Ámbito: Una función Trm[m] -> Trm[n] (para $m \le n$) que inyecta índices, manejando el desplazamiento requerido al moverse a un ámbito más amplio.
   • Concreción (Apertura): Reemplazar un índice $i$ en un término de (1+n) con un término-0 para producir un término-$n$. Esto implica desplazar los índices mayores que $i$ hacia abajo en una unidad.
   • Abstracción (Cierre): Reemplazar un nombre libre en un término-$n$ con un índice para producir un término de (1+n). Esto implica desplazar los índices hacia arriba.
   • Sustitución: Definida estructuralmente. Dado que la función de sustitución mapea nombres a términos-0 (Trm), la condición de "localmente cerrado" es impuesta automáticamente por el sistema de tipos. La sustitución en un término-$n$ produce otro término-$n$.

Contribuciones Clave

• La Biblioteca WSLN: Una biblioteca genérica en Agda que implementa términos localmente nombrados con ámbito bien definido. Proporciona la infraestructura para definir sintaxis, operaciones (debilitamiento, sustitución, abstracción, concreción) y principios de razonamiento para cualquier lenguaje especificado por una firma de enlace de Plotkin.
• Prueba de Adecuación Formal: El artículo proporciona una prueba rigurosa que establece una biyección entre:
  1. El tipo de términos localmente nombrados con ámbito bien definido y de tipo 0 (Trm[0]).
  2. Las clases de equivalencia $\alpha$ de términos "con nombres" (términos con nombres explícitos tanto para variables libres como ligadas).
     Esta biyección demuestra que la representación con ámbito bien definido captura correctamente la semántica de la sustitución que evita la captura y la equivalencia $\alpha$.
• Eliminación de Pruebas de Cierre Local: Al codificar las restricciones de ámbito en los índices de los tipos, se elimina la necesidad de predicados explícitos de "cierre local" y las obligaciones de prueba asociadas (por ejemplo, probar que la sustitución preserva el cierre local). Estas propiedades se convierten en consecuencias de las reglas de tipado.
• Manejo de Frescura: La biblioteca se integra con técnicas nominales, utilizando un conjunto de átomos "finitamente inexhaustible" (números naturales) para generar nombres frescos mediante cuantificación cofinita, asegurando que las condiciones de frescura se manejen sistemáticamente.

Resultados
El artículo valida el enfoque mediante tres ejemplos distintos implementados en Agda:

1. Cálculo $\pi$: Demuestra la aplicabilidad de la biblioteca más allá del cálculo $\lambda$, manejando expresiones de procesos y nombres de canales. Destaca que, aunque la biblioteca gestiona la estructura de enlace, la verificación de tipos para la corrección (por ejemplo, asegurar que los canales se utilizan donde se espera) sigue siendo un juicio separado definido por el usuario.
2. Teoría de Tipos de Martin-Löf (MLTT): Muestra cómo la biblioteca facilita la definición de reglas de tipado. Contrasta las reglas "existe-fresco" (que requieren suposiciones explícitas de frescura) con las reglas de "cuantificación cofinita" (donde la frescura es implícita), demostrando que la representación con ámbito bien definido apoya esta última, lo que conduce a formalizaciones más limpias y transparentes.
3. Sistema T de Gödel (Normalización por Evaluación): Un desarrollo sustancial que prueba la decidibilidad de la conversión $\beta\eta$. Este ejemplo ilustra cómo la representación con ámbito bien definido simplifica la semántica de la abstracción y el manejo de la frescura en construcciones semánticas complejas (presheaves con valores en setoides), evitando la necesidad de objetos semánticos con soporte finito.

Significado y Afirmaciones
El artículo afirma que la representación localmente nombrada con ámbito bien definido ofrece una solución "directa" pero poderosa a la "trampa" de los índices colgantes encontrada en los enfoques localmente nombrados tradicionales. Su principal significado radica en desplazar la carga de garantizar la corrección del ámbito del usuario (mediante pruebas manuales) al verificador de tipos del demostrador de teoremas (mediante tipos dependientes).

Los autores enfatizan que este enfoque mantiene la transparencia requerida por los criterios PoplMark: las definiciones formales reflejan estrechamente las convenciones informales, y el "yoga de índices" (manipulación de índices de de Bruijn) queda encapsulado dentro de las operaciones de la biblioteca. Si bien la implementación requiere un manejo cuidadoso de ordinales finitos (Fin n) y el desplazamiento de índices, la biblioteca parametriza esta complejidad, permitiendo a los usuarios definir lenguajes y probar propiedades sin gestionar la mecánica de bajo nivel del ámbito. El artículo nota modestamente que, si bien las firmas de enlace actuales no están ordenadas y modelan ámbitos de enlace simples, el enfoque es lo suficientemente robusto para manejar sistemas de tipos complejos y pruebas semánticas, como lo demuestra el desarrollo del Sistema T.