- Teoría de tipos
-
En matemáticas, lógica y ciencias de la computación, la teoría de tipos es cualquiera de varios sistemas formales que pueden servir como alternativas a la teoría informal de conjuntos, o al estudio de tales formalismos en general. En la teoría de lenguajes de programación, una rama de las ciencias de la computación, la teoría de tipos puede referirse al diseño, análisis y estudio de los sistemas de tipos, aunque algunos científicos de la computación limitan el significado del término al estudio de formalismos abstractos como el cálculo lambda tipado.
Historia
Bertrand Russell inventó la primera teoría de tipos en respuesta a su descubrimiento donde la versión de Gottlob Frege de la teoría de conjuntos nativa es afectada por la paradoja de Russell. Este tipo de la teoría de tipos aparece primariamente en el Principia Mathematica de Whitehead y Russell. Esta teoría evita la paradoja de Russell creando una jerarquía de tipos, luego asignando cada entidad matemática a un tipo. Objetos de un tipo dado son creados exclusivamente por objetos de un tipo anterior (aquellos mas abajo en la jerarquía), por lo tanto evitando ciclos.
Alonzo Church, inventor del calculo lambda, desarrolló una lógica de orden superior comúnmente llamada Teoría de Tipos de Church, para evitar la paradoja de Kleen-Rosser afectando el calculo lambda puro original. La teoría de tipos de Church es una variante del calculo lambda en el cual las expresiones (también llamadas formulas o términos lambda) son clasificadas en tipos, y los tipos de expresiones restringen las maneras en que pueden ser combinadas. En otras palabras, es un cálculo lambda tipado. Hoy en día muchos otros cálculos están en uso, incluyendo la Intuisionistica teoría de tipos de Per Martin-Löf, el Sistema F de Jean-Yves Girard y el Cálculo de Construcciones. En el calculo lambda tipado, tipos juegan un papel similar al de los conjuntos en la teoría de conjuntos.
Wikimedia foundation. 2010.
