Teoria dei tipi intuizionista

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 ($A\implies B$) corrisponde al tipo funzione ($A\mapsto B$). 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 $2+2$ e $2\cdot 2$ 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 $\bot$ e rappresenta proposizioni refutabili (ovvero, per le quali non può esistere una dimostrazione). Di conseguenza, la negazione è definita come una funzione in $\bot$: $\neg A\ {\overset {\underset {\mathrm {def} }{}}{=}}\ A\mapsto \bot$ .

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 $\top$.

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 ($A\times B$) di altri due tipi, $A$ e $B$. Logicamente, una tale coppia ordinata avrebbe una prova di $A$ e una prova di $B$, quindi si può vedere un Σ-tipo scritto come $A\wedge B$.

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ì:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

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 ${\mathbb {N} }\times {\mathbb {R} }$ è scritto come:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }$

È importante notare che il valore del primo termine, $n$, non dipende dal tipo del secondo termine, ${\mathbb {R} }$.

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:

$\sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}$

La tipizzazione dipendente consente ai Σ-tipi di svolgere il ruolo di quantificatore esistenziale. L'affermazione "esiste un $n$ di tipo $\mathbb {N}$, tale che $P(n)$ è dimostrato" diventa il tipo di coppie ordinate in cui il primo termine è il valore $n$ e il secondo è una dimostrazione di $P(n)$. Si noti che il tipo del secondo termine (dimostrazioni di $P(n)$) dipende dal valore del primo elemento ($n$). Il suo tipo è:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

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 $n$, restituisce un vettore contenente $n$ numeri reali, è scritto come:

$\prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

Quando il tipo di output non dipende dal valore in input, la funzione viene spesso scritta semplicemente con un $\mapsto$ . Così, $\mathbb {N} \mapsto \mathbb {R}$ è il tipo di funzioni dai numeri naturali ai numeri reali. I Π-tipi corrispondono all'implicazione logica. La proposizione $A\implies B$ corrisponde al tipo $A\mapsto B$, contenente funzioni che accettano dimostrazioni di A e restituiscono dimostrazioni di B. Questo tipo potrebbe essere scritto in modo più coerente come:

$\prod _{a{\mathbin {:}}A}B$

I Π-tipi sono anche usati in logica per la quantificazione universale. L'affermazione "per ogni $n$ di tipo ${\mathbb {N} }$, $P(n)$ è dimostrato" diventa una funzione da $n$ alle dimostrazioni di $P(n)$. Quindi, dato un valore ad $n$, la funzione genera una prova che $P(n)$ vale per quel valore. Il tipo si scrive come:

$\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

Costruttore =

Gli =-tipi vengono creati con due termini. Dati due termini come $2+2$ e $2\cdot 2$, si può creare un nuovo tipo $2+2=2\cdot 2$. I termini del nuovo tipo dimostrano che la coppia si riduce allo stesso termine canonico. Quindi, dal momento che entrambi $2+2$ e $2\cdot 2$ si riducono al termine canonico $4$, ci sarà un termine del tipo $2+2=2\cdot 2$. Nella teoria dei tipi intuizionista, c'è un solo modo per creare termini di =-tipo, ovvero attraverso la riflessività:

$\operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).$

È possibile creare =-tipi come $1=2$, 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 $1=2$, si potrebbe anche creare un termine del tipo $\bot$ che, se inserito in una funzione, genererebbe una funzione del tipo $1=2\to \bot$. Dal momento che $\ldots \to \bot$ è il modo in cui è definita la negazione, abbiamo che $\neg (1=2)$, ovvero $1\neq 2$.

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 $0$ oppure il successore di un altro numero naturale.

I tipi induttivi definiscono nuove costanti, come zero $0:\mathbb {N}$ e la funzione successore $S:\mathbb {N} \mapsto \mathbb {N}$ . Dato che $S$ non ha una definizione e non può essere valutata usando la sostituzione, termini come $S(0)$ e $S(S(S(0)))$ 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 $P(n)$ per ogni numero naturale $n$, si usa la seguente regola:

