Bertrand Russell inventó la primera teoría de tipos en respuesta a su descubrimiento de que la versión de Gottlob Frege de la teoría ingenua de conjuntos 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 más abajo en la jerarquía), por lo tanto evitando ciclos.
Alonzo Church, inventor del cálculo lambda, desarrolló una lógica de orden superior comúnmente llamada Teoría de Tipos de Church,[2] para evitar la paradoja de Kleen-Rosser que afectaba al cálculo lambda puro original. La teoría de tipos de Church es una variante del cálculo lambda en el cual las expresiones (también llamadas fórmulas 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 teoría de tipos intuicionista de Per Martin-Löf, el Sistema F de Jean-Yves Girard y el Cálculo de Construcciones. En el cálculo lambda tipado, los tipos juegan un papel similar al de los conjuntos en la teoría de conjuntos.
Referencias
William M. Farmer, The Seven Virtues of Simple Type Theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.
Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
Datos:Q1056428
Multimedia:Type theory / Q1056428
Enero 29, 2023
teoría, tipos, este, artículo, sección, tiene, referencias, pero, necesita, más, para, complementar, verificabilidad, este, aviso, puesto, octubre, 2017, matemáticas, lógica, ciencias, computación, teoría, tipos, cualquiera, varios, sistemas, formales, pueden,. Este articulo o seccion tiene referencias pero necesita mas para complementar su verificabilidad Este aviso fue puesto el 9 de octubre de 2017 En matematicas logica y ciencias de la computacion la teoria de tipos es cualquiera de varios sistemas formales que pueden servir como alternativas a la teoria de conjuntos como fundamento de las matematicas constructivas o al estudio de tales formalismos en general 1 En la teoria de lenguajes de programacion una rama de las ciencias de la computacion la teoria de tipos puede referirse al diseno analisis y estudio de los sistemas de tipos aunque algunos teoricos de la computacion limitan el significado del termino al estudio de formalismos abstractos como el calculo lambda tipado Historia EditarBertrand Russell invento la primera teoria de tipos en respuesta a su descubrimiento de que la version de Gottlob Frege de la teoria ingenua de conjuntos es afectada por la paradoja de Russell Este tipo de la teoria de tipos aparece primariamente en el Principia Mathematica de Whitehead y Russell Esta teoria evita la paradoja de Russell creando una jerarquia de tipos luego asignando cada entidad matematica a un tipo Objetos de un tipo dado son creados exclusivamente por objetos de un tipo anterior aquellos mas abajo en la jerarquia por lo tanto evitando ciclos Alonzo Church inventor del calculo lambda desarrollo una logica de orden superior comunmente llamada Teoria de Tipos de Church 2 para evitar la paradoja de Kleen Rosser que afectaba al calculo lambda puro original La teoria de tipos de Church es una variante del calculo lambda en el cual las expresiones tambien llamadas formulas o terminos lambda son clasificadas en tipos y los tipos de expresiones restringen las maneras en que pueden ser combinadas En otras palabras es un calculo lambda tipado Hoy en dia muchos otros calculos estan en uso incluyendo la teoria de tipos intuicionista de Per Martin Lof el Sistema F de Jean Yves Girard y el Calculo de Construcciones En el calculo lambda tipado los tipos juegan un papel similar al de los conjuntos en la teoria de conjuntos Referencias Editar William M Farmer The Seven Virtues of Simple Type Theory Journal of Applied Logic Vol 6 No 3 September 2008 pp 267 286 Alonzo Church A formulation of the simple theory of types The Journal of Symbolic Logic 5 2 56 68 1940 Datos Q1056428 Multimedia Type theory Q1056428 Obtenido de https es wikipedia org w index php title Teoria de tipos amp oldid 124394516, wikipedia, wiki, leyendo, leer, libro, biblioteca,
