Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!

Questo articolo introduce una nuova teoria equazionale per il calcolo $\lambda$I basata sugli "Ohana trees", che preservano le variabili nascoste o infinite, e ne dimostra la coerenza attraverso l'analisi di approssimazione, l'espansione di Taylor e un modello denotazionale basato su un sistema di tipi relazionale modificato.

L'essenziale

🌳 Ohana Trees: Non lasciare indietro nessun "amico" (variabile)

Immagina il Calcolo Lambda come un gigantesco laboratorio di cucina dove gli chef (i programmatori) creano ricette (i programmi) usando ingredienti (le variabili). Esiste una regola speciale in questo laboratorio, chiamata λI-calculus: qui, ogni volta che uno chef introduce un nuovo ingrediente in una ricetta, deve usarlo almeno una volta. Non puoi dire "aggiungo la cipolla" e poi non usarla mai (nessun "spreco" o cancellazione).

Il problema è che, finora, quando gli informatici cercavano di capire cosa succede a lungo termine a queste ricette (quando vengono cucinate all'infinito), usavano una mappa chiamata "Albero di Böhm". Questa mappa era un po' come una foto sfocata: se un ingrediente veniva spinto così lontano nel futuro da diventare invisibile, o se era nascosto dietro un piatto che non finiva mai di cuocere, la mappa diceva semplicemente "Non c'è nulla qui" e lo cancellava dalla memoria.

Il risultato? Due ricette che sembravano diverse perché avevano ingredienti nascosti, venivano considerate identiche. Era come se due amici si nascondessero in stanze diverse, ma la mappa dicesse che erano nella stessa stanza vuota.

🌟 La Soluzione: Gli "Alberi Ohana"

Gli autori di questo paper (Remy, Giulio e Alexis) hanno detto: "No! In famiglia (Ohana), nessuno viene lasciato indietro o dimenticato!".

Hanno inventato una nuova mappa chiamata Albero Ohana.
Immagina che ogni volta che un ingrediente (una variabile) viene spinto in una stanza segreta o spinto all'infinito, invece di cancellarlo, lo etichettiamo con un adesivo.

• Se un ingrediente è nascosto dietro un piatto che non finisce mai, l'Albero Ohana dice: "Qui c'è un piatto infinito, ma ricorda che c'è anche l'ingrediente X nascosto dietro".
• Se un ingrediente viene spinto all'infinito, l'albero dice: "Stiamo andando all'infinito, ma l'ingrediente Y ci sta seguendo".

In pratica, l'Albero Ohana è una mappa che ricorda tutto, anche le cose che sembrano sparite. Questo permette di distinguere ricette che prima sembravano uguali.

🔍 Come funziona la magia? (Due approcci)

Per dimostrare che questa nuova mappa funziona, gli autori hanno usato due metodi diversi, come due modi diversi di smontare un giocattolo per vederne i pezzi:

1. L'approccio classico (Approssimazione Continua):
   Immagina di guardare un film a scatti. Prima vedi solo il primo fotogramma, poi i primi due, poi i primi tre. Ogni fotogramma è una "stima" finita della ricetta. Gli autori hanno mostrato che se guardi abbastanza fotogrammi (approssimazioni finite), riesci a ricostruire perfettamente l'Albero Ohana completo. È come guardare un puzzle: più pezzi aggiungi, più l'immagine diventa chiara e ricorda tutto.

2. L'approccio "Taylor" (Scomposizione in risorse):
   Questo è più tecnico. Immagina di prendere una ricetta complessa e di scomporla in una serie infinita di "ingredienti base" che non possono essere duplicati né buttati via (come in un laboratorio di chimica molto rigoroso).
   Gli autori hanno creato un nuovo linguaggio (un "calcolo delle risorse con memoria") dove ogni ingrediente ha un'etichetta che ricorda da dove viene. Hanno dimostrato che se prendi la ricetta originale, la trasformi in questi ingredienti base, e poi li ricompili, ottieni esattamente la stessa struttura dell'Albero Ohana. È come dire: "Se smonti il giocattolo e lo rimonti seguendo le regole giuste, ottieni lo stesso oggetto, ma ora sappiamo esattamente dov'era ogni vite".

🧩 Il Modello Matematico (Il "Cervello" che ricorda)

Infine, hanno costruito un "cervello" matematico (un modello denotazionale) che impara a riconoscere queste ricette.
Immagina un sistema di classificazione (tipi) dove, invece di dire solo "Questa ricetta è un dolce", diciamo: "Questa ricetta è un dolce che usa 3 uova, ma ne nasconde 2 in un sacchetto etichettato 'X'".
Questo sistema è così preciso che due ricette hanno lo stesso "cervello" (stesso modello) se e solo se hanno lo stesso Albero Ohana. Se anche un solo ingrediente è stato dimenticato o etichettato diversamente, il sistema le distingue immediatamente.

💡 Perché è importante?

Fino ad oggi, per il λI-calculus (la versione senza sprechi), non c'era un modo soddisfacente per dire "questa ricetta è diversa da quella" quando entrambe sembravano infinite o confuse.
Con gli Alberi Ohana, gli autori hanno:

1. Creato una mappa che non perde mai traccia delle variabili.
2. Dimostrato che questa mappa è logica e coerente (se cambi una parte della ricetta, la mappa cambia in modo prevedibile).
3. Costruito un sistema matematico che "vede" esattamente queste differenze.

È come se avessimo inventato un nuovo tipo di occhiali che permette di vedere i dettagli nascosti di un programma, assicurandosi che nessuna variabile venga mai lasciata indietro, proprio come dice il titolo: Ohana significa famiglia, e in famiglia nessuno viene dimenticato!

Sommario tecnico

Ecco una sintesi tecnica dettagliata del paper "Ohana Trees, Linear Approximation and Multi-Types for the $\lambda$I-Calculus: No Variable Gets Left Behind or Forgotten!" di Rémy Cerda, Giulio Manzonetto e Alexis Saurin.

1. Il Problema e il Contesto

Il calcolo $\lambda$I è un sottocalcolo naturale del calcolo $\lambda$ classico, ottenuto vietando l'indebolimento (weakening): ogni astrazione $\lambda x.M$ deve legare almeno una occorrenza della variabile $x$. Sebbene storicamente utile per risultati come la finitezza degli sviluppi e la standardizzazione, le sue teorie equazionali hanno ricevuto scarsa attenzione.

Il problema centrale identificato dagli autori è la mancanza di modelli denotazionali informativi per il $\lambda$I-calcolo.

• Limiti dei modelli esistenti: Tutti i modelli denotazionali "propri" studiati in letteratura inducono teorie che equiparano tutti i termini non normalizzabili. Di conseguenza, la teoria risultante è banale (spesso coincide con la teoria $H_I$ o la sua versione estensionale $H^\eta_I$).
• Inadeguatezza degli Alberi di Böhm: Gli alberi di Böhm (BT), standard per il calcolo $\lambda$ completo, non sono adatti al $\lambda$I-calcolo. Poiché i BT sono definiti coinduttivamente, possono "spingere all'infinito" o "dimenticare" variabili libere che non vengono mai cancellate durante la riduzione ma scompaiono nel limite (es. nel termine $L_l$, la variabile $l$ è persistente ma scompare nell'albero di Böhm). Questo porta a situazioni in cui termini $\lambda$I distinti hanno lo stesso BT, violando l'intuizione che nessuna variabile dovrebbe essere persa in un calcolo senza indebolimento.

2. Metodologia e Approccio

Gli autori propongono un approccio trifase per costruire una nuova teoria non banale per il $\lambda$I-calcolo:

1. Definizione Sintattica (Alberi Ohana): Introduzione di una nuova nozione di albero di valutazione che traccia esplicitamente tutte le variabili libere, anche quelle nascoste in sottotermini privi di significato o spinte all'infinito.
2. Approssimazione Lineare (Taylor Expansion): Sviluppo di un calcolo delle risorse con memoria e di una espansione di Taylor qualitativa specifica per il $\lambda$I, capace di catturare la struttura degli alberi Ohana.
3. Semantica Denotazionale (Sistema di Tipi Multi): Costruzione di un modello denotazionale basato su un sistema di tipi intersezione non idempotente (multi-types) esteso con un ambiente separato per tracciare le variabili.

3. Contributi Chiave e Risultati

A. Gli Alberi Ohana (Ohana Trees)

Gli autori definiscono gli Alberi Ohana (OT) come una versione annotata degli alberi di Böhm.

• Definizione: Ogni nodo $\bot$ (rappresentante un termine senza forma normale di testa) e ogni applicazione nell'albero sono annotati con l'insieme delle variabili libere del termine che genera quel sottoprodotto.
• Proprietà Fondamentale: Gli OT sono invarianti per $\beta$-conversione. A differenza dei BT, gli OT non "dimenticano" le variabili: se una variabile è presente nel termine originale e non viene mai cancellata, essa rimane visibile nell'albero, anche se spinta all'infinito o nascosta dietro un $\bot$.
• Teoria di Approssimazione Continua: Viene dimostrato un teorema di approssimazione continua (Teorema 3.13): l'albero Ohana di un termine è univocamente determinato dall'insieme diretto dei suoi approssimanti finiti (alberi Ohana finiti). Questo stabilisce che l'uguaglianza degli OT è una teoria $\lambda$I coerente.

B. Calcolo delle Risorse con Memoria ed Espansione di Taylor

Per collegare gli OT alla semantica lineare, gli autori introducono un calcolo delle risorse $\lambda$I con memoria.

• Memoria: I termini risorse annotano i "buchi" vuoti (bagni vuoti) e le somme nulle con insiemi di variabili ($1_X$,$0_X$) che ricordano le variabili libere del termine originale.
• Sostituzione: Viene definita una sostituzione di risorse che gestisce sia la sostituzione lineare (distributiva sui bag) sia la sostituzione non lineare della "memoria" (aggiornamento degli insiemi di variabili).
• Teorema di Commutazione (Teorema 5.6): Il risultato centrale di questa sezione stabilisce che la forma normale dell'espansione di Taylor di un termine $\lambda$I coincide con l'espansione di Taylor del suo albero Ohana.
  $$\text{nf}(T_m(M)) = T_m(\text{OT}(M))$$
  Questo implica che l'uguaglianza indotta dagli alberi Ohana coincide con l'uguaglianza indotta dalle forme normali delle espansioni di Taylor.

C. Modello Denotazionale e Sistema di Tipi Multi

Viene costruito un modello denotazionale basato sulla semantica relazionale della logica lineare, ma modificato per catturare la teoria degli OT.

• Ambiente Separato: Il sistema di tipi introduce un secondo ambiente $\Delta$ accanto all'ambiente di tipi standard $\Gamma$. Mentre $\Gamma$ assegna tipi ai variabili, $\Delta$ traccia la corrispondenza tra le variabili nel termine e le variabili libere dei termini che verranno sostituite al loro posto. Questo è cruciale per gestire l'$\alpha$-conversione e le variabili "nascoste".
• Tipi Annotati: I tipi includono annotazioni di insiemi di variabili (es. $[]_X$) per gestire i casi in cui un argomento non viene utilizzato ma le sue variabili devono essere ricordate.
• Caratterizzazione (Teorema 6.11): Il modello è esattamente caratterizzante: due termini $\lambda$I hanno lo stesso albero Ohana se e solo se hanno lo stesso insieme di giudizi di tipaggio (semantica denotazionale).
  $$\text{OT}(M) = \text{OT}(N) \iff [[M]] = [[N]]$$
  Questo dimostra che la teoria indotta dagli alberi Ohana è compatibile con applicazione e astrazione, confermandola come una vera teoria $\lambda$I.

4. Significato e Impatto

• Nuova Teoria Non Banale: Il lavoro risolve il problema della scarsità di teorie informative per il $\lambda$I-calcolo, fornendo una teoria che distingue termini che i modelli precedenti equiparavano (es. termini con variabili persistenti ma non utilizzate).
• Generalizzazione dei Risultati di Ehrhard-Regnier: Estende la potente teoria dell'espansione di Taylor e la commutazione con gli alberi di Böhm al contesto del $\lambda$I-calcolo, introducendo la necessità di gestire la "memoria" delle variabili.
• Strumenti per l'Analisi: Fornisce strumenti sintattici (alberi Ohana), operazionali (calcolo delle risorse) e denotazionali (tipi multi) per analizzare programmi in contesti dove l'indebolimento è vietato, con potenziali applicazioni nella verifica di programmi e nella teoria dei linguaggi di programmazione.
• Futuro: Gli autori suggeriscono che questa metodologia potrebbe essere estesa ad altri tipi di alberi (Lévy-Longo, Berarducci) e potenzialmente al calcolo $\lambda$ completo, sebbene quest'ultimo presenti sfide significative legate alla compatibilità con l'applicazione.

In sintesi, il paper introduce una teoria robusta e non banale per il $\lambda$I-calcolo, dimostrando che è possibile costruire modelli denotazionali che rispettano la persistenza delle variabili, un aspetto fondamentale che i modelli tradizionali ignoravano.