$\mathbb {N} {\text{-elim}}:P(0)\mapsto \left(\prod _{n:\mathbb {N} }P(n)\mapsto P(S(n))\right)\mapsto \prod _{n:\mathbb {N} }P(n)$

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 ${\mathcal {U}}_{0}$ può essere mappato su un tipo creato con qualsiasi combinazione di $0,1,2,\Sigma ,\Pi ,=$ e il costruttore induttivo. Tuttavia, per evitare paradossi, non vi è alcun termine in ${\mathcal {U}}_{0}$ che mappa in ${\mathcal {U}}_{0}$.

Per costruire dimostrazioni riguardo tutti i "tipi piccoli" e ${\mathcal {U}}_{0}$, devi usare ${\mathcal {U}}_{1}$, che contiene un termine per ${\mathcal {U}}_{0}$, ma non per sé stesso. In maniera simile, per ${\mathcal {U}}_{2}$. Esiste una gerarchia predicativa sugli universi, quindi per quantificare una dimostrazione su una costante $k$ fissata di universi, si deve usare ${\mathcal {U}}_{k+1}$.

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 $A$ è un tipo e $B$ è un tipo, allora $\textstyle \sum _{a:A}B$ è un tipo" ci sono i giudizi "è un tipo ", "e" e " se ... allora...". L'espressione $\textstyle \sum _{a:A}B$ 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 $4=2+2$, ovvero che due termini si riducono allo stesso termine canonico. C'è anche un giudizio sull'uguaglianza di tipi, $A=B$, stante a significare che ogni elemento di tipo $A$ è un elemento di tipo $B$ e viceversa. A livello di tipo, esiste un tipo $4=2+2$, che contiene termini se esiste una dimostrazione che $4$ e $2+2$ 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 "$4$" per riferirci al termine canonico $S(S(S(S(0))))$. 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:

• $A\ {\mathsf {Type}}$

Un oggetto esiste ed è di un tipo se:

• $a{\mathbin {:}}A$

Gli oggetti possono essere uguali

• $a=b$

e i tipi possono essere uguali

• $A=B$

un tipo che dipende da un oggetto di un altro tipo viene dichiarato

• $(x{\mathbin {:}}A)B$

e rimosso per sostituzione

• $B[x/a]$, sostituendo la variabile $x$ con l'oggetto $a$ in $B$.

Un oggetto che dipende da un oggetto di un altro tipo può essere scritto in due modi. Se l'oggetto è "astratto", allora è scritto

• $[x]b$

e rimosso per sostituzione

• $b[x/a]$, sostituendo la variabile $x$ con l'oggetto $a$ in $b$.

Un oggetto dipendente da un oggetto può anche essere dichiarato come una costante parte di un tipo ricorsivo. Un esempio di tipo ricorsivo è:

• $0{\mathbin {:}}\mathbb {N}$
• $S{\mathbin {:}}\mathbb {N} \to \mathbb {N}$

Qui, $S$ è un oggetto dipendente da un oggetto costante. Non è associato a un'astrazione. Le costanti come $S$ possono essere rimosse definendo delle uguaglianze. Qui, la relazione con l'addizione è definita usando l'uguaglianza e il pattern matching per gestire la natura ricorsiva di $S$:

${\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}$

$S$ è manipolato come una costante opaca, non ha una struttura interna per la sostituzione.

Quindi, oggetti, tipi e relazioni sono usati per esprimere formule della teoria. Per creare nuovi oggetti, tipi e relazioni da quelli esistenti vengono utilizzati i seguenti stili di giudizi:

$\Gamma \vdash \sigma \ {\mathsf {Tipo}}$	σ è un tipo ben formato nel contesto Γ.
$\Gamma \vdash t{\mathbin {:}}\sigma$	t è un termine ben formato di tipo σ nel contesto Γ.
$\Gamma \vdash \sigma \equiv \tau$	σ e τ sono tipi uguali nel contesto Γ.
$\Gamma \vdash t\equiv u{\mathbin {:}}\sigma$	't e u' sono termini uguali di tipo σ nel contesto Γ.
$\vdash \Gamma \ {\mathsf {Contesto}}$	Γ è un contesto ben formato dei presupposti di tipizzazione.

