Técnicas de prueba para demostrar que la verificación de tipo dependiente es decidible

10

Estoy en una situación en la que necesito demostrar que la verificación de tipos es decidible para un cálculo de tipo dependiente en el que estoy trabajando. Hasta ahora, he podido demostrar que el sistema se está normalizando fuertemente y, por lo tanto, que la igualdad de definición es decidible.

En muchas referencias que leí, la capacidad de decisión de la verificación de tipos aparece como un corolario de una fuerte normalización, y lo creo en esos casos, pero me pregunto cómo se muestra esto.

En particular, estoy atascado en lo siguiente:

  • El hecho de que los términos bien tipados se estén normalizando fuertemente, no significa que el algoritmo no se repita para siempre en entradas no bien tipadas
  • Dado que las relaciones lógicas generalmente se usan para mostrar una fuerte normalización, no hay una métrica decreciente conveniente a medida que avanzamos los términos de verificación de tipos. Entonces, incluso si mis reglas de tipo están dirigidas por la sintaxis, no hay garantía de que la aplicación de las reglas finalmente termine.

Me pregunto, ¿alguien tiene una buena referencia a una prueba de capacidad de verificación de la tipificación de un idioma de tipo dependiente? Si es un cálculo de núcleo pequeño, está bien. Cualquier cosa que discuta técnicas de prueba para mostrar la capacidad de decisión sería genial.

jmite
fuente
77
Los algoritmos de verificación de tipo bidireccionales habituales nunca intentan normalizar un término (o un tipo) sin verificar primero que esté bien escrito (o bien formado). No necesita preocuparse por normalizar los términos sin tipo.
Andrej Bauer el
77
Respecto a la aplicación de las reglas: todas las reglas de términos y tipos disminuyen el objetivo, excepto la conversión de tipos. Por lo tanto, necesitamos controlar la conversión de tipos, lo que hacemos mediante el uso de un enfoque bidireccional.
Andrej Bauer el

Respuestas:

9

De hecho, hay una sutileza aquí, aunque las cosas funcionan bien en el caso de la verificación de tipos. Escribiré el problema aquí, ya que parece aparecer en muchos hilos relacionados, y trataré de explicar por qué las cosas funcionan bien cuando se verifica en una teoría de tipo dependiente "estándar" (seré deliberadamente vago, ya que estos problemas tienden a surgir independientemente):

DΓt:ADΓA:ssutBΔDΔu:B

Este buen hecho es algo difícil de demostrar, y se compensa con un hecho bastante desagradable:

Hecho 2: ¡En general, y no son sub-derivaciones de !DD DD

Esto depende un poco de la formulación precisa de su sistema de tipos, pero la mayoría de los sistemas "operativos" implementados en la práctica satisfacen el Hecho 2.

Esto significa que no puede "pasar a sub-términos" cuando razona por inducción en derivaciones, o concluye que la afirmación inductiva es verdadera sobre el tipo de término sobre el que está tratando de probar algo.

Este hecho lo muerde con bastante dureza cuando intenta demostrar declaraciones aparentemente inocentes, por ejemplo, que los sistemas con conversión con tipo son equivalentes a aquellos con conversión sin tipo.

Sin embargo , en el caso de la inferencia de tipos, puede proporcionar un algoritmo de inferencia simultáneo de tipo y clasificación (el tipo del tipo) mediante inducción en la estructura del término, que puede implicar un algoritmo dirigido por tipo como sugiere Andrej. Para un término dado (y contexto , usted falla o encuentra tal que y . No necesita usar la hipótesis inductiva para encontrar el último derivación, y así, en particular, evita el problema explicado anteriormente.tΓA,sΓt:AΓA:s

El caso crucial (y el único caso que realmente requiere conversión) es la aplicación:

infer(t u):
   type_t, sort_t <- infer(t)
   type_t' <- normalize(type_t)
   type_u, sort_u <- infer(u)
   type_u' <- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Cada llamado a la normalización se realizó en términos bien escritos, ya que este es el invariante para inferel éxito.


Por cierto, a medida que se implementa, Coq no tiene una verificación de tipos decidible, ya que normaliza el cuerpo de las fixdeclaraciones antes de intentar escribirlas.

En cualquier caso, los límites de las formas normales de términos bien tipados son tan astronómicos que, de todos modos, el teorema de la capacidad de decisión es principalmente académico en este punto. En la práctica, ejecuta el algoritmo de verificación de tipos durante el tiempo que tenga paciencia e intenta una ruta diferente si aún no ha finalizado.

cody
fuente
Tu respuesta me pareció muy útil, gracias. Tengo dos preguntas: 1. ¿Qué significa "sistemas operativos"? Cual es la alternativa? 2. ¿Puede ser más explícito con el ejemplo: qué significa (qué hecho estamos tratando de demostrar?) "Los sistemas con conversión con tipo son equivalentes a aquellos con conversión sin tipo". ¡Gracias!
Łukasz Lew
1
@ ŁukaszLew La alternativa a un sistema operativo (uno implementado en la práctica, por ejemplo, en el software Coq o Agda) sería un sistema teórico, que es útil para demostrar las propiedades meta-teóricas, pero es ineficiente o inconveniente de usar en la práctica. Probar la equivalencia de un sistema operativo y un sistema teórico es a menudo una parte importante del diseño de un sistema. Hablo más sobre esto aquí: cstheory.stackexchange.com/a/41457/3984
cody
¡Creo que vale la pena mencionar a Lennart Augustsson, Simpler, Easier! . Esta es una implementación mínima de Haskell de verificación de tipos y alguna inferencia para el cálculo lambda tipificado de forma dependiente. Hay un código que se corresponde estrechamente con el de Cody infer(t u):; para encontrarlo, busque " tCheck r (App f a) =". Para una implementación más completa pero simple, puede consultar Morte'stypeWith .
Łukasz Lew
1
@ ŁukaszLew El problema de conversión con tipo versus sin tipo es una pregunta abierta bien conocida que relaciona 2 formulaciones de teorías de tipo, y se resolvió recientemente: pauillac.inria.fr/~herbelin/articles/…
cody
¿Qué significa ? ut
jonaprieto