"Para ser de un (cierto tipo de)" es una relación fundamental de la ontología y de la ciencia de la computación "ontologías" están en el núcleo de la Web Semántica (que es de mi interés). Pero yo no encuentro un tratamiento matemático de los tipos. El "tipo de teoría" de las Nuevas Fundaciones a mí me parece que una "teoría de conjuntos", porque no veo nada en sus axiomas que sería indicio de un tratamiento de tipos tan diferentes de las colecciones. Puede alguien por favor elaborar sobre esto?
Respuesta
¿Demasiados anuncios?
sleske
Puntos
5824
Sí, hay un rico campo de la matemática tratamientos de tipos, en el sentido de los lenguajes de programación. Sin embargo, las Nuevas Fundaciones y Russell anteriores de las teorías de los tipos son muy atípico de lo que ahora es conocido generalmente como el Tipo de Teoría.
Un buen lugar para comenzar es con algo como la escribió λ-cálculos de la Iglesia y otros. Estos pueden ser exactamente visto como un mínimo de lenguajes de programación, y seria modernos lenguajes de programación funcional como Haskell y OCaml (y familiares) se basan muy de cerca en más elaboradas versiones de estos, con un montón de azúcar sintáctico y listo extensiones de tipo agregado.
Por otro lado, uno puede elaborar en este tipo de sistemas en diferentes direcciones para analizar cómo los tipos de datos de trabajo en más pragmáticamente diseñado lenguajes (C, Java, etc.).
En todos estos, sin embargo, la diferencia de la teoría de conjuntos no es tanto en qué tipos son visto como - en la mayoría de los sistemas de tipo sé, todavía son vistos esencialmente como algo abstracto colecciones. Hay dos diferencias principales con la teoría de conjuntos:
-
las operaciones previstas para la construcción de tipos y elementos de los tipos suelen ser muy concretas y constructivas, y el espejo familiar construcciones disponible en los lenguajes de programación.
Por ejemplo, un tipo de teoría, bien puede tener un básico de la construcción que, para un tipo de Una, proporciona un tipo de Lista de Unade las listas de elementos de Una.
-
en (la mayoría de) conjunto de teorías, los conjuntos son colecciones de un ambiente universo de los conjuntos, todo es un conjunto, puede ser un elemento de cualquier otro conjunto, y el "ser-un-elemento-de" es una relación, una propiedad con un valor de verdad. En la mayoría de los tipos de teorías, de los tipos no son subcolecciones de algunos ambiental de la colección son independientes de las colecciones de elementos.
Así, en la teoría de conjuntos, una declaración "para cada número primo $p$, ..." oficialmente significa "para todos los $p$ si $p$ es un número y $p$ es primo, entonces..." - por lo que el cuantificador permite, por ejemplo, $\mathbb{R}$ como un valor válido para $p$! En el tipo de teoría, sería formalmente convertido "para cada número $p$ si $p$ es primo entonces ..." - primeness puede ser una propiedad, pero al ser un número es el tipo básico de la cosa p es declarado tan pronto como se considera. Cada objeto que alguna vez hablar de algún tipo. Usted no puede (dentro del lenguaje de la teoría), tome el número 100, y luego preguntar "es 100 una cadena?" - ser de un tipo que no es una propiedad, es una declaración que se hace cuando una variable se introduce, o eso dedujo por un término derivado como (n+5). En la práctica, términos de programación, más o menos, dice que las implementaciones de los objetos están bien sellados abstracciones: una aplicación puede utilizar la misma base de la representación de un número entero y una cadena, pero el lenguaje sólo puede acceder a ellos como un entero y una cadena. (Por supuesto, el tipo de sistemas que están diseñados específicamente para cerca los modelos existentes de idiomas puede tirar tales abstracciones.)
Hay un montón de buenas introducciones a la teoría tipo por ahí. La página de la Wikipedia da un buen comienzo; para un importante libro sobre el tipo de teoría a partir de una lenguajes de programación punto de vista, que te llevará tan lejos como usted necesita ir, recomiendo Bob Harper Prácticos fundamentos de lenguajes de programación, disponible en formato pdf desde su página web. Él es muy testarudo y sus más polémicas declaraciones deben ser tomadas con un gran grano de sal, pero él es un fantástico escritor, con un hermoso mirador en el campo.
