Teoria de Tipos Depenents

En llògica i ciències de la computació, una teoria de tipos depenents és una teoria de tipos que inclou tipos depenents, és dir, tipos que depenen de certs valors o térmens d'atres tipos. En algunes teories de tipos, com la de Martin-Löf, estos tipos poden usar-se per a definir quantificadors universals i existencials segons la Correspondència de Curry-Howard.

Formalment, si introduïm una noció de univers de tipos a la forma de Russell i tenim un univers de tipos $U_i$ tal que $A:{𝒰}_{𝒾}$, llavors podem definir una família de tipos depenents $B:A\to {𝒰}_{𝒾}$ tal que assigna a cada $a:A$ un tipo $B(a):{𝒰}_{𝒾}$. Si, per l'atre costat, estos univers no existixen, estos juïns poden fer-se per mig de juïns de tipado, $A:Type$, pero $Type$ no s'interpreta com un tipo.

Tipos de suma i producte

El tipo Π

D'una família de tipos $B:A\to 𝒰$ podem construir el tipo de funcions depenents, o tipo de producte depenent, $\prod _{x:A}B(x)$ els térmens del qual són funcions que prenen un terme $a:A$ i tornen un terme $B(a)$.

Estos tipos poden vore's com un producte cartesiano de tipos. Els tipos Π també poden entendre's com quantificadors universals, aixina que $\prod _{x:A}B(x)$ pot entendre's com $\mathrm{\forall }x:A.B(x)$.

Tipo Σ

El dual del tipo de producte depenent és el tipo de parell depenent, o de suma depenent. Per a tot tipo $A:𝒰$ i família de tipos $B:A\to 𝒰$ existix el tipo $\sum _{x:A}B(x)$.

Un terme d'este tipo és un parell (a,b) tal que $a:A$ i $b:B[a/x]$, és dir, un habitant del tipo $B(x)$ quan substituïm a $x:A$ per $a:A$. Estos tipos poden entendre's també com quantificadors existencials tal que $\sum _{x:A}B(x)$ significa $\mathrm{\exists }x:A.B(x)$.

Teoria de Tipos Intuicionista o de Martin-Löf

La teoria de tipos intuicionista va ser creada per Per Martin-Löf, matemàtic i filòsof suec, qui la va publicar per primera volta en 1975. Martin-Löf va dissenyar la teoria de tipos basant-se en els principis del constructivisme matemàtic. Segons este constructivisme, la veritat d'una proposició depén de que tinga un "certificat" o demostració de la seua veritat, fet que pot formalisar-se en teoria de tipos depenents segons la Correspondència de Curry-Howard. Una conseqüència útil és que les proves es convertixen en objectes matemàtics que poden examinar-se, comparar-se i manipular-se.

En esta teoria de tipos depenents es considera ademés un tipo identitat per a dos térmens d'un tipo $A$, denotat per $i{d}_A(a,b)$. També tenim el juí metateorético: $a\equiv b$ que afirma que abdós térmens són exactament el mateix terme. L'identitat $i{d}_A(a,b)$ no necessàriament deu interpretar-se d'esta forma. Per eixemple, en el model homotópico de Steve Awodey i Michael Warren usat en teoria homotópica de tipos, $i{d}_A(a,b)$ s'interpreta com un camí entre dos punts d'un espai, $a,b:A$.