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

Sintesi Tecnica: Lambda Calcolo Modale a Tipo Semplice e Dominio Costante I: Riduzione Beta Distanziata e Logica Combinatoria

1. Problema e Motivazione
Il saggio affronta una lacuna nell'integrazione formale tra la logica modale e il lambda calcolo tipizzato. Sebbene Richard Montague e Dana Gallin abbiano sviluppato sistemi che integrano questi campi, il loro lavoro si basava sulla teoria dei tipi semplice di Church (che include l'identità e la quantificazione) ed era limitato nella gestione delle variabili di stato. I contemporanei lambda calcoli tipizzati, in particolare il lambda calcolo tipizzato semplice (STLC), sono la base teorica standard per l'informatica e la linguistica, ma mancano delle specifiche caratteristiche modali (come le molteplici variabili di stato e i contesti intensionali) richieste dalla moderna analisi semantica.

L'autore, Sean Walsh, identifica due deficit primari nei framework esistenti:

1. Forza: Il sistema di Montague è "troppo forte" per le applicazioni moderne perché assume tutte le risorse della teoria dei tipi semplice di Church, mentre i sistemi moderni spesso utilizzano basi teoriche più deboli come l'STLC.
2. Debolezza: Il sistema di Montague è "troppo debole" riguardo all'espressività modale; manca di meccanismi per la semantica bidimensionale, gli operatori di attualità e il legame di molteplici variabili di stato distinte all'interno di un singolo termine.

Il saggio mira a rimediare a ciò sviluppando un sistema, denotato $\lambda\theta$, che integra la logica modale con il lambda calcolo tipizzato semplice. Una sfida centrale è la natura a "variabili finite" di $\lambda\theta$: il sistema restringe il numero di variabili disponibili per ogni tipo di stato (controllato da un parametro $\theta$). Questa restrizione impedisce l'uso di modelli di termini aperti standard per dimostrare la completezza, poiché le consuete tecniche di $\alpha$-conversione falliscono quando il numero di variabili disponibili è insufficiente per rinominare le variabili legate senza cattura.

2. Metodologia e Definizioni Core
Il solo introduce $\lambda\theta$ come una famiglia di sistemi parametrizzati da $\theta$, dove $\theta$ mappa ogni tipo di stato a un numero cardinale (da $1$a$\omega$) che rappresenta il conteggio delle variabili disponibili per quel tipo.

• Tipi: I tipi di stato non possono essere il codominio di un tipo funzionale (ovvero, se $A$ è un tipo di stato, $A \to B$ non è un tipo). Ciò assicura che i termini di tipo di stato siano strettamente variabili o costanti (Proposizione 2.6).
• Riduzione Beta Distanziata: Un contributo innovativo è la definizione di riduzione $\beta$-distanziata. A differenza della riduzione $\beta$ standard dove un argomento è applicato direttamente a un astratto lambda, la riduzione distanziata permette a un argomento $N$ di essere separato dall'astratto $\lambda v:A.L$ da una sequenza di termini intermedi $\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}$$
  Questo meccanismo è necessario per eseguire riduzioni sotto le astrazioni lambda quando il sistema manca di variabili sufficienti per eseguire la $\alpha$-conversione standard per evitare la cattura delle variabili.
• Base di Logica Combinatoria: Il saggio impiega una base di logica combinatoria centrata sui combinatori BCDKW (B, C, D, K, W) piuttosto che sulla tradizionale base SKI. L'inclusione del combinatore Dardinal ($D$) è specifica per questo sistema, gestendo i casi in cui una costante viene sostituita in una funzione.

3. Contributi Chiave e Risultati

• Caratterizzazione Combinatoria dei Modelli (Teorema 1.5):
  Il saggio generalizza la caratterizzazione di Andrews dei modelli Henkin per l'STLC al contesto modale. Dimostra che un frame è un modello di $\lambda\theta$ se e solo se le denotazioni di tutti i termini combinatori BCDKW sono ben definite. Questa caratterizzazione evita la necessità di modelli di termini aperti, che falliscono per parametri non massimali (ad esempio $\lambda_1$) a causa della mancanza di variabili per l'$\alpha$-conversione (Esempio 3.9).