Per convenzione, esiste un tipo che rappresenta tutti gli altri tipi. È chiamato ${\mathcal {U}}$ (o $\operatorname {Set}$). Dato che ${\mathcal {U}}$ è un tipo, i suoi membri sono oggetti. C'è un tipo dipendente $\operatorname {El}$ che associa ciascun oggetto al tipo corrispondente. Nella maggior parte dei testi $\operatorname {El}$ non è mai scritto. Dal contesto, un lettore può quasi sempre distinguere se $A$ si riferisce a un tipo o se si riferisce all'oggetto in ${\mathcal {U}}$ che corrisponde al tipo.

Questa è la base completa della teoria. Tutto il resto è derivato.

Per implementare la logica, ogni proposizione ha il suo tipo. Gli oggetti in questi tipi rappresentano i possibili modi diversi per dimostrare la proposizione. Ovviamente, se non ci sono dimostrazioni per la proposizione, allora il tipo non contiene oggetti. Operatori come "e" e "o", lavorando su proposizioni, introducono nuovi tipi e nuovi oggetti. Così, $A\times B$ è un tipo che dipende dal tipo $A$ e dal tipo $B$. Gli oggetti di quel tipo dipendente sono definiti per esistere per ogni coppia di oggetti di $A$ e di $B$. Ovviamente, se $A$ o $B$ sono tipi vuoti, allora il nuovo tipo che rappresenta $A\times B$ è anch'esso vuoto.

Ciò può essere fatto per altri tipi (booleani, numeri naturali, ecc.) e per i loro operatori.

Modelli categorici della teoria dei tipi

Utilizzando il linguaggio della teoria delle categorie, R. A. G. Seely ha introdotto la nozione di categoria locale cartesiana chiusa (CLCC) come modello base della teoria dei tipi. Questo è stato perfezionato da Hofmann e Dybjer in Categorie con Famiglie o Categorie con Attributi basati su precedenti lavori di Cartmell.

Una categoria con famiglie è una categoria C di contesti (in cui gli oggetti sono contesti e i morfismi di contesto sono sostituzioni), insieme a un funtore $a$.

${\text{Fam(Set)}}$ è la categoria delle famiglie di insiemi, in cui gli oggetti sono coppie $(A,B)$ formate da un "insieme indice" $A$ e da una funzione $B:X\mapsto A$, e i morfismi sono coppie di funzioni $f:A\mapsto A'$ e $g:X\mapsto X'$, tali che $B'\circ g=f\circ B$ — in altre parole, $f$ mappa $B_{a}$ in $B_{a}$.

Il funtore $T$ assegna a un contesto $G$ un insieme di tipi $Ty(G)$ e, per ogni $A:Ty(G)$, un insieme di termini $Tm(G,A)$. Gli assiomi di un funtore richiedono che questi siano in sinergia con la sostituzione. La sostituzione è solitamente scritta nella forma $Af$ o $af$, dove $A$ è un tipo in $Ty(G)$, $a$ è un termine in $Tm(G,A)$ e $f$ è una sostituzione da $D$ a $G$. Qui $Af:Ty(D)$ e $af:Tm(D,Af)$.

La categoria $C$ deve contenere un oggetto terminale (il contesto vuoto) e un oggetto finale per una forma di prodotto chiamata comprensione, o estensione del contesto, in cui l'elemento destro è un tipo nel contesto dell'elemento sinistro. Se $G$ è un contesto e $A:Ty(G)$, allora dovrebbe esserci un oggetto finale $(G,A)$ tra contesti $D$ con mappature $p:D\mapsto G$, $q:Tm(D,Ap)$.

Una struttura logica come quella di Martin-Löf assume la forma di condizioni di chiusura su insiemi di tipi e termini dipendenti dal contesto: dovrebbe esistere un tipo per ogni insieme e uno chiamato $\operatorname {Set}$, inoltre i tipi dovrebbero essere chiusi rispetto a forme di somma e prodotto dipendenti, e così via.

