En la teoría de tipos , el tipo identidad representa el concepto de igualdad . También se lo conoce como igualdad proposicional para diferenciarlo 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 de homotopía . [1]
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 .
El tipo de identidad puede hacer más que lo que puede hacer la igualdad de juicio. Puede usarse para mostrar "para todos ", lo cual es imposible de mostrar con la igualdad de juicio. Esto se logra usando 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. Esa nueva función "P" se define como "(λ x:nat . x+1 = 1+x)". Los demás argumentos actúan como las partes de una prueba de 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. Básicamente, esto dice que cuando "x+1 = 1+x" tiene "x" reemplazada por un valor canónico, la expresión será la misma que "refl nat (x+1)".
El tipo de identidad es complejo y es 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 radicalmente.
En las versiones "extensionales", cualquier tipo de identidad se puede convertir 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.
Martin Hoffman y Thomas Streicher refutaron que la teoría de tipos de ideas requería que todos los términos del tipo identidad fueran iguales. [4]
Una rama popular de investigación sobre el tipo identidad es la teoría de tipos de homotopía [5] y su teoría de tipos cúbicos.