• Conservazione Semantica ed Espressività (Teoremi 1.1 & 1.2):
  Il saggio risolve una questione posta da Zimmermann (1989) riguardante la relazione tra il sistema massimale $\lambda\omega$ (dove $\theta(A) = \omega$ per ogni tipo di stato) e i sistemi ristretti $\lambda\theta$.

  • Conservazione: Ogni modello di $\lambda\theta$ è un modello di $\lambda\omega$. Pertanto, la validità semantica è preservata: $\lambda\theta \models M = N$ se e solo se $\lambda\omega \models M = N$.
  • Espressività: Qualsiasi termine in $\lambda\omega$ le cui variabili libere e costanti sono tratte da $\lambda\theta$ può essere espresso da un termine in $\lambda\theta$ con la stessa denotazione.
    Questi risultati implicano che la restrizione a "variabili finite" non limita il potere espressivo del sistema nella semantica standard; il sistema massimale è conservativo rispetto a quelli ristretti.

• Relazioni Deduttive tra Sistemi Modali e Non Modali (Teoremi 1.3 & 1.4):
  Il saggio stabilisce una relazione tra il sistema modale $\lambda\omega$ e l'ordinario STLC non modale ($\lambda$).

  • Conservazione Deduttiva: Per i termini in $\lambda\omega$, l'uguaglianza $\beta\eta$ in $\lambda\omega$ vale se e solo se vale in $\lambda$.
  • Espressività Deduttiva: Termini in $\lambda$ con tipi e costanti compatibili con $\lambda\omega$ possono essere espressi all'interno di $\lambda\omega$.
    Queste prove si basano sugli strumenti standard di STLC (Church-Rosser, normalizzazione forte) e sono comparativamente brevi.

• Completezza tramite la Regola $\infty$ (Teorema 1.6):
  Poiché $\lambda\theta$ (per $\theta$ non massimale) manca di un modello di termini aperti e non soddisfa la proprietà di Church-Rosser per la riduzione $\beta\eta$ standard (Esempio 2.26), il saggio introduce la regola $\infty$. Questa regola permette una riduzione $M \to_\infty N$ se $M =_{\beta\eta} N$ nel sistema massimale $\lambda\omega$. Con l'aggiunta di questa regola, $\lambda\theta$ diventa deduttivamente completo rispetto alla sua semantica.

• Conservazione Deduttiva Debole (Teorema 1.7):
  Il saggio investiga il lambda calcolo "debole", dove riduzioni e uguaglianze non sono preservate sotto astrazione lambda (assenza della regola $\xi$). Utilizzando una logica combinatoria intensionale pura (CL$\theta$) basata sulla base BCDKW, l'autore dimostra che le $\beta$-uguaglianze deboli in $\lambda\omega$ sono estese conservativamente alle $\beta\eta$-uguaglianze in $\lambda\theta$ (a condizione che la firma non contenga costanti di tipo di stato). Questo risultato si basa sull'instaurazione di una proprietà Church-Rosser per la logica combinatoria debole usando il metodo dei completi sviluppi di Takahashi.

4. Significato e Rivendicazioni
Il saggio sostiene di fornire il primo sviluppo approfondito di un "moderno" lambda calcolo modale a tipo semplice che integri le risorse del contemporaneo STLC con la logica modale. La sua importanza risiede in:

1. Rispondere alla Domanda di Zimmermann: Esso afferma ampiamente che il potere espressivo del sistema modale massimale è catturato anche in contesti ristretti di variabili finite, sia semanticamente che deduttivamente (con la regola $\infty$).
2. Strumenti Metateorici: Introduce la "riduzione $\beta$ distanziata" e una logica combinatoria basata su BCDKW come strumenti essenziali per gestire sistemi con disponibilità di variabili ristretta, superando il fallimento dei modelli standard di termini aperti.
3. Semantica Intensionale: Supporta la visione che i termini di tipo $A \to B$ possano essere interpretati come procedure, anche in contesti intensionali, mostrando che il sistema ristretto $\lambda\theta$ è semanticamente equivalente al sistema massimale $\lambda\omega$.

Il saggio nota esplicitamente i limiti: non fornisce un teorema di completezza per $\lambda\theta$ utilizzando solo le regole $\beta\eta$ standard (Domanda 4.17), e riconosce che il sistema non mostra le sue interpretazioni (come le relazioni di accessibilità) in modo esplicito, richiedendo convenzioni di tipizzazione specifiche per modellarle. Il saggio complementare estende questi risultati alla teoria dei tipi semplice di Church.