En lógica y ciencias de la computación, una teoría de tipos dependientes es una teoría de tipos que incluye tipos dependientes, es decir, tipos que dependen de ciertos valores o términos de otros tipos. En algunas teorías de tipos, como la de Martin-Löf, estos tipos pueden usarse para definir cuantificadores universales y existenciales según la Correspondencia de Curry-Howard.
Formalmente, si introducimos una noción de universos de tipos a la forma de Russell y tenemos un universo de tipos tal que , entonces podemos definir una familia de tipos dependientes tal que asigna a cada un tipo . Si, por el otro lado, estos universos no existen, estos juicios pueden hacerse mediante juicios de tipado, , pero no se interpreta como un tipo.
Tipos de suma y producto
El tipo Π De una familia de tipos podemos construir el tipo de funciones dependientes, o tipo de producto dependiente, cuyos términos son funciones que toman un término y devuelven un término .
Estos tipos pueden verse como un producto cartesiano de tipos. Los tipos Π también pueden entenderse como cuantificadores universales, así que puede entenderse como .
Tipo Σ El dual del tipo de producto dependiente es el tipo de par dependiente, o de suma dependiente. Para todo tipo y familia de tipos existe el tipo .
Un término de este tipo es un par (a,b) tal que y , es decir, un habitante del tipo cuando sustituimos a por . Estos tipos pueden entenderse también como cuantificadores existenciales tal que significa .
Teoría de Tipos Intuicionista o de Martin-Löf La teoría de tipos intuicionista fue creada por Per Martin-Löf, matemático y filósofo sueco, quien la publicó por primera vez en 1975. Martin-Löf diseñó la teoría de tipos basándose en los principios del constructivismo matemático. Según este constructivismo, la verdad de una proposición depende de que tenga un "certificado" o demostración de su verdad, hecho que puede formalizarse en teoría de tipos dependientes según la Correspondencia de Curry-Howard. Una consecuencia útil es que las pruebas se convierten en objetos matemáticos que pueden examinarse, compararse y manipularse.
En esta teoría de tipos dependientes se considera además un tipo identidad para dos términos de un tipo , denotado por . También tenemos el juicio metateorético: que afirma que ambos términos son exactamente el mismo término. La identidad no necesariamente debe interpretarse de esta forma. Por ejemplo, en el modelo homotópico de Steve Awodey y Michael Warren usado en teoría homotópica de tipos, se interpreta como un camino entre dos puntos de un espacio, .
Referencias
Categoría:Métodos formales Categoría:Teoría de tipos