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

Resumo Técnico: Cálculo Lambda Modal de Domínio Constante Simplesmente Tipado I: Redução Beta Distanciada e Lógica Combinatória

1. Problema e Motivação
O artigo aborda uma lacuna na integração formal da lógica modal e do cálculo lambda tipado. Embora Richard Montague e Dana Gallin tenham desenvolvido sistemas que integram esses campos, o trabalho deles baseava-se na teoria de tipos simples de Church (que inclui identidade e quantificação) e era limitado no tratamento de variáveis de estado. Os cálculos lambda tipados contemporâneos, particularmente o cálculo lambda simplesmente tipado (STLC), são a base teórica padrão para a ciência da computação e a linguística, mas carecem das características modais específicas (como múltiplas variáveis de estado e contextos intencionais) necessárias para a análise semântica moderna.

O autor, Sean Walsh, identifica dois déficits primários nos sistemas existentes:

1. Força: O sistema de Montague é "forte demais" para aplicações modernas porque assume todos os recursos da teoria de tipos simples de Church, enquanto sistemas modernos frequentemente utilizam bases teóricas mais fracas como o STLC.
2. Fraqueza: O sistema de Montague é "fraco demais" em termos de expressividade modal; carece de mecanismos para semântica bidimensional, operadores de atualidade e o vínculo de múltiplas variáveis de estado distintas dentro de uma única expressão.

O artigo visa remediar isso desenvolvendo um sistema, denotado por $\lambda\theta$, que integra a lógica modal com o cálculo lambda simplesmente tipado. Um desafio central é a natureza de "variáveis finitas" de $\lambda\theta$: o sistema restringe o número de variáveis disponíveis para cada tipo de estado (controlado por um parâmetro $\theta$). Essa restrição impede o uso de modelos padrão de termos abertos para provar a completude, uma vez que as técnicas usuais de $\alpha$-conversão falham quando o número de variáveis disponíveis é insuficiente para renomear variáveis ligadas sem captura.

2. Metodologia e Definições Principais
O artigo introduz $\lambda\theta$ como uma família de sistemas parametrizados por $\theta$, onde $\theta$ mapeia cada tipo de estado a um número cardinal (de $1$a$\omega$) representando a contagem de variáveis disponíveis para esse tipo.

• Tipos: Tipos de estado não podem ser o codomínio de um tipo funcional (ou seja, se $A$ é um tipo de estado, $A \to B$ não é um tipo). Isso garante que termos de tipo de estado sejam estritamente variáveis ou constantes (Proposição 2.6).
• Redução Beta Distanciada: Uma contribuição inovadora é a definição de redução $\beta$-distanciada. Diferente da redução $\beta$ padrão, onde um argumento é aplicado diretamente a um abstrato lambda, a redução distanciada permite que um argumento $N$ seja separado do abstrato $\lambda v:A.L$ por uma sequência de termos intermediários $\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 é necessário para realizar reduções sob abstrações lambda quando o sistema carece de variáveis suficientes para realizar a $\alpha$-conversão padrão para evitar a captura de variáveis.
• Base de Lógica Combinatória: O artigo emprega uma base de lógica combinatória centrada nos combinadores BCDKW (B, C, D, K, W) em vez da tradicional base SKI. A inclusão do combinador Dardinal ($D$) é específica para este sistema, lidando com casos onde uma constante é substituída em uma função.

3. Contribuições Principais e Resultados

• Caracterização Combinatória de Modelos (Teorema 1.5):
  O artigo generaliza a caracterização de Andrews para modelos de Henkin para o STLC para o cenário modal. Prova-se que um quadro (frame) é um modelo de $\lambda\theta$ se, e somente se, as denotações de todos os termos combinatórios BCDKW forem bem definidas. Esta caracterização evita a necessidade de modelos de termos abertos, que falham para parâmetros não maximais (ex: $\lambda_1$) devido à falta de variáveis para $\alpha$-conversão (Exemplo 3.9).

