Sobre la Metateoría Formal de los Sistemas de Tipos Puros utilizando Nombres de Variables Unisortados y Sustituciones Múltiples

Información Básica

• ID del Artículo: 2510.12300
• Título: On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
• Autor: Sebastián Urciuoli (Universidad ORT Uruguay, Uruguay)
• Clasificación: cs.LO (Lógica en Ciencia de la Computación)
• Conferencia de Publicación: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
• Enlace del Artículo: https://arxiv.org/abs/2510.12300
• Enlace del Código: https://github.com/surciuoli/pts-metatheory

Resumen

Este artículo desarrolla una teoría formal de la conversión para términos λ de estilo Church con tipos Π, utilizando sintaxis de primer orden, nombres de variables unisortados y sustituciones múltiples de Stoughton. Posteriormente, formaliza los Sistemas de Tipos Puros (Pure Type Systems, PTS) y algunas propiedades metatéoricas fundamentales: debilitamiento, validez sintáctica, clausura bajo conversión α y sustitución. Finalmente, compara trabajos de formalización relacionados. Todo el desarrollo ha sido verificado mecánicamente utilizando el sistema Agda. El trabajo demuestra que la mecanización de la teoría de tipos dependientes utilizando sintaxis tradicional sin identificar términos λ convertibles por α es viable.

Contexto de Investigación y Motivación

Contexto del Problema

1. Desafíos de Formalización: La verificación mecánica de la teoría de tipos dependientes ha sido siempre un desafío, particularmente al tratar con ligaduras de variables y equivalencia α
2. Dilema de Elección Sintáctica: Los métodos existentes típicamente adoptan índices de de Bruijn o nombres de variables bisortados para evitar problemas de captura de nombres, pero estos métodos se distancian de las implementaciones reales
3. Complejidad de Operaciones de Sustitución: La definición tradicional de sustitución unaria es no estructuralmente recursiva, requiriendo métodos inductivos complejos en pruebas mecanizadas

Motivación de Investigación

1. Prueba de Escalabilidad: Verificar si el marco basado en la teoría de sustitución de Stoughton puede extenderse a lenguajes más complejos (como PTS)
2. Reducción de la Brecha Teoría-Práctica: Utilizar sintaxis tradicional de nombres de variables unisortados, más cercana a las implementaciones reales de verificadores de tipos
3. Simplificación de Métodos de Prueba: Mediante definiciones mejoradas de conversión α, permitir pruebas de lemas clave utilizando métodos de inducción estructural más simples

Contribuciones Principales

1. Extensión del Marco de Sustitución de Stoughton: Extensión del marco original del cálculo λ puro para soportar abstracciones λ de estilo Church y tipos Π
2. Definición Mejorada de Conversión α: Propuesta de una nueva definición de conversión α que permite que lemas clave se prueben mediante inducción estructural
3. Formalización de Metateoría de PTS: Verificación mecánica de propiedades metatéoricas fundamentales de PTS, incluyendo debilitamiento, validez sintáctica, clausura bajo conversión α y clausura bajo sustitución
4. Prueba de Equivalencia: Demostración de la equivalencia bidireccional entre sistemas de reglas infinitas utilizando inducción generalizada y sistemas de reglas finitas estándar
5. Implementación Completa en Agda: Provisión de verificación mecánica completa con aproximadamente 3000 líneas de código

Explicación Detallada del Método

Definición de Sintaxis

El artículo utiliza la definición sintáctica tradicional de primer orden para términos λ:

data Λ : Set where
  c : C → Λ                    -- constantes
  v : V → Λ                    -- variables  
  λ[_:_]_ : V → Λ → Λ → Λ      -- abstracción λ de estilo Church
  Π[_:_]_ : V → Λ → Λ → Λ      -- tipo Π
  _·_ : Λ → Λ → Λ              -- aplicación

Funciones de Selección y Sustitución

La innovación central radica en utilizar sustituciones múltiples de Stoughton, evitando captura de nombres mediante funciones de selección:

X : Res → V
X (σ, xs) = X' (concat (map (fv ∘ σ) xs))

La operación de sustitución se define como recursión estructural:

λ[ x : A ] M • σ = λ[ y : A • σ ](M • σ , x := v y) 
  where y = X (σ , fv M - x)

