Supongamos que quisiera formalizar la prueba de Turing sobre el problema de detención para que una máquina pueda verificarlo. Algunos de los sistemas de prueba de teoremas automatizados conocidos incluyen Mizar, Coq y HOL4. Descargué y experimenté con Coq, pero no tiene una biblioteca para máquinas Turing. Pensé en codificar uno yo mismo, pero me pareció que faltaba el tutorial y el idioma era difícil de aprender.
Mi pregunta es: ¿Existe un comprobador de teoremas automatizado que generalmente sea bueno para probar teoremas que involucren máquinas de Turing? Consideraría que un teorema de este tipo es "bueno" si puede formalizar una prueba de la indecidibilidad del problema de detención utilizando bibliotecas ya existentes. Lo consideraría aún mejor si es relativamente fácil de aprender. (Para el registro, generalmente no tengo dificultades con los lenguajes de programación).
Gracias,
Philip
Respuestas:
Aquí hay una biblioteca Isabelle / HOL que contiene el teorema de Rice, que establece la indecidibilidad de una amplia gama de problemas. Dado que esta biblioteca modela la computabilidad a través de funciones recursivas, debe codificar una máquina Turing universal como una función recursiva para utilizar este teorema para probar la indecidibilidad del problema de detención de las máquinas Turing. Sin embargo, las partes esenciales de la prueba de indecidibilidad ya están hechas.
http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html
fuente