En términos de la lógica matemática alguien puede darme una definición de la palabra "tipo", junto con un par de ejemplos de la palabra que se utiliza.
El libro que estoy leyendo lo define como un "representante de las inscripciones que tienen el mismo aspecto y las expresiones que suenan igual", me parece que este tipo de vaga, y no puedo entender la definición dada por wikipedia.
Buscando en la página 3 del libro vinculado, el autor es el uso de "tipo" en el sentido filosófico, no en el sentido matemático. Este "tipo de token de distinción" es un tema que llama mucho la atención en la filosofía, pero la mayoría de los libros sobre lógica matemática no hablar de ello, porque se puede conseguir por mucho tiempo sin tener que preocuparse mucho acerca de ella, y porque el tiempo que se tarda para discutir adecuadamente llevaría tiempo y energía de las matemáticas.
La idea general es que hay algunos de la colección de abstracto "tipos" de las cosas. Por ejemplo, hay un tipo de "bicicletas" y un tipo de "manzanas". Entonces no son específicos de bicicletas - cada uno de los cuales es un "símbolo" del tipo de bicicletas, y no son específicos de las manzanas, que son símbolos del tipo de "manzanas". Esto debe de sonido vagamente como algo de Platón.
Del mismo modo, existe un tipo de "la cadena 101". Cada vez que escribo "101", me anote sólo un token de la cadena. Así, 101, 101 y 101 son tres diferentes muestras de la misma cadena.
En la filosofía, la pregunta "¿qué es un tipo, realmente?" ha recibido una gran cantidad de discusión, como se podría imaginar. Pero esa pregunta no es particularmente importante para el estudio directo de las matemáticas, podemos hacer una gran cantidad de matemáticas sin preocuparse por ella.
Un lugar en el que el type/token distinción que hace surgir en lógica con las ocurrencias de las variables. Consideremos la oración, de la lógica de primer orden $$ R(x) \de la tierra (\exists x) [P(x)] $$ Aquí sólo hay una variable "x", de modo que una variable es de un tipo. Hay dos ocurrencias (tokens) de la variable, aunque (tres si contamos "$(\exists x)$"). Uno de ellos es en el ámbito de un cuantificador, y la otra no. Esta distinción entre "variables" y "ocurrencias de las variables" es muy importante para entender el concepto de libertad y variables vinculadas.
En el campo de tipo de teoría (y la programación de la computadora) es algo relacionado con la idea de que el tipo de una variable. En estos sistemas, cada variable tiene un tipo asociado con él, y el tipo de la variable que dicta lo que se puede hacer con la variable. Por ejemplo, en un sistema que tiene un tipo de números naturales y un tipo de conjuntos de números naturales. Si tengo dos números, me pueden agregar. Si tengo un número y un set, me puede preguntar si el número es un elemento del conjunto. Pero, en este escrito el sistema, no puedo agregar dos conjuntos o preguntar si un número es un elemento de otro número, porque esas operaciones no coinciden los tipos. La mayoría de la lógica de primer orden se realiza en un no-escribió manera (tan sólo hay un tipo de variable).
Así que usted necesita preocuparse por el tipo de token de distinción para la lógica proposicional como el aprendizaje de los estudiantes por primera vez? Si usted está interesado en los aspectos filosóficos de la materia, entonces usted sin duda lo hacen. Si usted está interesado sólo en la pura relaciones matemáticas entre las fórmulas de la lógica, y menos sobre las aplicaciones de la lógica a la filosofía, entonces usted puede ser capaz de obtener, ya que muchos de los textos de hacer, con un poco de sentido común, pero de lo contrario no pasar demasiado tiempo en distinguir los tipos de tokens.
Creo que el autor puede referirse a un concepto ontológico de tipo de token. Tal vez usted podría encontrar más información en este enlace.
En lenguajes como C o Haskell, sólo está permitido para realizar las operaciones que tengan sentido para el tipo. Por lo tanto, puede anexar una carta a una cadena de letras "hola"+ " s " ="holas", pero a menos que definir lo que significa, usted no será capaz de añadir 's' a un número, y, de hecho, usted no puede esperar a + a llevar a la semántica de anexar algo.
El modelo de la teoría de la versión de un tipo que es esencialmente un pato sistema de escritura, como en Ruby - si se parece a una cadena, y se pueden concatenar cadenas como una cadena, entonces es una cadena. Para hacer esto usted necesita una manera de construir un tipo de conjunto de comportamientos, que se implementa como un conjunto de primer orden fórmulas.
EDIT: he pensado en una programación de metáfora para el tipo de token de distinción, así.
La programación orientada a objetos se basa en la definición de las clases, que son tipos que en la anterior sentidos de la palabra, para utilizar como una plantilla para la creación de tokens de ese tipo. Por ejemplo, en los juegos donde muchos de los mismos enemigo puede existir a la vez, se podría definir una clase para que el enemigo y crear instancias de ella muchas veces, creando así muchos enemigos, todos del mismo tipo. Pero la diferencia entre el tipo y las fichas es que uno puede tener el tipo "string", y una cadena real, como "hola mundo" y marque el tipo de "hola mundo", no el símbolo en sí, cuando asegurándose de que no se establezca una posición del carácter en el espacio de "hola mundo". Lo mismo va para la eliminación de todas las (fichas) de un tipo de enemigo del juego - que no elimina el tipo del juego.
En realidad, el centro de la lógica, donde la noción de tipo está presente es el reino de orden superior de la lógica, ya que estas lógicas son generalmente desarrollados como extensiones de tipo de teorías (que no necesita ser lógicas). En este orden superior de tipos de contexto son intuitivamente se entiende mejor como tipo de expresiones interpretables, que determinan el tipo de semántica de los objetos asignados a las expresiones de este tipo.
Definiciones precisas de los tipos en un formato general son difíciles de dar, así que voy a tratar de transmitir algo de precisión por describir (el comienzo) de la Iglesia de estilo (extensional) de orden superior de la lógica, que se extiende de la Iglesia de la teoría simple de tipos. Deje que el conjunto de tipos, $T$, el menor conjunto que contiene un conjunto de tipos simples (normalmente representado como $e$$t$) que es cerrado bajo la construcción funcional de los tipos de $\sigma \rightarrow \tau$ (funcional de los tipos de $\sigma \rightarrow \tau$ se interpretan como funciones de cosas de tipo $\sigma$ a las cosas de tipo $\tau$). Suponemos que el vocabulario contiene, además de las constantes lógicas $=$$\lambda$, un denumerably lista infinita de variables de tipo $\tau$ y una lista de constantes de tipo $\tau$, para todos los $\tau \in T$. La sintaxis es dada en forma de Backus-Naur (Índices indican los tipos): $$ \alpha_\sigma ::= x\sigma~ | ~c_\sigma~ |~ \beta_\tau = \gamma_\tau, ~\text{donde}~ \sigma = t~|~ \beta_{\eta \rightarrow \sigma}(\gamma_\eta)~|~\lambda x\eta. \beta_ \rho \text{donde}~ \sigma = \eta \rightarrow \rho $$
Para algunos $D \not = \emptyset$ deje $I_{e, D} := D; I_{t, D} := 2 = \lbrace 0, 1 \rbrace; I_{\sigma \rightarrow \tau, D} := I_{\tau, D}^{I_{\sigma, D}}$. Vamos a un modelo de ser un par de $M=\langle D, a \rangle$ tal que $a: Con_\sigma \rightarrow I_{\sigma, D}$ ($Con_\sigma := \lbrace c_\sigma: \sigma \in T\rbrace$), y una asignación (en $M$) una función $\theta: Var_\sigma \rightarrow I_{\sigma, D}$ ($Var_\sigma := \lbrace x_\sigma : \sigma \in T \rbrace$). Finalmente definimos una denotación de la función $\mathcal{\Delta}_{M, \theta}$, que asigna a cada una de las $\alpha_\sigma$ a un miembro de $I_\sigma$. Deje $\Delta_{M, \theta}(c) := a(c); \Delta_{M, \theta}(x) := \theta(x); \Delta_{M, \theta} (\beta = \gamma) := 1 ~\text{iff}~ \Delta_{M, \theta}(\beta) = \Delta_{M, \theta} (\gamma); \Delta_{M, \theta}(\beta(\gamma)) := \Delta_{M, \theta}(\beta) (\Delta_{M, \theta}(\gamma)); \Delta{M, \theta}(\lambda x. \beta):=f: I_\sigma \rightarrow I_\tau ~\text{such that} f(d) = \Delta_{M, \theta \frac{d}{x}}(\beta).$ de La habitual de verdad de las funciones y de orden superior, los cuantificadores pueden ser introducidas a través de Henkin definiciones de estilo.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
