¿Qué hace que un lenguaje (y su sistema de tipos) sea capaz de probar teoremas sobre sus propios términos?

12

Recientemente intenté implementar Aaron's Cedille-Core , un lenguaje de programación minimalista capaz de probar teoremas matemáticos sobre sus propios términos. También probé la inducción de tipos de datos codificados con λ, lo que dejó en claro por qué serían necesarias sus extensiones.

Menos aún, todavía me pregunto de dónde provienen esas extensiones. ¿Por qué son lo que son? ¿Qué los justifica? Sé, por ejemplo, que algunas extensiones, como la recursividad, arruinan el lenguaje como un sistema de pruebas. Si decidiera extender también CoC con otras primitivas, ¿cómo justificaría? Entiendo que es necesaria una prueba de normalización, pero eso no prueba que esas primitivas "tengan sentido".

En resumen, ¿qué es lo que califica específicamente un lenguaje (y su sistema de tipos) como un sistema capaz de probar teoremas sobre sus propios términos?

type-theory functional-programming constructive-mathematics MaiaVictor
fuente
Leí un blog que estaba relacionado con esta pregunta, pero no puedo encontrarlo ahora :( Contenía la frase "¡El sistema T es suficiente!" O algo así y hablaba de sistemas de tipos dependientes.
Labbekak
2
Lo encontré: queuea9.wordpress.com/2010/01/17/… En realidad está escrito por Aaron Stump, por lo que es posible que ya lo sepas.
Labbekak
La recursión no vigilada "arruina" el lenguaje como sistema de prueba, la recursión vigilada no. Para demostrar que las primitivas tienen sentido, diría que construyes un modelo. Y para probar teoremas sobre sus propios términos, necesita una especie de isomorfismo de Curry-Howard y un tipo dependiente para que las cosas que demuestres (tipos) puedan hablar sobre tus términos.
xavierm02

Respuestas:

5

[Sigue la autopublicidad, pero creo que esto es relevante.]

tut≡utu∀v,(λx.x)v≡v

Por supuesto, también puede asumir equivalencias, y hay varias formas diferentes de cuantificadores (con tipo / sin tipo, universal / existencial). Este mecanismo se puede utilizar para razonar sobre cualquier programa (no es necesario que se pruebe que finalicen o incluso que se tipeen). La única restricción es que los programas que se utilizan como pruebas deben ser probados por el sistema (la recurrencia general arbitraria conduce a una inconsistencia).

Aquí hay un par de referencias si quieres ver esto:

Rodolphe Lepigre
fuente