Gibt es Beweise für die Existenz eines nicht konstruktiven Algorithmus?

47

Ich erinnere mich, dass ich möglicherweise auf Probleme gestoßen bin, die sich mit einer bestimmten Komplexität als lösbar erwiesen haben, aber mit keinem bekannten Algorithmus, um diese Komplexität tatsächlich zu erreichen.

Ich habe Mühe, mir Gedanken darüber zu machen, wie dies der Fall sein kann. wie ein nicht konstruktiver Beweis für die Existenz eines Algorithmus aussehen würde.

Gibt es tatsächlich solche Probleme? Haben sie viel praktischen Wert?

jkff
quelle
11
Algorithmen basierend auf dem Robertson-Seymour-Theorem ? Oder einfacher: Verwenden von PEM, um zu beweisen, dass es einen Algorithmus gibt, bei dem wir nicht wissen, welcher (das Halteproblem ist für jede feste Turing-Maschine trivial entscheidbar, aber wie können wir einen Algorithmus finden, der das Problem richtig löst, ohne es zu lösen (die einheitliche Version von) das haltproblem?) ps: was meinst du mit "praktischem wert"?
Kaveh
6
Warum gibt es auch einfachere Beispiele .
Raphael
1
Raphael, es scheint mir, dass Ihr Kommentar plausibel zu einer Antwort aufgewertet werden könnte. Vielleicht könnten Sie (oder jemand) dies versuchen?
John Sidles
2
Dies ist jetzt auf Wikipedia .
Raphael

Antworten:

33

Betrachten Sie die Funktion (von hier genommen )

