Non-Derivability Results in Polymorphic Dependent Type Theory

Questo articolo dimostra che in $λ$P2 non è possibile derivare i principi di induzione e coinduzione per tipi di dati definiti, mostrando tramite modelli controesempio che l'estensione con l'assioma di estensionalità funzionale è essenziale per rendere provabili tali principi.

L'essenziale

Immagina di essere un architetto che sta progettando una città digitale chiamata $\lambda$P2. Questa città è costruita con regole matematiche molto precise (la "Teoria dei Tipi") e permette di creare oggetti complessi come numeri, liste di cose e funzioni che agiscono su di essi.

In questa città, c'è un problema fondamentale: puoi costruire gli "scheletri" di questi oggetti, ma non riesci a farli funzionare completamente come vorresti. È come se avessi le formule per costruire una macchina, ma non riuscissi a farla partire o a farla guidare in modo sicuro.

Questo articolo, scritto da Herman Geuvers in onore del collega Stefano Berardi, è come una serie di esperimenti scientifici per capire perché certe cose non funzionano e cosa manca per farle funzionare.

Ecco la spiegazione semplice, divisa per concetti chiave:

1. Il Problema della "Regola d'Oro" (Induzione)

Immagina di voler insegnare a un bambino a contare. Gli dai lo zero e gli dici: "Se sai contare fino a $n$, sai contare fino a $n+1$". Questa è la regola d'induzione. È il modo in cui garantiamo che la nostra logica funzioni per tutti i numeri, non solo per quelli che abbiamo già visto.

Nel sistema $\lambda$P2, gli architetti possono creare i numeri (come i famosi "numeri di Church"), ma non riescono a dimostrare che questa regola d'oro funziona per tutti i numeri possibili. È come se avessi una ricetta per fare la torta, ma non potessi dimostrare che la torta verrà buona ogni volta che la cuoci, indipendentemente dal forno che usi.

La scoperta: L'autore mostra che, nel sistema base, non importa quanto sia "intelligente" il modo in cui costruisci i numeri: la regola d'oro non può essere dimostrata. È come se mancasse un pezzo fondamentale del motore.

2. I "Fiumi Infiniti" (Tipi Co-induttivi)

Oltre ai numeri, puoi creare oggetti infiniti, come un flusso di dati (stream), simile a un fiume che non finisce mai. In matematica, per dire che due fiumi sono "uguali", non devi guardarli fino alla fine (perché non finiscono mai), ma devi controllare che ogni goccia d'acqua che esce sia uguale all'altra. Questo si chiama co-induzione.

L'autore mostra che nel sistema $\lambda$P2, anche se puoi costruire questi fiumi, non riesci a dimostrare che due fiumi che sembrano uguali (hanno la stessa acqua che esce) sono davvero la stessa cosa. È come se avessi due specchi che riflettono la stessa immagine, ma non potessi mai essere sicuro al 100% che non ci sia una differenza nascosta.

3. I "Gruppi di Amici" (Tipi Quoziente)

Immagina di avere una lista di persone e di voler dire: "Tutti quelli che hanno lo stesso colore degli occhi sono nello stesso gruppo". In matematica, questo si chiama quoziente. Crei un nuovo tipo di oggetto dove le differenze irrilevanti (come il colore degli occhi) vengono cancellate.

L'autore dimostra che nel sistema base, non puoi creare questi "gruppi di amici" in modo che funzionino per qualsiasi tipo di situazione (non sono "parametrici"). Se provi a farlo, il sistema si blocca o non rispetta le regole di uguaglianza. È come se provassi a dividere una classe di studenti in gruppi basati sui gusti musicali, ma la regola non funzionasse se cambiassi il genere musicale.

4. Cosa serve per risolvere il problema? (I Superpoteri)

Gli studiosi avevano già scoperto che aggiungendo alcuni "superpoteri" al sistema, questi problemi sparivano. Ma quali erano esattamente necessari?

L'autore ha costruito dei laboratori virtuali (modelli) per testare le combinazioni:

• Potere A (Estensione Funzionale): Se due macchine fanno esattamente la stessa cosa per ogni input, sono la stessa macchina.
• Potere B (Tipi Identità e Unicità): Se due cose sono uguali, c'è un solo modo per dimostrarlo.
• Potere C (Tipi Somma): Permette di combinare informazioni in modo più flessibile.

