Criterio para la consistencia de los sistemas de tipos puros

Question

Los sistemas de tipos puros se caracterizan de una forma casi combinatoria: un conjunto de axiomas $\star_i : \star_j$, y un conjunto de triples $(\star_i, \star_j, \star_k)$ que indican cuándo se puede formar el producto dependiente $\prod_{x : A} B(x)$ y hacia dónde va -- $\prod_{x:A}B(x) : \star_k$ exactamente cuando $A:\star_i, B:\star_j$, sin tener en cuenta problemas de contexto.

Así surge una pregunta, de manera natural que me desconcertó cuando no pude encontrar resultados relevantes: ¿existe algún criterio simple para determinar cuándo un sistema de tipos puro es consistente? Aunque no espero que dicho criterio sea a la vez sólido y completo, dada la complejidad lógica que subyace en ello.

¿Hay algún resultado relacionado con esta pregunta? Agradezco si pudieras proporcionar un indicador.

Answer 1

Escribiré algunos fragmentos de pensamientos aquí.

Primero algunos resultados conocidos. Todo el cubo lambda es consistente (y normalizante, aunque no lo mencioné en la pregunta, también me interesa eso). Una estructura jerárquica que $\star_i : \star_{i+1}$ y la regla $(\star_i, \star_j, \star_k)$ solo si $k > i, j$ es consistente, según la construcción de @AndrejBauer (encontré una página web que detalla eso, pero perdí la URL, la enlazaré cuando la encuentre). Y el sistema $U^-$ es inconsistente, sufriendo el paradoja de Girard.

Luego, algunas reducciones teóricas de grafos. Considera el PTS como un hipergrafo con aristas de 2 y 3. Luego se pueden considerar solo los componentes conectados. Además, una incrustación $\lambda S_1 \to \lambda S_2$ de dos PTS (es decir, un mapeo de los vértices que conserva las aristas) refleja la consistencia: la consistencia de $\lambda S_2$ implica la de $\lambda S_1$, y la implicación inversa para la inconsistencia.

Creo que hay alguna forma de cortar algunas aristas errantes, pero aún no he entrado en eso. Pero la idea es definir una dependencia débil entre tipos. Digo que $\star_i$ depende débilmente de $\star_j$ si para alguna expresión $\Gamma, x:N \vdash A:M:\star_i$ donde $N:\star_j$, $A$ puede contener $x$ de manera bien tipificada. Si no hay una dependencia débil, probablemente la regla $(\star_i, \star_j, \star_k)$ se puede traducir por un método similar de traducción de $\lambda P$ a $\lambda ^\to$, ver el Cálculos Lambda con Tipos de Barendregt.

Me imagino que si hacemos suficientes reducciones, podríamos determinar la consistencia de todos los PTS. La esperanza radica en que la mayoría de los PTS probablemente sean trivialmente inconsistentes porque están demasiado enredados e impredicativos :(