f(n)={10n tritt in der Dezimaldarstellung von auf π0sonst

Trotz des Aussehens kann mit dem folgenden Argument berechnet werden. Entwederf

  1. 0n kommt für jedes oder vorn
  2. Es gibt ein sodass auftritt, jedoch nicht.0 k 0 k + 1k0k0k+1

Wir wissen (noch) nicht, was es ist, aber wir wissen, dass mitfF={f,f0,f1,}

  1. f(n)=1 und
  2. fk(n)=[nk] .

Da , ist berechenbar - aber wir können nicht sagen, was ist. f fFREff

Raphael
quelle
2
Diese Antwort ist gut, ebenso wie die anderen Antworten. Offensichtlich hat jkffs Frage mehr als eine Antwort in dem Sinne, dass es mehrere Proof-Technologien gibt, die die Existenz von Algorithmen nicht konstruktiv demonstrieren können.
John Sidles
Ich bezeichne diese jedoch als "akzeptiert", da sie bei weitem die einfachste ist und die Kernidee zeigt, wie ein Beweis für die Existenz eines nicht konstruktiven Algorithmus entstehen kann.
jkff
@jkff So einfach es auch ist, es ist eine großartige Übung für Studenten in TCS-Einführungskursen. Ich brauchte Wochen, um meine Intuition / mein Konzept der Berechenbarkeit im Lichte dieser Funktion anzupassen.
Raphael
Ich wäre bereit, eine Million Dollar zu wetten, dass die konstante 1-Funktion ist. Und ich habe keine Million Dollar. f
Daniel McLaury
26

Dies ist vielleicht nicht genau das , was Sie meinen, aber der optimale Minimum-Spanning-Tree-Algorithmus von Seth Pettie und Vijaya Ramachandran ist in gewissem Sinne nicht konstruktiv.

Es ist eine offene Frage, ob es einen deterministischen Algorithmus gibt, um minimale Spannbäume in linearer (dh ) Zeit zu berechnen . Pettie und Ramachandran beschreiben einen Algorithmus, der MSTs in linearer Zeit berechnet, falls ein solcher Algorithmus existiert .O(n+m)

Intuitiv reduziert ihr Algorithmus jede Vertex-Instanz des MST-Problems auf O ( n / k ) kleinere Instanzen mit O ( k ) Vertices in linearer Zeit, wobei (sagen wir) k = O ( log log log log log log log n ) . Dann berechnen sie den optimalen Vergleichsbaum , der den minimalen Spannbaum jedes k- Vertex-Graphen durch Brute-Force-Aufzählung berechnet . Selbst wenn dies in k nur fünffach exponentielle Zeit in Anspruch nimmt, ist das nur OnO(n/k)O(k)k=O(LogLogLogLogLogLogLogn)kk Zeit. Schließlich lösen sie die kleinen Instanzen mit diesem optimalen Entscheidungsbaum.O(LogLogn)

Mit anderen Worten, Pettie und Ramachandran konstruieren einen optimalen MST-Algorithmus nur indirekt, indem sie einen Algorithmus konstruieren, der einen optimalen MST-Algorithmus konstruiert.

Jeffε
quelle
Das ist cool! Übrigens, ihr Algorithmus stimmt mit der besten Laufzeit in einem Entscheidungsbaummodell überein, oder?
Sasho Nikolov
Ja, das ist richtig!
Jeffs
2
In gewissem Sinne klingt dies eher nach einer Funktion höherer Ordnung (eine Funktion, die eine andere Funktion übernimmt, und der Beweis ihrer zeitlichen Komplexität hängt von der Komplexität der Eingabe ab) als nach einem nicht konstruktiven Beweis. Ich würde einen nicht konstruktiven Beweis als etwas bezeichnen, das die klassische Logik (LEM, DNE oder Peirce) maßgeblich für die Erstellung des Beweises für die Existenz des Algorithmus heranzieht, ohne ihn tatsächlich bereitzustellen. Es ist trotzdem cool.
Copumpkin
13

Hier sind zwei Beispiele.

  1. Einige Algorithmen, die den Satz von Robertson-Seymour verwenden . Der Satz besagt, dass es für jeden Fall ein endliches Hindernis gibt, aber keinen Weg gibt, eine solche endliche Menge zu finden. Obwohl wir nachweisen können, dass der Algorithmus existiert, hängt die explizite Aussage des Algorithmus daher von dem endlichen Hindernissatz ab, den wir nicht finden können. Mit anderen Worten, wir wissen, dass es einen Algorithmus gibt, aber wir wissen (noch) nicht, wie wir einen finden können.

  2. Ein stärkeres Beispiel, obwohl weniger natürlich, ist die Verwendung von PEM oder ähnlichen nicht-konstruktiven Axiomen. Dies ist insofern stärker, als wir nachweisen können, dass die konstruktive Existenz eines Algorithmus ein nichtkonstruktives Axiom implizieren würde (ähnlich wie bei Brouwers schwachen Gegenbeispielen ). Ein solches Beispiel ist stärker , weil es nicht nur sagt , dass wir nicht wissen , jetzt eine explizite Algorithmus (oder eine algorithmische Weise ein zu finden), sondern auch , dass es keine Hoffnung gibt , dies zu tun.

    Als Beispiel können wir PEM verwenden, um zu beweisen, dass ein Algorithmus existiert, während wir nicht wissen, welcher und ein konstruktiver Weg, einen zu finden, ein nicht konstruktives Axiom implizieren würde. Lassen Sie mich ein einfaches Beispiel geben:

    Das Problem des Anhaltens ist für jede feste Turing-Maschine trivial zu entscheiden (jede TM hält an oder hält nicht an, und in jedem Fall gibt es eine TM, die die richtige Antwort ausgibt), aber wie können wir einen Algorithmus finden, der das Problem richtig löst, ohne es zu lösen ( die einheitliche version von) das haltproblem?

    Genauer gesagt können wir nicht konstruktiv beweisen, dass es bei einem TM ein TM H T gibt , das das Halteproblem für M entscheidet . Formal kann die folgende Aussage nicht konstruktiv bewiesen werden:MHTM

    eN fN [({f}( )=0{e})({f}( )=1{e})]

    Hier ist das TM mit dem Code e (in einer festen Darstellung von TMs), { e } bedeutet { e } hält an und { f } bedeutet, dass { f } nicht anhält.{e}e{e}{e}{f}{f}

Kaveh
quelle
1
Was ist "endliche Behinderung für jeden Fall"? Ich glaube , Sie „finite Hindernis bedeuten Satz für jede unendliche Menge von kleineren Graphen geschlossen “ auch noch nicht gut ist (ich Ihre Antwort bearbeitet , es zu beheben scheint aber abgelehnt, ziehe ich es nicht diese zu wiederholen).
Saeed
8

Ja.

An einem Punkt in (1) beweisen der Dichotomiesatz des komplexgewichteten Zählgraphen für jede endliche Domänengröße, Cai, Chen und Lu, nur die Existenz einer Polynomzeitverringerung zwischen zwei Zählproblemen durch Polynominterpolation. Ich kenne keinen praktischen Wert für einen solchen Algorithmus.

Siehe Abschnitt 4 der arXiv-Version. Das fragliche Lemma ist Lemma 4.1, das als "Erstes feststeckendes Lemma" bezeichnet wird.

Eine Möglichkeit, diesen Beweis konstruktiv zu gestalten, besteht darin, die komplex gewichtete Version eines Ergebnisses von Lovasz zu beweisen :

Für all , Z H ( G , w , i ) = Z H ( G , W , j ) genau dann , wenn es eine automorphism existiert f von G , so daß f ( i ) = j .GZH(G,w,i)=ZH(G,w,j)fGf(i)=j

Hier ein Scheitelpunkt in ist H , i und j sind Vertices in G und Z H ( G , w , i ) ist die Summe über alle komplexen gewichteten Graphen homomorphisms von G bis H mit der zusätzlichen Einschränkung , dass i zugeordnet werden müssen zu w .wHijGZH(G,w,i)GHiw

(1) Jin-Yi Cai, Xi Chen und Pinyan Lu, Graphhomomorphismen mit komplexen Werten: Ein Dichotomiesatz ( arXiv ) ( ICALP 2010 )

Tyson Williams
quelle
7

Einige frühe Ergebnisse aus den späten 80ern:

Aus der Zusammenfassung des zweiten Punktes:

Jüngste grundlegende Fortschritte in der Graphentheorie haben jedoch leistungsfähige neue nichtkonstruktive Werkzeuge zur Verfügung gestellt, mit denen die Zugehörigkeit zu P garantiert werden kann. Diese Werkzeuge sind auf zwei verschiedenen Ebenen nichtkonstruktiv: Sie produzieren weder den Entscheidungsalgorithmus noch stellen sie nur die Endlichkeit eines Hindernissatzes fest Sie enthüllen auch nicht, ob ein solcher Entscheidungsalgorithmus bei der Konstruktion einer Lösung hilfreich sein kann. Wir betrachten und veranschaulichen kurz die Verwendung dieser Werkzeuge und diskutieren die scheinbar schwierige Aufgabe, die versprochenen Algorithmen für die Polynomzeitentscheidung zu finden, wenn diese neuen Werkzeuge angewendet werden.

vzn
quelle
6

Ein Beispiel für eine unendliche Familie von Problemen (von fraglichem praktischem Wert), für die wir zeigen können:

  1. Das für jedes Problem gibt es einen Algorithmus, um es zu lösen.
  2. Dass es keine Möglichkeit gibt, diese Algorithmen (im Allgemeinen) zu konstruieren.

Mit anderen Worten, ein nachweislich nicht konstruktiver Beweis. Unsere Problemfamilie (aus dieser Frage ) für jede Turingmaschine :M

LM={M|L(M)=L(M) und |M||M|}

  1. M

  2. PMP(M)LMMM|M||M|P(M)(M)P

Artem Kaznatcheev
quelle
2
Süß. Der praktische Wert ist jedoch möglicherweise weniger fragwürdig als Sie denken: Dies ist eine Entscheidungsversion des Problems, das kürzeste Programm mit einer bestimmten Ausgabe zu finden, dh eine optimale Datenkomprimierung.
David Eppstein
1
Ich denke, das Beispiel ähnelt dem, das ich gegeben habe. Beachten Sie, dass wir, wenn wir sagen, dass es nicht konstruktiv ist, das Wort konstruktiv als rekursiv / berechenbar interpretieren, was eine der Schulen im Konstruktivismus ist.
Kaveh
2

Aus "Bidimensionalitätstheorie und Algorithmischer Graph Minor Theory Lecture Notes" für MohammadTaghi Hajiaghayis Tutorial, von Mareike Massow, Jens Schmidt, Daria Schymura und Siamak Tazari.

Jede Eigenschaft mit geschlossenen Graphen kann durch eine endliche Menge verbotener Minderjähriger charakterisiert werden.

Leider ist ihr Ergebnis "inhärent" nicht konstruktiv, dh es gibt keinen Algorithmus, der im Allgemeinen bestimmen kann, welche Minderjährigen für eine gegebene Eigenschaft eines geringfügig geschlossenen Graphen ausgeschlossen werden sollen. Darüber hinaus kann die Anzahl der verbotenen Minderjährigen hoch sein: Beispielsweise sind für auf dem Torus eingebettete Grafiken mehr als 30.000 verbotene Minderjährige bekannt, die Liste ist jedoch unvollständig.

[...]

Jede Eigenschaft eines kleinen geschlossenen Graphen kann in Polynomzeit (auch in Kubikzeit) festgelegt werden.

Kumpel
quelle
0

Algorithmisches lokales Lemma von Lovász - "Das algorithmische lokale Lemma von Lovász bietet eine algorithmische Methode zum Konstruieren von Objekten, die einem System von Abhängigkeiten mit begrenzter Abhängigkeit gehorchen die schlechten Ereignisse zu vermeiden. " Unter bestimmten Voraussetzungen / Einschränkungen für die Verteilung wird von Moser / Tardos ein konstruierter Algorithmus angegeben [1]. Das lokale Lemma von Lovasz scheint verschiedene tiefe Verbindungen zur Komplexitätstheorie zu haben, siehe z. B. [2].

[1] Ein konstruktiver Beweis des General Lovász Local Lemma von Moser, Tardos

[2] Das lokale Lemma und die Zufriedenheit von Lov´asz Gebauer, Moser, Scheder, Welzl

vzn
quelle
Es ist ein anderes Gefühl von "konstruktiv". Manchmal verwenden Komplexitätstheoretiker (ab) das Wort "konstruktiv", um effizient algorithmisch zu bedeuten, und in diesem Zusammenhang wird alles, was nicht effizient algorithmisch ist, als nicht konstruktiv bezeichnet. Dies unterscheidet sich von dem in der Frage beabsichtigten konstruktiven Beweisbegriff.
Kaveh
Dein erster Satz ist irreführend. Die algorithmische LLL ist eine völlig konstruktive im Sinne eines polynomialen Zeitalgorithmus. Die ursprüngliche LLL hatte einen nicht konstruktiven Beweis im Sinne eines induktiven Arguments über einen potenziell riesigen Wahrscheinlichkeitsraum. Die Nacharbeiten zu Mosers und Tardos 'Aufsatz haben praktisch alle Lücken zwischen dem algorithmischen LLL und sogar einer gewissen Stärkung des LLL geschlossen (siehe doi.acm.org/10.1145/1993636.1993669
Sasho Nikolov,
Das ursprüngliche Lemma von 1975 war nicht konstruktiv, und spätere Forscher (Jahrzehnte später) fanden konstruktive Algorithmen für Sonderfälle, aber "praktisch alle Lücken" sind nicht dasselbe wie "alle Lücken". Es ist ein nützliches Beispiel, um zu zeigen, dass es nicht garantiert ist, dass ein nichtkonstruktiver Existenznachweis immer so bleibt, dh Nichtkonstruktivität ist nicht immer absolut und kann "Änderungen unterliegen", und dass weitere / spätere Forschungen Lücken schließen können, und sogar ob Alle Lücken werden durch einen Algorithmus geschlossen. es gibt andere Beispiele dafür. Ich habe Moser / Tardos-Lösung zitiert.
VZN
1
Ich sage nur, dass die Art und Weise, wie Sie Ihren ersten Satz geschrieben haben, den Eindruck erweckt, dass das "algorithmische LLL" "nicht konstruktiv" ist. In diesem Zitat gab es einen Verweis auf die ursprüngliche LLL, aber dieser Verweis wird übersprungen, da Sie die Ellipsen dort platzieren. Könnten Sie das Zitat so bearbeiten, dass es nicht verwirrend ist?
Sasho Nikolov
1
Ich denke, Ihre Antwort hat nur einen tangentialen Bezug zum Thema, aber es ist ein guter Punkt, dass einige Sätze mit nicht konstruktiven Beweisen auch konstruktive Beweise zulassen (und manche nachweislich nicht, je nachdem, wie Sie "konstruktiv" definieren). Ein weiteres Problem bei der Weiterentwicklung des konstruktiven lebenslangen Lernens ist, dass nicht klar ist, wie ein angemessenes Rechenproblem in allen Situationen definiert werden kann, in denen das
Sasho Nikolov,