Théorie de la complexité officiellement vérifiée

18

Existe-t-il un projet en cours pour vérifier formellement les théorèmes et les preuves de la théorie de la complexité à l'aide d'un assistant de preuve comme Coq? Y a-t-il des limites à cela?

cc.complexity-theory complexity proof-assistants Samuel Schlesinger
la source
3
Je pense que des recherches sont en cours à l'Université de Bologne avec l'assistant de preuve Matita. Voir par exemple Formalisation des machines de Turing .
Marzio De Biasi
Connexes: cstheory.stackexchange.com/q/4052/129 . Certaines des réponses parlent même de Coq, et d'autres mentionnent des résultats qui pourraient être interprétés comme des obstacles théoriques à ce projet, bien qu'ils ne soient probablement pas des obstacles dans la pratique.
Joshua Grochow
Merci, cette question était géniale @JoshuaGrochow, tellement heureux d'avoir appris cette monographie de Hartmannis. Si je comprends bien, la barrière serait alors de s'assurer que les classes de complexité que vous définissez sont ce que vous pensez qu'elles sont plutôt que la version "prouvable en Coq".
Samuel Schlesinger
1
Il y a une réponse à une question similaire ici , bien qu'il s'agisse davantage de prouver des limites de complexité spécifiques que des résultats de la théorie de la complexité générale
jmite
Oui, c'est pertinent. Je suis curieux de savoir comment le système de types sous-jacent pourrait aider, comme en incluant certaines notions de complexité dans les types de fonctions. Bien sûr, cela conduirait à un large éventail d'égalités, mais je pense que c'est ce que nous avons naturellement de la complexité de toute façon.
Samuel Schlesinger

Réponses:

6

Dans l'article suivant, mon collègue Uli Schöpp présente une vérification formelle (en Coq) d'un résultat non trivial par Cook et Rackoff sur la puissance de calcul des automates graphiques. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Une limite inférieure formalisée sur l'accessibilité des graphiques non orientés. Dans Logic for Programming, Artificial Intelligence, and Reasoning ( pp. 621-635). Springer Berlin / Heidelberg.)

Martin Hofmann
la source
1
Pourriez-vous s'il vous plaît donner la référence complète afin que la réponse ne dépende pas de la validité du lien?
holf