Una teoria come quella degli insiemi predicativa esprime le condizioni di chiusura sui tipi di insiemi e sui loro elementi: dovrebbero essere chiusi rispetto a operazioni che riflettono la somma e il prodotto dipendenti e rispetto a varie forme di definizione induttiva.

Estensionale versus intensionale

Una distinzione fondamentale è la teoria dei tipi estensionale rispetto a quella intensionale. In quella estensionale, l'uguaglianza per definizione (cioè computazionale) non è distinta dall'equivalenza logica, che richiede una dimostrazione. Di conseguenza, il sistema dei tipi è indecidibile nella teoria dei tipi estensionale, perché i programmi nella teoria potrebbero non terminare. Ad esempio, tale teoria consente di dare un tipo all'Y-combinatore, un esempio dettagliato di ciò può essere trovato in Programming in Martin-Löf's Type Theory di Nordstöm e Petersson. Tuttavia, ciò non impedisce alla teoria dei tipi estensionale di essere una base per uno strumento pratico, ad esempio NuPRL si basa su tale teoria. Da un punto di vista pratico, non c'è differenza tra un programma che non termina e un programma che impiega un milione di anni per terminare.

Al contrario, nella teoria dei tipi intensionale il sistema dei tipi è decidibile, ma la rappresentazione di concetti matematici standard è un po' più ingombrante, poiché il ragionamento intensionale richiede l'uso di insiemi estensionali o costruzioni simili. Esistono molti oggetti matematici comuni con cui è difficile lavorare o che non possono essere rappresentati senza di essi, ad esempio numeri interi, numeri razionali e numeri reali. Numeri interi e numeri razionali possono essere rappresentati senza usare insiemi estensionali, ma questa rappresentazione non è facile da maneggiare. I numeri reali di Cauchy non possono essere rappresentati senza di essi.

La teoria dei tipi omotopica si occupa di risolvere questo problema. Permette di definire tipi induttivi di ordine superiore, che non solo definiscono costruttori del primo ordine (valori o punti), ma costruttori di ordine superiore, cioè uguaglianze tra elementi (archi), uguaglianze tra uguaglianze (omotopie), all'infinito.

Implementazioni

Diverse forme di teoria dei tipi sono state implementate come sistemi formali alla base di numerosi assistenti alla dimostrazione. Mentre molti sono basati sulle idee di Per Martin-Löf, altri hanno aggiunto funzionalità, più assiomi o diversi background filosofici. Ad esempio, il sistema NuPRL si basa sulla teoria dei tipi computazionale e Coq si basa sul calcolo delle costruzioni (co)induttive . I tipi dipendenti caratterizzano anche la progettazione di linguaggi di programmazione come ATS, Cayenne, Epigram, Agda e Idris.

Teorie dei tipi di Martin-Löf

Per Martin-Löf costruì diverse teorie dei tipi che furono pubblicate varie volte, alcune delle quali molto più tardi che le prestampe con la loro descrizione divennero accessibili agli specialisti (tra cui Jean-Yves Girard e Giovanni Sambin). Il seguente elenco tenta di elencare tutte le teorie che sono state descritte in forma stampata e di delineare le caratteristiche chiave che le hanno distinte tra loro. Tutte queste teorie avevano prodotti dipendenti, somme dipendenti, unioni disgiunte, tipi finiti e numeri naturali. Tutte le teorie avevano le stesse regole di riduzione, che non includevano la η-riduzione, né per i prodotti né per le somme dipendenti, fatta eccezione per MLTT79, in cui viene aggiunta la η-riduzione per i prodotti dipendenti.

MLTT71 è stata la prima teoria dei tipi creata da Per Martin-Löf. È apparsa in una prestampa nel 1971. Aveva un universo, ma questo universo conteneva il proprio nome al suo interno, ovvero era una teoria dei tipi con un "tipo nel tipo", come viene chiamato oggi. Jean-Yves Girard ha dimostrato che questo sistema era incoerente e la prestampa non è mai stata pubblicata.

