Formalnie zweryfikowana teoria złożoności

18

Czy jest jakiś realizowany projekt formalnej weryfikacji twierdzeń i dowodów teorii złożoności przy użyciu asystenta dowodu, takiego jak Coq? Czy są jakieś granice?

cc.complexity-theory complexity proof-assistants Samuel Schlesinger
źródło
3
Myślę, że niektóre badania są prowadzone na uniwersytecie w Bolonii przy pomocy asystenta Matity. Zobacz na przykład Formalizowanie maszyn Turinga .
Marzio De Biasi
Powiązane: cstheory.stackexchange.com/q/4052/129 . Niektóre odpowiedzi mówią nawet o Coq, a inne wspominają o wynikach, które można interpretować jako teoretyczne bariery dla tego projektu, choć prawdopodobnie nie są to bariery w praktyce.
Joshua Grochow
Dzięki, to pytanie było świetne @JoshuaGrochow, więc cieszę się, że dowiedziałem się o monografii Hartmannisa. Jeśli rozumiem, barierą byłoby upewnienie się, że zdefiniowane przez ciebie klasy złożoności są tym, co według nich są, a nie wersją „możliwą do udowodnienia w Coq”.
Samuel Schlesinger
1
Jest odpowiedzią na podobne pytanie tutaj , chociaż to bardziej o udowodnienie konkretnych granic złożoności niż ogólna złożoność wyników teoretycznych
jmite
To prawda, ale to istotne. Zastanawiam się, w jaki sposób pomocny system typów mógłby pomóc, na przykład poprzez włączenie pewnych pojęć złożoności do typów funkcji. Oczywiście doprowadziłoby to do szerokiego zakresu równości, ale myślę, że i tak mamy naturalnie złożoność.
Samuel Schlesinger

Odpowiedzi:

6

W poniższym artykule mój kolega Uli Schöpp przedstawia formalną weryfikację (w Coq) nietrywialnego wyniku Cooka i Rackoffa na mocy obliczeniowej automatów grafowych. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Sformalizowana dolna granica nieukierunkowanej dostępności grafów. W logice programowania, sztucznej inteligencji i uzasadnienia ( str. 621-635). Springer Berlin / Heidelberg.)

Martin Hofmann
źródło
1
Czy możesz podać pełne odniesienie, aby odpowiedź nie zależała od ważności linku?
holf