Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

Resumen Técnico: Cálculo Lambda Modal de Dominio Constante Simplemente Tipado I: Reducción Beta Distanciada y Lógica Combinatoria

1. Problema y Motivación
El artículo aborda una brecha en la integración formal de la lógica modal y el cálculo lambda tipado. Mientras que Richard Montague y Dana Gallin desarrollaron sistemas que integran estos campos, su trabajo dependía de la teoría de tipos simple de Church (que incluye identidad y cuantificación) y estaba limitado en su manejo de variables de estado. Los cálculos lambda tipados contemporáneos, particularmente el cálculo lambda simplemente tipado (STLC, por sus siglas en inglés), son la base teórica estándar para la informática y la lingüística, pero carecen de las características modales específicas (como múltiples variables de estado y contextos intensionales) requeridas para el análisis semántico moderno.

El autor, Sean Walsh, identifica dos déficits primarios en los marcos existentes:

1. Fortaleza: El sistema de Montague es "demasiado fuerte" para aplicaciones modernas porque asume todos los recursos de la teoría de tipos simple de Church, mientras que los sistemas modernos suelen utilizar teorías base más débiles como el STLC.
2. Debilidad: El sistema de Montague es "demasiado débil" respecto a la expresividad modal; carece de mecanismos para la semántica bidimensional, operadores de actualidad y la vinculación de múltiples variables de estado distintas dentro de una misma expresión.

El artículo tiene como objetivo remediar esto mediante el desarrollo de un sistema, denotado como $\lambda\theta$, que integra la lógica modal con el cálculo lambda simplemente tipado. Un desafío central es la naturaleza de "variables finitas" de $\lambda\theta$: el sistema restringe el número de variables disponibles para cada tipo de estado (controlado por un parámetro $\theta$). Esta restricción impide el uso de modelos estándar de términos abiertos para probar la completitud, ya que las técnicas habituales de $\alpha$-conversión fallan cuando el número de variables disponibles es insuficiente para renombrar variables ligadas sin captura.

2. Metodología y Definiciones Centrales
El artículo introduce $\lambda\theta$ como una familia de sistemas parametrizados por $\theta$, donde $\theta$ mapea cada tipo de estado a un número cardinal (del $1$ al $\omega$) que representa el conteo de variables disponibles para ese tipo.

• Tipos: Los tipos de estado no pueden ser el codominio de un tipo funcional (es decir, si $A$ es un tipo de estado, $A \to B$ no es un tipo). Esto asegura que los términos de tipo de estado sean estrictamente variables o constantes (Proposición 2.6).
• Reducción Beta Distanciada: Una contribución novedosa es la definición de la reducción $\beta$ "distanciada". A diferencia de la reducción $\beta$ estándar donde un argumento se aplica directamente a un abstracto lambda, la reducción distanciada permite que un argumento $N$ sea separado del abstracto $\lambda v:A.L$ por una secuencia de términos intermedios $\vec{M}$:
  $$(\lambda \vec{x}: \vec{B}. \lambda v:A. L) \vec{M} N \to_\beta (\lambda \vec{x}: \vec{B}. L[v := N]) \vec{M}$$
  Este mecanismo es necesario para realizar reducciones bajo abstracciones lambda cuando el sistema carece de suficientes variables para realizar la $\alpha$-conversión estándar para evitar la captura de variables.
• Base de Lógica Combinatoria: El artículo emplea una base de lógica combinatoria centrada en los combinadores BCDKW (B, C, D, K, W) en lugar de la base tradicional SKI. La inclusión del combinador Dardinal ($D$) es específica de este sistema, manejando casos donde una constante es sustituida en una función.

3. Contribuciones Clave y Resultados

• Caracterización Combinatoria de Modelos (Teorema 1.5):
  El artículo generaliza la caracterización de Andrews de los modelos Henkin para el STLC al entorno modal. Demuestra que un marco es un modelo de $\lambda\theta$ si y solo si las denotaciones de todos los términos combinatorios BCDKW están bien definidas. Esta caracterización evita la necesidad de modelos de términos abiertos, que fallan para parámetros no máximos (por ejemplo, $\lambda_1$) debido a la falta de variables para la $\alpha$-conversión (Ejemplo 3.9).