MLTT72 è stata presentata in una prestampa del 1972, ora pubblicata. Questa teoria aveva un universo V e nessun tipo identità. L'universo era "predicativo", nel senso che il prodotto dipendente di una famiglia di oggetti da V su un oggetto che non era in V, come ad esempio V stesso, non si considerava essere in V. L'universo era alla Russell, cioè, si scriveva direttamente "T∈V" e "t∈T" (Martin-Löf usa il segno "∈" invece del moderno ":"), senza il costruttore aggiuntivo "El".

MLTT73 fu la prima definizione di teoria dei tipi pubblicata da Per Martin-Löf (fu presentata al Logic Colloquium 73 e pubblicata nel 1975). Esistono tipi identità che egli chiama "proposizioni", ma poiché non viene introdotta alcuna reale distinzione tra proposizioni e il resto dei tipi, il significato di ciò non è chiaro. È presente ciò che in seguito acquisisce il nome di J-eliminatore, ma ancora senza un nome (vedi pp. 94–95). C'è inoltre una sequenza infinita di universi V₀, ..., V_n, ... . Gli universi sono predicativi, alla Russell e non cumulativi! Infatti, il corollario 3.10 a pag. 115 dice che se A∈V_m e B∈V_n sono tali che A e B sono convertibili, allora m = n. Ciò significa, ad esempio, che sarebbe difficile formulare l'univalenza in questa teoria - ci sono tipi riducibili in ciascuno dei V_i, ma non è chiaro come dichiararli uguali, poiché non ci sono tipi identità che collegano V_i e V_j per i ≠ j.

MLTT79 fu presentata nel 1979 e pubblicata nel 1982. In questo articolo, Martin-Löf ha introdotto i quattro tipi base di giudizi per la teoria dei tipi dipendenti, che da allora è diventata fondamentale nello studio della meta-teoria di tali sistemi. Ha anche introdotto i contesti come un concetto separato (vedi p. 161). Ci sono tipi identità con il J-eliminatore (che era già apparso in MLTT73, ma senza avere questo nome), ma anche con la regola che rende la teoria "estensionale" (p. 169). Sono presenti anche i W-tipi e una sequenza infinita di universi predicativi che sono cumulativi.

Bibliopolis C'è una discussione su una teoria dei tipi nel libro Bibliopolis del 1984, ma è in qualche modo non ben specificata e non sembra rappresentare un particolare insieme di scelte, quindi non vi è alcuna specifica teoria dei tipi ad essa associata.

Bibliografia

• Per Martin-Löf, Intuitionistic type theory (PDF), Sambin, Giovanni, Napoli, Bibliopolis, 1984, ISBN 978-88-7088-105-9, OCLC 12731401.
• Per Martin-Löf's Notes, as recorded by Giovanni Sambin (1980)
• Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory, Oxford University Press, 1990, ISBN 978-0-19-853814-1.
• Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991, ISBN 0-201-41667-0.
• Johan G. Granström, Treatise on Intuitionistic Type Theory, Springer, 2011, ISBN 978-94-007-1735-0.
• Note di Per Martin-Löf, registrato da Giovanni Sambin (1980)
• Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory, Oxford University Press, 1990, ISBN 978-0-19-853814-1. Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory, Oxford University Press, 1990, ISBN 978-0-19-853814-1. Bengt Nordström, Kent Petersson e Jan M. Smith, Programming in Martin-Löf's Type Theory, Oxford University Press, 1990, ISBN 978-0-19-853814-1.
• Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991, ISBN 0-201-41667-0. Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991, ISBN 0-201-41667-0. Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991, ISBN 0-201-41667-0.
• Johan G. Granström, Treatise on Intuitionistic Type Theory, Springer, 2011, ISBN 978-94-007-1735-0. Johan G. Granström, Treatise on Intuitionistic Type Theory, Springer, 2011, ISBN 978-94-007-1735-0. Johan G. Granström, Treatise on Intuitionistic Type Theory, Springer, 2011, ISBN 978-94-007-1735-0.

Voci correlate

• Logica Intuizionista
• Lambda calcolo tipizzato

Collegamenti esterni

• EU Types Project: Tutorials - appunti e diapositive della Types Summer School 2005
• n-Categories - Sketch of a Definition - lettera di John Baez e James Dolan a Ross Street, 29 novembre 1995