Teoría de la complejidad formalmente verificada

18

¿Existe algún proyecto en curso para verificar formalmente los teoremas y las pruebas de la teoría de la complejidad utilizando un asistente de pruebas como Coq? ¿Hay límites para hacer esto?

Samuel Schlesinger
fuente
3
Creo que se está investigando en la Universidad de Bolonia con el asistente de pruebas Matita. Ver por ejemplo Formalización de máquinas de Turing .
Marzio De Biasi
Relacionado: cstheory.stackexchange.com/q/4052/129 . Algunas de las respuestas incluso hablan de Coq, y otras mencionan resultados que podrían interpretarse como barreras teóricas para este proyecto, aunque probablemente no sean barreras en la práctica.
Joshua Grochow
Gracias, esa pregunta fue genial @JoshuaGrochow, me alegro mucho de haberme enterado de esa monografía de Hartmannis. Si entiendo, la barrera sería asegurarse de que las clases de complejidad que defina sean lo que usted cree que son en lugar de la versión "demostrable en Coq".
Samuel Schlesinger el
1
Hay una respuesta a una pregunta similar aquí , aunque se trata más de probar los límites de complejidad específicos que los resultados de la teoría de complejidad en general
jmite
Sin embargo, eso es relevante. Tengo curiosidad acerca de las formas en que el sistema de tipos subyacente podría ayudar, como incluir algunas nociones de complejidad en los tipos de funciones. Por supuesto, esto conduciría a una amplia gama de igualdades, pero creo que eso es lo que naturalmente tenemos en complejidad.
Samuel Schlesinger el

Respuestas:

6

En el siguiente artículo, mi colega Uli Schöpp presenta una verificación formal (en Coq) de un resultado no trivial por parte de Cook y Rackoff sobre el poder computacional de los autómatas gráficos. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Un límite inferior formalizado sobre accesibilidad gráfica no dirigida. En lógica para programación, inteligencia artificial y razonamiento ( pp. 621-635). Springer Berlin / Heidelberg.)

Martin Hofmann
fuente
1
¿Podría dar la referencia completa para que la respuesta no dependa de la validez del enlace?
holf