• Conservación Semántica y Expresibilidad (Teoremas 1.1 y 1.2):
  El artículo resuelve una pregunta planteada por Zimmermann (1989) con respecto a la relación entre el sistema maximal $\lambda\omega$ (donde $\theta(A) = \omega$ para todo tipo de estado) y los sistemas restringidos $\lambda\theta$.

  • Conservación: Todo modelo de $\lambda\theta$ es un modelo de $\lambda\omega$. Por lo tanto, la validez semántica se preserva: $\lambda\theta \models M = N$ si y solo si $\lambda\omega \models M = N$.
  • Expresibilidad: Cualquier término en $\lambda\omega$ cuyas variables libres y constantes se extraigan de $\lambda\theta$ puede ser expresado por un término en $\lambda\theta$ con la misma denotación.
    Estos resultados implican que la restricción de "variables finitas" no limita la potencia expresiva del sistema en la semántica estándar; el sistema maximal es conservativo sobre los restringidos.

• Relaciones Deductivas entre Sistemas Modales y No Modales (Teoremas 1.3 y 1.4):
  El artículo establece una relación entre el sistema modal $\lambda\omega$ y el STLC ordinario no modal ($\lambda$).

  • Conservación Deductiva: Para términos en $\lambda\omega$, la igualdad $\beta\eta$ en $\lambda\omega$ se cumple si y solo si se cumple en $\lambda$.
  • Expresibilidad Deductiva: Los términos en $\lambda$ con tipos y constantes compatibles con $\lambda\omega$ pueden ser expresados dentro de $\lambda\omega$.
    Estas pruebas se basan en herramientas estándar de STLC (Church-Rosser, normalización fuerte) y son comparativamente cortas.

• Completitud mediante la Regla $\infty$ (Teorema 1.6):
  Dado que $\lambda\theta$ (para $\theta$ no maximal) carece de un modelo de términos abiertos y falla la propiedad de Church-Rosser para la reducción $\beta\eta$ estándar (Ejemplo 2.26), el artículo introduce la regla $\infty$. Esta regla permite una reducción $M \to_\infty N$ si $M =_{\beta\eta} N$ en el sistema maximal $\lambda\omega$. Con la adición de esta regla, $\lambda\theta$ se vuelve deductivamente completo con respecto a su semántica.

• Conservación Deductiva Débil (Teorema 1.7):
  El artículo investiga un cálculo lambda "débil", donde las reducciones e igualdades no se preservan bajo la abstracción lambda (sin regla $\xi$). Usando una lógica combinatoria puramente intensional (CL$\theta$) basada en la base BCDKW, el autor demuestra que las igualdades $\beta$ débiles en $\lambda\omega$ se extienden conservativamente a igualdades $\beta\eta$ en $\lambda\theta$ (siempre que la firma no contenga constantes de tipo de estado). Este resultado se basa en establecer una propiedad de Church-Rosser para la lógica combinatoria débil utilizando el método de desarrollos completos de Takahashi.

4. Significado y Reivindicaciones
El artículo afirma proporcionar el primer desarrollo exhaustivo de un cálculo lambda modal simplemente tipado "moderno" que integra los recursos del STLC contemporáneo con la lógica modal. Su importancia radica en:

1. Responder a la Pregunta de Zimmermann: Afirma en gran medida que la potencia expresiva del sistema modal maximal se captura incluso en entornos de variables finitas y restringidas, tanto semánticamente como deductivamente (con la regla $\infty$).
2. Herramientas Metateóricas: Introduce la "reducción $\beta$ distanciada" y una lógica combinatoria basada en BCDKW como herramientas esenciales para manejar sistemas con disponibilidad de variables restringida, superando el fallo de los modelos de términos abiertos estándar.
3. Semántica Intensional: Apoya la visión de que los términos de tipo $A \to B$ pueden interpretarse como procedimientos, incluso en contextos intensionales, al demostrar que el sistema restringido $\lambda\theta$ es semánticamente equivalente al sistema maximal $\lambda\omega$.

El artículo señala explícitamente sus limitaciones: no proporciona un teorema de completitud para $\lambda\theta$ utilizando solo reglas $\beta\eta$ estándar (Pregunta 4.17), y reconoce que el sistema no muestra sus interpretaciones (como las relaciones de accesibilidad) de forma evidente, requiriendo convenciones de tipado específicas para modelarlas. El artículo compañero extiende estos resultados a la teoría de tipos simple de Church.