Estaba pensando en pruebas y me encontré con una observación interesante. Por lo tanto, las pruebas son equivalentes a los programas a través del isomorfismo de Curry-Howard, y las pruebas circulares corresponden a una recursión infinita. Pero sabemos por el problema de detención que, en general, es indecidible probar si un programa arbitrario se repite para siempre. Por Curry-Howard, ¿eso significa que no hay un "comprobador de pruebas" que pueda determinar si una prueba usa razonamiento circular?
Siempre he pensado que se supone que las pruebas están compuestas por pasos fáciles de verificar (que corresponden a las aplicaciones de las reglas de inferencia), y verificar todos los pasos le da la confianza de que la conclusión sigue. Pero ahora me pregunto: ¿tal vez es realmente imposible escribir un comprobador de pruebas de este tipo, porque no hay forma de evitar el problema de detención y detectar el razonamiento circular?
fuente
Function
oProgram Fixpoint
construcciones para probar que alguna función es total si falla el verificador de totalidad. Un ejemplo simple es la función merge-sort en las listas. Es necesario probar manualmente que dividimos las listas (de longitud> 1) en sublistas estrictamente más pequeñas.Program
y similares son una pista falsa. No cambian la teoría. Lo que hacen es azúcar sintáctico para usar una medida en una prueba: en lugar de razonar que el objeto que le interesa se hace más pequeño, agrega un nivel de indirección: calcule que algún otro objeto se hace más pequeño (por ejemplo, algún tamaño) y demuestre que se hace más pequeño Ver laWf
biblioteca