Verwenden Algorithmen- oder Komplexitätsforscher in Anbetracht der auf einer Konferenz wie STOC behandelten Themen aktiv COQ oder Isabelle? Wenn ja, wie setzen sie es in ihrer Forschung ein? Ich gehe davon aus, dass die meisten Leute solche Tools nicht verwenden würden, da die Proofs zu niedrig wären. Verwendet jemand diese Proof-Assistenten auf eine Art und Weise, die für seine Forschung von entscheidender Bedeutung ist, im Gegensatz zu einer netten Ergänzung?
Ich bin interessiert, weil ich möglicherweise anfange, eines dieser Tools zu lernen, und es würde Spaß machen, sie im Kontext von Reduktions-, Richtigkeits- oder Laufzeitnachweisen zu lernen.
Antworten:
Eine allgemeine Faustregel lautet: Je abstrakter / exotischer die Mathematik ist, die Sie mechanisieren möchten, desto einfacher wird es. Umgekehrt ist es umso schwieriger, je konkreter / vertrauter die Mathematik ist. So sind (zum Beispiel) seltene Tiere wie die prädikative punktfreie Topologie wesentlich einfacher zu mechanisieren als die gewöhnliche metrische Topologie.
Dies mag zunächst ein wenig überraschend erscheinen, aber dies liegt im Grunde daran, dass konkrete Objekte wie reelle Zahlen an einer Vielzahl von algebraischen Strukturen beteiligt sind und Beweise, die sie beinhalten, jede Eigenschaft aus jeder Sicht verwenden können. Um zu den gewöhnlichen Argumenten zu gelangen, an die Mathematiker gewöhnt sind, müssen Sie all diese Dinge mechanisieren. Im Gegensatz dazu haben sehr abstrakte Konstruktionen eine (absichtlich) kleine und eingeschränkte Menge von Eigenschaften, sodass Sie viel weniger mechanisieren müssen, bevor Sie zu den guten Elementen gelangen können.
Beweise in Komplexitätstheorie und Algorithmen / Datenstrukturen tendieren (in der Regel) dazu, ausgefeilte Eigenschaften einfacher Gadgets wie Zahlen, Bäume oder Listen zu verwenden. Kombinatorische, probabilistische und zahlentheoretische Argumente tauchen beispielsweise in Theoremen der Komplexitätstheorie routinemäßig alle gleichzeitig auf. Es ist eine Menge Arbeit, die Unterstützung für Proof Assistant-Bibliotheken so weit zu bringen, dass dies angenehm ist!
Ein Kontext, in dem Menschen bereit sind, in die Arbeit einzusteigen, sind kryptografische Algorithmen. Es gibt aus komplexen mathematischen Gründen sehr subtile algorithmische Einschränkungen, und da Krypto-Code in einer gegnerischen Umgebung ausgeführt wird, kann selbst der kleinste Fehler katastrophal sein. So hat das Certicrypt-Projekt beispielsweise eine umfangreiche Verifizierungsinfrastruktur aufgebaut, um maschinengeprüfte Beweise für die Richtigkeit kryptografischer Algorithmen zu erstellen .
quelle
Ein sehr prominentes Beispiel ist natürlich die Gonthiers-Coq-Formalisierung des 4-Farben-Theorems in Coq, die eine Menge Kombinatorik verwendet.
Mein Kollege Uli Schöpp nutzte dazu die von Gonthier entwickelte ssreflect-Bibliothek, um auch in Coq ein Ergebnis von Cook und Rackoff auf Graphenautomaten zu verifizieren (und geringfügig zu erweitern). https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Eine formalisierte Untergrenze für ungerichtete Erreichbarkeit von Graphen. In Logik für Programmierung, künstliche Intelligenz und Argumentation ( S. 621-635). Springer Berlin / Heidelberg.)
quelle