Il risultato sorprendente:
L'autore ha scoperto che anche se dai al sistema i Poteri B e C (i tipi identità e le somme), il sistema continua a fallire nel dimostrare la regola d'oro per i numeri.
Serve assolutamente il Potere A (Estensione Funzionale). Senza di esso, il sistema è come un'auto con le ruote e il motore, ma senza la chiave per accenderlo. L'estensione funzionale è la chiave che permette alla logica di funzionare correttamente.

In sintesi

Questo articolo è una mappa che ci dice:

1. Cosa non funziona: Nel sistema base, non puoi dimostrare che i tuoi numeri o i tuoi fiumi infiniti si comportano come dovrebbero.
2. Perché non funziona: Perché manca una regola fondamentale che dice "se due cose fanno la stessa cosa, sono la stessa cosa".
3. La soluzione: Per costruire una città digitale perfetta dove tutto funziona (induzione, co-induzione, gruppi), devi aggiungere questa regola specifica. Senza di essa, la città è incompleta.

È un lavoro di "debugging" filosofico e matematico, dedicato a un grande amico e collega, che ci aiuta a capire esattamente quali mattoni servono per costruire una logica solida e affidabile.

Sommario tecnico

Ecco una sintesi tecnica dettagliata del paper "Non-Derivability Results in Polymorphic Dependent Type Theory" di Herman Geuvers, basata sul testo fornito.

Titolo e Contesto

Titolo: Non-Derivability Results in Polymorphic Dependent Type Theory (Risultati di non derivabilità nella teoria dei tipi dipendenti polimorfi)
Autore: Herman Geuvers (Radboud University & Eindhoven University of Technology)
Contesto: Il lavoro è dedicato a Stefano Berardi e si inserisce nel dibattito sulla rappresentazione dei tipi di dati induttivi e coinduttivi nella teoria dei tipi.

1. Il Problema

Nella pura Calculus of Constructions (CC) e nella sua versione di secondo ordine con tipi dipendenti ($\lambda P2$), è possibile codificare tipi di dati (come i numeri naturali) e funzioni su di essi utilizzando l'encoding di Church. Tuttavia, un problema fondamentale è che i principi di induzione (per i tipi induttivi) e co-induzione (per i tipi co-induttivi) non sono derivabili all'interno del sistema puro.

Mentre l'encoding standard (es. numeri di Church) permette di definire i costruttori (zero, successore), non garantisce che il tipo soddisfi le proprietà di algebra iniziale o co-algebra finale.
Il paper si pone le seguenti domande aperte, sollevate da lavori precedenti (in particolare [1] e [8]):

1. È possibile definire tipi quoziente con un principio di induzione corretto in $\lambda P2$ puro, o sono necessarie estensioni?
2. I tipi co-induttivi definibili (come gli stream) soddisfano un principio di co-induzione forte (es. unicità della corecursione o equivalenza di bisimulazione) in $\lambda P2$?
3. Quali estensioni specifiche (tipi identità, UIP, estensionalità funzionale, tipi $\Sigma$) sono realmente necessarie per rendere dimostrabili i principi di induzione e co-induzione?

2. Metodologia

L'autore utilizza un approccio basato sulla costruzione di modelli controesempio (counter-models) di natura sintattica.

• Modelli Polyset: Il lavoro si basa su modelli di realizzaibilità costruiti su Algebre Combinatorie Debolmente Estensionali (WECA - Weakly Extensional Combinatory Algebras).
• Struttura del Modello: I tipi sono interpretati come sottoinsiemi dell'algebra (polyset), e i termini come elementi dell'algebra. La validità di un tipo corrisponde alla non vacuità della sua interpretazione nel modello.
• Strategia: Per dimostrare che un principio (es. induzione) non è derivabile, l'autore costruisce un modello specifico in cui:
  1. Il sistema $\lambda P2$ (o le sue estensioni) è coerente (sound).
  2. L'interpretazione del tipo che rappresenta il principio (es. il tipo dell'induzione) è vuota (non è abitata).
• Strumenti Specifici: Vengono utilizzati modelli basati su termini $\lambda$ non tipati modulo $\beta$ o $\beta\eta$, e modelli generati da costanti specifiche (come refl per i tipi identità) per controllare le proprietà di estensionalità e identità.

3. Contributi Chiave e Risultati

