Hispanopedia WikiEn la teoría de tipos , una rama de las matemáticas, el tipo identidad representa el concepto de igualdad . También se le conoce como igualdad proposicional para diferenciarla de la "igualdad de juicio". La igualdad en la teoría de tipos es un tema complejo y ha sido objeto de investigación, como en el campo de la teoría de tipos homotópicos . [ 1 ]
Comparación con la igualdad de juicio
El tipo identidad es una de las dos nociones diferentes de igualdad en la teoría de tipos. [ 2 ] La noción más fundamental es la "igualdad de juicio", que es un juicio .
Más allá de la igualdad basada en el juicio
El tipo de identidad puede hacer más que lo que puede hacer la igualdad basada en juicios. Se puede utilizar para mostrar "para todos".", lo cual es imposible de demostrar con igualdad de juicio. Esto se logra utilizando el eliminador (o "recursor") de los números naturales, conocido como "R".
La función "R" nos permite definir una nueva función sobre los números naturales. Esta nueva función "P" se define como "(λ x:nat . x+1 = 1+x)". Los demás argumentos actúan como las partes de una demostración por inducción. El argumento "PZ : P 0" se convierte en el caso base "0+1 = 1+0", que es el término "refl nat 1". El argumento "PS : P n → P (S n)" se convierte en el caso inductivo. En esencia, esto significa que cuando "x+1 = 1+x" se reemplaza por un valor canónico, la expresión será la misma que "refl nat (x+1)".
Versiones del tipo de identidad
El tipo identidad es complejo y objeto de investigación en la teoría de tipos. Si bien todas las versiones coinciden en el constructor, "refl", sus propiedades y funciones de eliminación difieren drásticamente.
Para las versiones "extensionales", cualquier tipo de identidad puede convertirse en una igualdad de juicio. Una versión computacional se conoce como "Axioma K" debido a Thomas Streicher. [ 3 ] Estas no son muy populares últimamente.
Complejidad del tipo de identidad
Martin Hofmann y Thomas Streicher refutaron la idea de que la teoría de tipos requería que todos los términos del tipo identidad fueran iguales. [ 4 ]
Una rama popular de la investigación sobre el tipo identidad es la teoría de tipos homotópicos [ 5 ] y su teoría de tipos cúbicos .
Referencias
- ↑ "Tipo de identidad" . nLab . Consultado el 19 de enero de 2022 .
- ↑ Martin-Löf, Per (junio de 1980). Teoría de tipos intuicionista (PDF) .
- ↑ Streicher, Thomas (1993). Investigaciones sobre la teoría de tipos intensionales (PDF) .
- ↑ Hofmann, Martin; Streicher, Thomas (julio de 1994). «El modelo de grupoide refuta la unicidad de las pruebas de identidad». Actas del Noveno Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación . págs. 208–212 . doi : 10.1109/LICS.1994.316071 . ISBN 0-8186-6310-3. S2CID 19496198 .
- ↑ Programa de Fundamentos Univalentes (12 de marzo de 2013). Teoría de tipos homotópicos . Instituto de Estudios Avanzados.
- teoría de tipos
