Sustitución hereditaria con una jerarquía universal.

He leído sobre la sustitución hereditaria del cálculo simple de Lambda y del marco lógico con términos y tipos distintos.

Me pregunto, ¿hay algún ejemplo de sustitución hereditaria en un sistema de tipo dependiente con una jerarquía universal? es decir, donde etc.$True : Set_0 : Set_1:Set_2$

Me pregunto en particular cómo establecer una medida de inducción en dicho sistema. La versión de tipo simple está disminuyendo estructuralmente en el tipo de la variable que se reemplaza. Esto no funciona con tipos dependientes, ya que para LF el papel que vinculé usa la eliminación simple de los términos, realizando inducción sobre la forma del tipo.

Sin embargo, borrar a tipos simples no funciona con una jerarquía de universos, ya que si tiene algo como esto:

• $f : (x : Set_1)\to x \to True$ implica que
• $f\ ((y : True) \to True \to True ): True \to True \to True$

es decir, la aplicación de una función dio como resultado un tipo estructuralmente más grande.

Supongo que la solución tiene algo que ver con los índices del universo, pero si existe una técnica existente para establecer que la inducción está bien fundada, preferiría citarla en lugar de crear algo por mi cuenta.

Aquí hay una referencia para el sistema predicativo F. La medida de hecho incluye el conjunto múltiple de niveles de universo en un tipo. No puedo decir mucho sobre si este enfoque se generaliza a la teoría del tipo dependiente predicativo.

A partir de noviembre de 2018, cómo hacer esto para las teorías de tipo dependiente con grandes eliminaciones es una pregunta abierta.

Establecer que la recursión está bien fundada no es tan malo; puedes usar el teorema de Pataraia para probar que existe el punto fijo que deseas. Vea los * Sistemas de tipo de construcción de Robert Harper sobre una semántica operacional para obtener instrucciones . (También puede hacerlo a través de una definición inductiva-recursiva).

La parte difícil es formular la sustitución hereditaria de una manera agradable: la dirección natural lo lleva a sustituir no un término, sino una sustitución completa por un contexto, y esto plantea muchas preguntas sobre cuándo y cómo establecer las propiedades de las cosas composiciones similares de sustituciones (hereditarias).

Si resultara imposible, estaría totalmente conmocionado. Sin embargo, en la actualidad nadie lo ha hecho. Si quieres trabajar en esto, te sugiero que te pongas en contacto con Andreas Abel, Dan Licata y Mike Shulman. (O yo, para el caso).