Definición Mejorada de Conversión α

La nueva definición de conversión α utiliza equivalencia sintáctica en lugar de definición recursiva:

∼λ : ∀ {x x' y A A' M M'} → A ∼α A' → y ∉ fv M - x → y ∉ fv M' - x'
   → M [ x := v y ] ≡ M' [ x' := v y ] → λ[ x : A ] M ∼α λ[ x' : A' ] M'

Sistema de Tipos PTS

Utiliza inducción generalizada para definir PTS, con reglas clave incluyendo:

⊢abs : Γ ⊢ A : s₁ → ∀z → z ∉ domΓ → Γ,z : A ⊢ B[y := z] : s₂
     → ∀z → z ∉ domΓ → Γ,z : A ⊢ M[x := z] : B[y := z]
     → R s₁ s₂ s₃
     → Γ ⊢ λ[x : A]M : Π[y : A]B

Puntos de Innovación Técnica

1. Redefinición de Tipos Restringidos

Redefinición de restricciones de Sub × Λ a Sub × List V, proporcionando mayor flexibilidad:

Res = Sub × List V

2. Prueba de Conversión α Estructurada

El lema clave iotaAlpha ahora puede probarse mediante inducción estructural:

iotaAlpha : ∀ {M M'} → M • ι ≡ M' • ι → M ∼α M'

3. Premisas Mejoradas en Regla de Aplicación

Adición de premisas de validez de tipos en la regla de aplicación, simplificando pruebas posteriores:

⊢app : Γ ⊢ M : Π[x : A]B → Γ ⊢ N : A → Γ ⊢ B[x := N] : s
     → Γ ⊢ M·N : B[x := N]

Configuración Experimental

Entorno de Formalización

• Asistente de Pruebas: Sistema Agda
• Escala de Código: Aproximadamente 3000 líneas de código
• División de Módulos: Marco y metateoría de PTS ocupan aproximadamente la mitad cada uno

Contenido de Verificación

1. Teoría Fundamental: Propiedades de operaciones de sustitución, equivalencia de conversión α
2. Metateoría de PTS: Debilitamiento, validez sintáctica, teoremas de clausura
3. Equivalencia: Equivalencia entre sistemas de reglas infinitas y sistemas de reglas finitas

Resultados Experimentales

Logros Principales

1. Mecanización Completa: Verificación mecánica exitosa de propiedades metatéoricas centrales de PTS
2. Simplificación de Pruebas: Todos los resultados (excepto completitud de conversión α) se prueban mediante inducción estructural
3. Eficiencia de Código: 3000 líneas de código implementan teoría completa, más conciso que otros trabajos

Teoremas Clave

• Lema 4.1 (Debilitamiento): thinning : ∀ {Γ Δ M A} → Γ ⊆ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M : A
• Lema 4.3 (Validez Sintáctica): syntacticValidity : ∀ {Γ M A} → Γ ⊢ M : A → ∃ λ s → A ≡ c s ⊎ Γ ⊢ A : c s
• Lema 4.4 (Clausura bajo Conversión α): closAlphaAsg : ∀ {Γ Δ M N A} → Γ ≈α Δ → M ∼α N → Γ ⊢ M : A → Δ ⊢ N : A
• Lema 4.6 (Clausura bajo Sustitución): closureSub : ∀ {Γ Δ M A σ} → σ : Γ ⇀ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M • σ : A • σ

Resultados de Equivalencia

• Teoremas 4.9-4.11: Demostración de equivalencia bidireccional entre sistemas de reglas infinitas y sistemas de reglas finitas estándar

Trabajo Relacionado

Comparación Principal

1. McKinna & Pollack: Utilizan nombres de variables bisortados, evitando conversión α pero requiriendo predicados de buena formación
2. Barras & Werner: Utilizan notación de de Bruijn, aproximadamente 2600 líneas de código para funcionalidad similar
3. Urban et al.: Utilizan Nominal Isabelle, aproximadamente 15K líneas de código, con 1800 líneas para metateoría
4. Desarrollos Modernos: Formalizaciones de teorías de tipos más grandes por Abel et al., Adjedj et al., Sozeau et al.

Análisis de Ventajas

• Directitud: La clausura de conversión β bajo sustitución puede probarse directamente mediante inducción estructural
• Concisión: Sin necesidad de pruebas de equivalencia adicionales o lemas de renombramiento
• Practicidad: Más cercano a la implementación de verificadores de tipos reales

Conclusiones y Discusión

Conclusiones Principales

1. Verificación de Viabilidad: Demostración de la viabilidad de mecanización de teoría de tipos dependientes utilizando sintaxis tradicional y nombres de variables unisortados
2. Ventajas del Método: El método de sustitución de Stoughton sigue siendo efectivo al tratar sistemas de tipos complejos
3. Contribución Teórica: La definición mejorada de conversión α simplifica pruebas clave

Limitaciones

1. Restricción de Escala: Actualmente solo trata metateoría fundamental de PTS, sin abordar propiedades más complejas como normalización fuerte
2. Consideraciones de Rendimiento: La complejidad computacional de sustituciones múltiples puede afectar aplicaciones prácticas
3. Extensibilidad: La extensión a sistemas de tipos más grandes (como aquellos con universos, grandes eliminaciones) aún requiere verificación

Direcciones Futuras

1. Extensión a Sistemas Más Complejos: Como sistemas con tipos inductivos, jerarquías de universos
2. Optimización de Rendimiento: Investigación de implementaciones eficientes de operaciones de sustitución
3. Aplicación Práctica: Aplicación de resultados teóricos a implementaciones de verificadores de tipos reales

Evaluación Profunda

Fortalezas

1. Innovación Teórica: La definición mejorada de conversión α es una contribución teórica importante, simplificando complejidad de pruebas
2. Valor Práctico: El uso de sintaxis tradicional reduce la brecha entre teoría y práctica
3. Completitud: Proporciona verificación mecánica completa de metateoría de PTS
4. Claridad: Escritura clara del artículo, descripción precisa de detalles técnicos
5. Reproducibilidad: Provisión de código Agda completo, facilitando verificación y extensión

Deficiencias

1. Alcance de Cobertura: Comparado con algunos trabajos de formalización a gran escala, el contenido teórico cubierto es relativamente limitado
2. Análisis de Rendimiento: Falta análisis profundo de complejidad computacional de operaciones de sustitución
3. Verificación Práctica: Ausencia de verificación comparativa con implementaciones de verificadores de tipos reales
4. Discusión de Extensibilidad: Discusión insuficiente de desafíos en extensión a sistemas más complejos

Impacto

1. Contribución Académica: Proporciona nueva ruta técnica para mecanización de teoría de tipos dependientes
2. Valor Práctico: Proporciona base teórica para verificación de corrección de verificadores de tipos
3. Metodología: La aplicación exitosa del método de sustitución de Stoughton puede inspirar más trabajos relacionados
4. Valor de Herramientas: La biblioteca Agda puede proporcionar infraestructura para investigación posterior

Escenarios Aplicables

1. Verificación de Verificadores de Tipos: Aplicable a escenarios que requieren verificación de corrección de verificadores de tipos
2. Investigación Educativa: Puede servir como excelente caso de estudio para aprender formalización de teoría de tipos dependientes
3. Investigación Teórica: Proporciona base para investigación de metateoría de sistemas de tipos más complejos
4. Desarrollo de Herramientas: Puede servir como implementación de referencia para desarrollo de herramientas de verificación formal

Referencias

El artículo cita 31 referencias importantes, incluyendo principalmente:

• Stoughton (1988): Teoría original de sustituciones múltiples
• Barendregt (1992): Teoría clásica de PTS
• McKinna & Pollack (1993, 1999): Formalización de PTS en LEGO
• Barras & Werner: Formalización de CC en Coq
• Urban et al. (2011): Metateoría de LF utilizando Nominal Isabelle
• Tasistro et al. (2015): Trabajo original del marco de sustitución de Stoughton

Evaluación General: Este es un artículo de alta calidad en ciencia de la computación teórica que realiza contribuciones importantes en verificación mecánica de teoría de tipos dependientes. Los puntos de innovación técnica del artículo son claros, la implementación es completa, y proporciona base teórica valiosa y experiencia práctica para investigación posterior en este campo.