¿Cómo mostrar que un tipo en un sistema con tipos dependientes no está habitado (es decir, la fórmula no es comprobable)?

15

Para sistemas sin tipos dependientes, como el sistema de tipos Hindley-Milner, los tipos corresponden a fórmulas de lógica intuicionista. Allí sabemos que sus modelos son álgebras de Heyting y, en particular, para refutar una fórmula, podemos restringir a un álgebra de Heyting donde cada fórmula está representada por un subconjunto abierto de .R

Por ejemplo, si queremos mostrar que no está habitada, construimos un mapeo partir de fórmulas para abrir subconjuntos de definiendo: Luego Esto muestra que la fórmula original no puede ser demostrable, ya que tenemos un modelo donde no es cierto, o de manera equivalente (por el isomorfismo de Curry-Howard) el tipo no puede ser habitado.ϕ R ϕ ( α )α.α(α)ϕRϕ ( α )

ϕ(α)=(-,0 0)
ϕ(α)=En t([0 0,))=(0 0,)ϕ(α(α))=(-,0 0)(0 0,)=R0 0.

Otra posibilidad sería utilizar marcos Kriepke .


¿Existen métodos similares para sistemas con tipos dependientes? ¿Como alguna generalización de álgebras de Heyting o cuadros de Kripke?

Nota: No estoy solicitando un procedimiento de decisión, sé que no puede haber ninguno. Solo pido un mecanismo que permita presenciar la imposibilidad de probar una fórmula, para convencer a alguien de que no es demostrable.

Petr Pudlák
fuente

Respuestas:

13

Que una fórmula no sea demostrable se puede hacer esencialmente de dos maneras. Con un poco de suerte, podremos mostrar dentro de la teoría de tipos que la fórmula implica una que ya se sabe que no es demostrable. La otra forma es encontrar un modelo en el que la fórmula no sea válida, y esto puede ser bastante difícil. Por ejemplo, llevó mucho tiempo encontrar el modelo de grupo de la teoría del tipo dependiente, que fue el primero en invalidar la unicidad de las pruebas de identidad .

La pregunta "¿qué es un modelo de teoría del tipo dependiente?" Tiene una respuesta algo complicada. Si ignora ciertas propiedades de sustitución, un modelo es una categoría cerrada localmente cartesiana , y esa podría ser la respuesta más simple. Si desea un modelo "real", existen varias opciones, consulte la página nLab sobre modelos categóricos de la teoría del tipo dependiente . En cualquier caso, la respuesta siempre es un poco complicada porque la teoría del tipo dependiente es un sistema formal bastante complejo.

Si tuviera que sugerir un solo artículo sobre el tema, probablemente recomendaría el artículo original de Robert Seely, "Categorías cerradas localmente cartesianas y teoría de los tipos" . Si tuviera que sugerir otro, probablemente sería uno que explicara lo que debe corregirse en el artículo de Seely, por ejemplo, "Sobre la interpretación de la teoría de tipos en categorías cerradas localmente cartesianas" de Martin Hoffman .

Un avance importante reciente en esta área es la constatación de que los modelos teóricos de homotopía también son modelos de teoría de tipos dependientes, ver referencias de homotopytypetheory.org . Esto ofrece una gran cantidad de posibilidades, pero ahora uno debe aprender la teoría de la homotopía para obtener los modelos.

Andrej Bauer
fuente
2
Esta respuesta es bastante buena, aunque ignora quizás la forma más simple posible de demostrar que un tipo no está habitado: ¡inducción en formas normales! En particular, es fácil demostrar que el medio excluido no puede ser habitado en el Cálculo de Construcciones por dicha inducción. Por supuesto, debe demostrar que cada término se puede poner en una forma normal del mismo tipo, y eso implica la construcción de un modelo ...
cody
@cody: buen punto, las formas normales pueden ser muy útiles.
Andrej Bauer el
@cody: "entonces debes demostrar que cada término se puede poner en una forma normal del mismo tipo": ¿no es una parte estándar de la metateoría para un sistema de tipos "bueno" (siempre que no lo hagas? tener axiomas) o una lógica "buena" (cuando esto es eliminación de corte)? Entonces puedes reutilizar la prueba existente, ¿verdad?
Blaisorblade
@ Blaisorblade: por supuesto, solo necesita probar la eliminación de cortes una vez. El punto de mayo fue que usar la inducción en formas normales en lugar de construcciones de modelos era una forma de plantear la pregunta: ya está construyendo un modelo para mostrar que cada término se puede poner en forma normal. En cierto sentido, está trabajando en el "modelo de forma normal", en lugar de hacer un trabajo estrictamente sintáctico.
cody
Ya veo: estaba pensando en el "esfuerzo de prueba", mientras que creo que estás razonando sobre cómo se implementa toda la prueba. Pero me has hecho cuestionar una vez más la distinción entre enfoques sintácticos y semánticos, dadas construcciones como modelos de términos. Así que hice una pregunta por separado sobre eso: cstheory.stackexchange.com/q/21534/989
Blaisorblade