A. Non derivabilità del principio di co-induzione per gli Stream

• Risultato: Il tipo di stream definibile in $\lambda P2$ (come co-algebra finale) non soddisfa il principio di co-induzione.
• Dimostrazione: Viene costruito un modello in cui esistono due stream distinti ($s_1$ e $s_2$) che sono bisimili ($s_1 \sim s_2$) ma non uguali ($s_1 \neq s_2$).
• Dettaglio Tecnico: Gli stream sono codificati come tipi esistenziali. Nel modello, si possono definire due stream che producono la stessa sequenza di osservazioni finite (head/tail), ma che hanno strutture interne diverse (normal forms diversi nel calcolo $\lambda$). Poiché la bisimulazione non implica l'uguaglianza nel modello, il tipo non è una co-algebra finale.

B. Non derivabilità dei Tipi Quoziente Parametrici

• Risultato: I tipi quoziente parametrici (dove l'operazione di quoziente è polimorfa e rispetta la relazione in modo uniforme) non sono definibili in $\lambda P2$.
• Definizione: Un quoziente parametrico richiede l'esistenza di una funzione di classificazione cls polimorfa e di un eliminatore recq che rispetti la relazione.
• Dimostrazione: Viene mostrato che in certi modelli (basati su $\Lambda$, termini $\lambda$ aperti modulo $\beta$), una funzione che dovrebbe agire come cls su un quoziente parametrico sarebbe costretta a essere una funzione costante, il che porta a contraddizioni quando si applica a tipi come i booleani (dove true e false dovrebbero rimanere distinti dopo il quoziente se la relazione è l'uguaglianza).

C. Il Ruolo Cruciale dell'Estensionalità Funzionale (FunExt)

• Contesto: Il lavoro di Awodey, Frey e Speight [1] ha mostrato che aggiungendo a $\lambda P2$ tipi identità, Unicità delle Prove di Identità (UIP), estensionalità funzionale (FunExt) e tipi $\Sigma$, è possibile definire tipi induttivi con induzione provabile.
• Risultato Principale: Geuvers dimostra che l'estensionalità funzionale è necessaria.
• Dimostrazione: Viene costruito un modello esteso di $\lambda P2$ che include:
  1. Tipi identità ($=$).
  2. Tipi $\Sigma$.
  3. Unicità delle prove di identità (UIP).
  • Ma non include FunExt.
• Conclusione: In questo modello, anche se UIP e $\Sigma$ sono presenti, il principio di induzione per i numeri naturali non è derivabile. Questo prova che FunExt non è solo un'aggiunta conveniente, ma è un ingrediente essenziale per la derivabilità dell'induzione in questo contesto.

4. Significato e Implicazioni

1. Limiti di $\lambda P2$: Il paper conferma e generalizza i limiti intrinseci della teoria dei tipi polimorfa pura. Senza estensioni specifiche, non è possibile ottenere le proprietà categoriali complete (inizialità/co-finalità) per i tipi di dati codificati.
2. Gerarchia delle Estensioni: Il lavoro chiarisce la gerarchia delle estensioni necessarie:
   • Solo $\lambda P2$: Nessuna induzione/co-induzione forte.
   • $\lambda P2 + \Sigma + \text{Identity} + \text{UIP}$: Ancora nessuna induzione forte.
   • $\lambda P2 + \Sigma + \text{Identity} + \text{UIP} + \text{FunExt}$: Induzione e co-induzione diventano dimostrabili (come mostrato in [1] e [8]).
3. Natura dei Modelli: L'uso di modelli sintattici basati su algebre combinatorie debolmente estensionali permette di isolare proprietà specifiche (come l'estensionalità) e dimostrare la loro indispensabilità in modo più diretto rispetto ai modelli semantici tradizionali (es. modelli PER).
4. Riferimento a Berardi: Il lavoro onora il contributo di Stefano Berardi allo studio di modelli non parametrici e alla comprensione delle limitazioni dei sistemi di tipi, continuando la sua linea di ricerca sulla rappresentazione dei dati e dei principi di ragionamento.

In sintesi, il paper fornisce una risposta negativa rigorosa alla possibilità di ottenere principi di induzione e co-induzione forti in $\lambda P2$ puro o con estensioni parziali, identificando l'estensionalità funzionale come il fattore critico mancante per rendere tali principi dimostrabili.