Me pregunto si alguien puede darme la intuición detrás de por qué la estricta positividad de los tipos de datos inductivos garantiza una fuerte normalización.
Para ser claros, veo cómo tener ocurrencias negativas conduce a la divergencia, es decir, al definir:
data X where Intro : (X->X) -> X
Podemos escribir una función divergente.
Pero me pregunto, ¿cómo podemos demostrar que los tipos inductivos estrictamente positivos no permiten la divergencia? es decir, ¿hay alguna medida de inducción que nos permita construir una prueba de fuerte normalización (usando relaciones lógicas o similares)? ¿Y dónde se desglosa tal prueba de sucesos negativos? ¿Hay alguna buena referencia que muestre una fuerte normalización para un lenguaje con tipos inductivos?