超多項式時間アルゴリズム/誘導証明の例？
組合せ論では、時々、アルゴリズム証明を得ることができる。これは、ゆるやかに次のような形式をとる。
-証明は段階を経て
-不変量が前の段階から帰納的に成り立つことを示す。
-アルゴリズムが終了することが示される
-終了時に保持される不変量は、目的の主張を含意する。
私が知っている最も良い例は、Konig's theorem のアルゴリズムによる証明で、ある意味では単なる max-flow/min-cut アルゴリズムである。 ある意味で，ほとんどの帰納法の証明はこの型に当てはまります．
上の例は多項式時間で実行されます。 このような帰納法が明らかに必要でないことを証明するために、 超多項式 時間かかるアルゴリズム/帰納法の証明の良い例はありますか？
つまり、Ackermannのような再帰や、ブルートフォース的なものは望んでいないのです。さらに、私は問題のインスタンスを解く超多項式時間アルゴリズムを探しているのではなく、ある種の定理を証明する超多項式時間アルゴリズムを探しています（例えば、上記の例では組合せ最大-最小定理のようなものです）。
3
3
この文脈で私が最初に思い浮かべるのは、Sperner's Lemmaの標準的な証明である。 特に帰納的なものではありません。 それでも、この証明では、指数関数的な時間がかかるかもしれないが、組合せ論的な理由で終了が保証されている経路追跡アルゴリズムが使われている。
実際、複雑さのクラスPPADは、このような経路追跡の議論が存在を証明する問題として定義されており、"SPERNER"はPPAD-completeな問題である。 このような問題が多項式時間で解けるかどうかは未解決の問題です（ほとんどの人がそうではないと予想していると思います）。 さらに、定義によれば、他のすべてのPPAD完全問題（またはPPAD問題一般）は、あなたが望む形、すなわち、アルゴリズム的存在証明を持っています。
非多項式時間存在証明のタイプで定義された複雑さのクラスは、他にもたくさんあります。 例えば、PPA, PLSなどである。 Papadimitriouの論文(On the complexity of the parity argument and other inefficient proofs of existence")を参照されたい。
Papadimitrouがアルゴリズム証明のいくつかの規範的なタイプを分類したことは、数学的実在証明の計算複雑性を理解する上で非常に適切であると、私はNoahと同意見です。
もう一つの興味深いクラスは、n次元立方体の非周期的一意性シンク配向（AUSO）におけるシンクを見つけることによって説明されている。これは、すべての面が一意なシンクを持つように、離散立方体を配向させたものである。このシンクを$exp (\sqrt n )$ステップで求めるアルゴリズムがある。
また，アルゴリズムによる証明で複雑さが不明なものに，Baranyの有色カラテオドリーの定理があります．
ヒドラゲームです。
これがアッカーマン的な再帰と言えるかどうかは分かりませんが、このアルゴリズムは超超指数的であり、さらにその上です。 実行時間の公式を書くことさえできませんが、確実に終了します。