• Conservação Semântica e Expressibilidade (Teoremas 1.1 & 1.2):
  O artigo resolve uma questão colocada por Zimmermann (1989) sobre a relação entre o sistema maximal $\lambda\omega$ (onde $\theta(A) = \omega$ para todo tipo de estado) e os sistemas restritos $\lambda\theta$.

  • Conservação: Todo modelo de $\lambda\theta$ é um modelo de $\lambda\omega$. Assim, a validade semântica é preservada: $\lambda\theta \models M = N$ se, e somente se, $\lambda\omega \models M = N$.
  • Expressibilidade: Qualquer termo em $\lambda\omega$ cujas variáveis livres e constantes sejam extraídas de $\lambda\theta$ pode ser expresso por um termo em $\lambda\theta$ com a mesma denotação.
    Estes resultados implicam que a restrição de "variáveis finitas" não limita o poder expressivo do sistema na semântica padrão; o sistema maximal é conservativo sobre os sistemas restritos.

• Relações Dedutivas entre Sistemas Modais e Não-Modais (Teoremas 1.3 & 1.4):
  O artigo estabelece uma relação entre o sistema modal $\lambda\omega$ e o STLC comum não-modal ($\lambda$).

  • Conservação Dedutiva: Para termos em $\lambda\omega$, a igualdade $\beta\eta$ em $\lambda\omega$ ocorre se, e somente se, ocorrer em $\lambda$.
  • Expressibilidade Dedutiva: Termos em $\lambda$ com tipos e constantes compatíveis com $\lambda\omega$ podem ser expressos dentro de $\lambda\omega$.
    Estas provas baseiam-se em ferramentas padrão do STLC (Church-Rosser, normalização forte) e são comparativamente curtas.

• Completude via Regra $\infty$ (Teorema 1.6):
  Como $\lambda\theta$ (para $\theta$ não-maximal) carece de um modelo de termos abertos e falha na propriedade Church-Rosser para a redução $\beta\eta$ padrão (Exemplo 2.26), o artigo introduz a regra $\infty$. Esta regra permite uma redução $M \to_\infty N$ se $M =_{\beta\eta} N$ no sistema maximal $\lambda\omega$. Com a adição desta regra, $\lambda\theta$ torna-se dedutivamente completo em relação à sua semântica.

• Conservação Dedutiva Fraca (Teorema 1.7):
  O artigo investiga o cálculo lambda "fraco", onde reduções e igualdades não são preservadas sob abstração lambda (sem a regra $\xi$). Usando uma lógica combinatória pura (CL$\theta$) baseada na base BCDKW, o autor prova que as igualdades $\beta$ fracas em $\lambda\omega$ são estendidas conservativamente para igualdades $\beta\eta$ em $\lambda\theta$ (desde que a assinatura não contenha constantes de tipo de estado). Este resultado baseia-se no estabelecimento de uma propriedade Church-Rosser para a lógica combinatória fraca usando o método de desenvolvimentos completos de Takahashi.

4. Significância e Alegações
O artigo afirma fornecer o primeiro desenvolvimento minucioso de um cálculo lambda modal simplesmente tipado "moderno" que integra os recursos do STLC contemporâneo com a lógica modal. Sua significância reside em:

1. Respondendo à Questão de Zimmermann: Ele afirma amplamente que o poder expressivo do sistema modal maximal é capturado mesmo em configurações de variáveis finitas e restritas, tanto semântica quanto (com a regra $\infty$) dedutivamente.
2. Ferramentas Metateóricas: Introduz a "redução $\beta$ distanciada" e uma lógica combinatória baseada em BCDKW como ferramentas essenciais para lidar com sistemas de disponibilidade de variáveis restrita, superando a falha dos modelos de termos abertos padrão.
3. Semântica Intencional: Suporta a visão de que termos de tipo $A \to B$ podem ser interpretados como procedimentos, mesmo em contextos intencionais, ao mostrar que o sistema restrito $\lambda\theta$ é semanticamente equivalente ao sistema maximal $\lambda\omega$.

O artigo nota explicitamente limitações: ele não fornece um teorema de completude para $\lambda\theta$ usando apenas regras $\beta\eta$ padrão (Questão 4.17), e reconhece que o sistema não exibe suas interpretações (como relações de acessibilidade) de forma explícita, exigindo convenções de tipagem específicas para modelá-las. O artigo complementar estende estes resultados para a teoria de tipos simples de Church.