La teoria dei tipi intuizionista (nota anche come teoria dei tipi costruttiva o teoria dei tipi di Martin-Löf) è una teoria dei tipi e una fondazione della matematica alternativa. Fu creata da Per Martin-Löf, matematico e filosofo svedese, che la pubblicò per la prima volta nel 1972. Esistono diverse versioni della teoria: Martin-Löf ha proposto varianti intensionali, estensionali e inizialmente impredicative, delle quali il paradosso di Girard ha mostrato l'incoerenza, dando il via alle versioni predicative. Tuttavia, tutte le versioni mantengono il design centrale della logica costruttiva, utilizzando tipi dipendenti.
Design Martin-Löf progettò la teoria dei tipi basandosi sui principi del costruttivismo matematico. Il costruttivismo richiede a una qualunque dimostrazione di esistenza di esibire un "testimone". Ad esempio, qualsiasi prova che esista un numero primo maggiore di 1000 deve identificare un numero specifico che è sia primo che maggiore di 1000. La teoria dei tipi intuizionista ha raggiunto quest'obiettivo interiorizzando l'interpretazione BHK. Una conseguenza interessante è che le dimostrazioni diventano oggetti matematici che possono essere esaminati, confrontati e manipolati.
I costruttori dei tipi sono stati strutturati in modo che seguissero una corrispondenza uno a uno con i connettivi logici. Ad esempio, l'implicazione logica () corrisponde al tipo funzione (). Questa corrispondenza si chiama isomorfismo di Curry-Howard. Anche le precedenti teorie dei tipi avevano seguito questo isomorfismo, ma quelle di Martin-Löf furono le prime ad estenderlo alla logica predicativa, introducendo i tipi dipendenti.
Teoria dei tipi La teoria dei tipi intuizionista ha 3 tipi finiti, che sono composti usando 5 diversi costruttori. A differenza delle teorie degli insiemi, le teorie dei tipi non sono costruite sulla logica del primo ordine. Quindi, ogni aspetto della teoria dei tipi ha una doppia interpretazione: sia come oggetto matematico che come componente logico.
Se non hai familiarità con la teoria dei tipi e conosci la teoria degli insiemi, un breve riepilogo è: i tipi contengono termini proprio come gli insiemi contengono elementi. I termini appartengono a un solo tipo. Termini come e calcolano ("si riducono a") termini canonici come 4. Per approfondire, vedi l'articolo sulla teoria dei tipi .
Tipo 0, tipo 1 e tipo 2 Ci sono tre tipi finiti: il tipo 0 contiene 0 termini, il tipo 1 contiene un termine canonico e il tipo 2 contiene 2 termini canonici.
Poiché il tipo 0 contiene 0 termini, viene anche chiamato tipo vuoto. È usato per rappresentare tutto ciò che non può esistere. È anche scritto e rappresenta proposizioni refutabili (ovvero, per le quali non può esistere una dimostrazione). Di conseguenza, la negazione è definita come una funzione in : .
Allo stesso modo, il tipo 1 contiene 1 termine canonico e rappresenta l'esistenza. Viene anche chiamato tipo unità. Spesso rappresenta proposizioni che possono essere dimostrate, pertanto, a volte è scritto .
Infine, il tipo 2 contiene 2 termini canonici. Rappresenta una scelta definita tra due valori. È usato per valori booleani, ma non per proposizioni. Le proposizioni sono considerate essere il tipo 1 e possono essere refutabili (di tipo 0), oppure possono non essere dimostrabili né refutabili (la legge del terzo escluso non vale nella teoria dei tipi intuizionista).
Costruttore Σ I Σ-tipi contengono coppie ordinate. Come per i tipici insiemi di coppie ordinate, un Σ-tipo descrive il prodotto cartesiano () di altri due tipi, e . Logicamente, una tale coppia ordinata avrebbe una prova di e una prova di , quindi si può vedere un Σ-tipo scritto come .
I Σ-tipi sono più potenti dei tipici insiemi di coppie ordinate, a causa della tipizzazione dipendente. Nella coppia ordinata, il tipo del secondo termine può dipendere dal valore del primo termine. Ad esempio, il primo termine della coppia potrebbe essere un numero naturale e il tipo del secondo termine potrebbe essere un vettore di lunghezza pari al primo termine. Un tale tipo si scriverebbe così:
Usando la terminologia della teoria degli insiemi, ciò è simile ad unioni disgiunte indicizzate di insiemi. Nel caso delle normali coppie ordinate, il tipo del secondo termine non dipende dal valore del primo termine. Quindi, l'insieme che descrive il prodotto cartesiano è scritto come:
È importante notare che il valore del primo termine, , non dipende dal tipo del secondo termine, .
Ovviamente, i Σ-tipi possono essere usati per costruire ennuple più lunghe dipendentemente tipizzate, usate in matematica, e i record o structs, usati nella maggior parte dei linguaggi di programmazione. Un esempio di tripla dipendentemente tipizzata è composto da due numeri interi e da una dimostrazione che il primo è più piccolo del secondo, descritta dal tipo:
La tipizzazione dipendente consente ai Σ-tipi di svolgere il ruolo di quantificatore esistenziale. L'affermazione "esiste un di tipo , tale che è dimostrato" diventa il tipo di coppie ordinate in cui il primo termine è il valore e il secondo è una dimostrazione di . Si noti che il tipo del secondo termine (dimostrazioni di ) dipende dal valore del primo elemento (). Il suo tipo è:
Costruttore Π I Π-tipi rappresentano funzioni. Come con le normali funzioni, sono costituiti da un tipo di input e un tipo di output. Sono tuttavia più potenti delle normali funzioni, in quanto il tipo di valori restituiti può dipendere dal valore in input. Le funzioni della teoria dei tipi sono diverse da quelle della teoria degli insiemi. Nella teoria degli insiemi, cerchi il valore dell'argomento in un insieme di coppie ordinate. Nella teoria dei tipi, l'argomento viene inserito in un termine e quindi il calcolo ("riduzione") viene applicato al termine.
Ad esempio, un tipo di funzione che, dato un numero naturale , restituisce un vettore contenente numeri reali, è scritto come:
Quando il tipo di output non dipende dal valore in input, la funzione viene spesso scritta semplicemente con un . Così, è il tipo di funzioni dai numeri naturali ai numeri reali. I Π-tipi corrispondono all'implicazione logica. La proposizione corrisponde al tipo , contenente funzioni che accettano dimostrazioni di A e restituiscono dimostrazioni di B. Questo tipo potrebbe essere scritto in modo più coerente come:
I Π-tipi sono anche usati in logica per la quantificazione universale. L'affermazione "per ogni di tipo , è dimostrato" diventa una funzione da alle dimostrazioni di . Quindi, dato un valore ad , la funzione genera una prova che vale per quel valore. Il tipo si scrive come:
Costruttore = Gli =-tipi vengono creati con due termini. Dati due termini come e , si può creare un nuovo tipo . I termini del nuovo tipo dimostrano che la coppia si riduce allo stesso termine canonico. Quindi, dal momento che entrambi e si riducono al termine canonico , ci sarà un termine del tipo . Nella teoria dei tipi intuizionista, c'è un solo modo per creare termini di =-tipo, ovvero attraverso la riflessività:
È possibile creare =-tipi come , in cui i termini non si riducono allo stesso termine canonico, ma non sarà possibile creare termini di quel tipo. Infatti, se si potesse creare un termine del tipo , si potrebbe anche creare un termine del tipo che, se inserito in una funzione, genererebbe una funzione del tipo . Dal momento che è il modo in cui è definita la negazione, abbiamo che , ovvero .
L'equivalenza delle dimostrazioni è un'area di ricerca attiva in teoria della dimostrazione, e ha portato allo sviluppo della teoria dei tipi omotopica e di altre teorie dei tipi.
Tipi induttivi I tipi induttivi consentono la creazione di tipi complessi e autoreferenziali. Ad esempio, una lista concatenata di numeri naturali è una lista vuota oppure una coppia formata da un numero naturale e un'altra lista concatenata. I tipi induttivi possono essere utilizzati per definire strutture matematiche illimitate come alberi, grafici, ecc. In effetti, il tipo dei numeri naturali può essere definito induttivamente, essendo ogni numero naturale oppure il successore di un altro numero naturale.
I tipi induttivi definiscono nuove costanti, come zero e la funzione successore . Dato che non ha una definizione e non può essere valutata usando la sostituzione, termini come e diventano i termini canonici per i numeri naturali.
Le dimostrazioni sui tipi induttivi sono rese possibili dall'induzione. Ogni tipo induttivo ha una propria regola induttiva. Per dimostrare un predicato per ogni numero naturale , si usa la seguente regola:
I tipi induttivi sono definiti in termini di W-tipi, ovvero gli alberi ben fondati. Successivi lavori nella teoria dei tipi hanno generato i tipi coinduttivi, induzione-ricorsione e induzione-induzione per lavorare su tipi autoreferenziali di natura più oscura. Tipi induttivi di ordine superiore consentono di definire l'uguaglianza tra termini.
Tipi universo I tipi universo consentono di costruire dimostrazioni riguardanti tutti i tipi creati con gli altri costruttori di tipi. Ogni termine nel tipo universo può essere mappato su un tipo creato con qualsiasi combinazione di e il costruttore induttivo. Tuttavia, per evitare paradossi, non vi è alcun termine in che mappa in .
Per costruire dimostrazioni riguardo a tutti i "tipi piccoli" e , devi usare , che contiene un termine per , ma non per sé stesso. In maniera simile, per . Esiste una gerarchia predicativa sugli universi, quindi per quantificare una dimostrazione su una costante fissata di universi, si deve usare .
I tipi universo sono un aspetto complicato delle teorie dei tipi. Infatti, fu necessario modificare la prima versione della teoria per tenere conto del paradosso di Girard. Ricerche successive hanno toccato argomenti come "super-universi", "universi Mahlo" e universi impredicativi.
Giudizi La definizione formale della teoria dei tipi intuizionista è scritta usando giudizi. Ad esempio, nell'affermazione "se è un tipo e è un tipo, allora è un tipo" ci sono i giudizi "è un tipo ", "e" e " se ... allora...". L'espressione non è un giudizio, ma è il tipo che viene definito.
Questo secondo livello della teoria dei tipi può essere fonte di confusione, in particolare per quanto riguarda l'uguaglianza. C'è un giudizio sull'uguaglianza di termini, che potrebbe affermare , ovvero che due termini si riducono allo stesso termine canonico. C'è anche un giudizio sull'uguaglianza di tipi, , stante a significare che ogni elemento di tipo è un elemento di tipo e viceversa. A livello di tipo, esiste un tipo , che contiene termini se esiste una dimostrazione che e si riducono allo stesso valore (ovviamente, termini di questo tipo sono generati usando il giudizio sull'uguaglianza di termini). Infine, esiste un livello di uguaglianza metalinguistico, poiché usiamo la parola "quattro" e il simbolo "" per riferirci al termine canonico . Sinonimi come questi sono chiamati "uguali per definizione" da Martin-Löf.
La descrizione dei giudizi che segue si basa sulla trattazione in Nordström, Petersson e Smith.
La teoria formale lavora con tipi e oggetti.
Un tipo è dichiarato da:
Un oggetto esiste ed è di un tipo se:
Gli oggetti possono essere uguali
e i tipi possono essere uguali
un tipo che dipende da un oggetto di un altro tipo viene dichiarato
e rimosso per sostituzione
, sostituendo la variabile con l'oggetto in .
Un oggetto che dipende da un oggetto di un altro tipo può essere scritto in due modi. Se l'oggetto è "astratto", allora è scritto
e rimosso per sostituzione
, sostituendo la variabile con l'oggetto in .
Un oggetto dipendente da un oggetto può anche essere dichiarato come una costante parte di un tipo ricorsivo. Un esempio di tipo ricorsivo è: