Czy istnieje algorytm, który można udowodnić, chociaż nie wiemy, co to jest?

W matematyce istnieje wiele dowodów na istnienie, które nie są konstruktywne, więc wiemy, że istnieje pewien obiekt, chociaż nie wiemy, jak go znaleźć.

Szukam podobnych wyników w informatyce. W szczególności: czy istnieje problem, który możemy udowodnić, że można go rozstrzygać bez pokazywania odpowiedniego algorytmu? Tzn. Wiemy, że można go rozwiązać za pomocą algorytmu, ale nie wiemy, jak wygląda algorytm?

Najprostszy przypadek, jaki znam algorytm, który istnieje, choć nie wiadomo, który algorytm dotyczy automatów skończonych.

Iloraz języka L 1 przez język L 2 jest zdefiniowany jako L 1 / L 2 = { x ∣ ∃ y ∈ L 2  tak, że  x y ∈ L 1 } .$L_1/L_2$$L_1$$L_2$$L_1/L_2=\{x \mid \exists y\in L_2 \text{ such that } xy\in L_1\}$

Łatwo jest udowodnić, że zbiór regularny jest zamykany pod ilorazem przez dowolny zestaw. Innymi słowy, jeżeli jest regularny i L 2 jest dowolna (niekoniecznie regularny), a L 1 / L 2 jest prawidłowe, za.$L_1$$L_2$$L_1/L_2$

Dowód jest dość prosty. Niech będzie FSA akceptującym regularny zbiór R , gdzie Q i F są odpowiednio zbiorem stanów i zbiorem stanów akceptujących, i niech L będzie dowolnym językiem. Niech F ′ = { q ∈ Q ∣ ∃ y ∈ $M=(Q,\Sigma,\delta,q_0,F)$$R$$Q$$F$$L$ jest zbiorem stanów, z których końcowy stan może przyjmując ciąg z L .$F'=\{q\in Q\mid \exists y\in L \;\;\delta(q,y)\in F\}$$L$

Automat , który różni się od M tylko w jego zestawie F ' stanów końcowych rozpoznaje dokładnie R / l . (Lub zobacz Hopcroft-Ullman 1979, strona 62, aby uzyskać dowód na ten fakt.)$M'=(Q,\Sigma,\delta,q_0,F')$$M$$F'$$R/L$

Jednak gdy zbiór nie jest rozstrzygalny, może nie być algorytmu decydującego, które stany mają właściwość, która definiuje F ' . Tak więc, chociaż wiemy, że zbiór F ' jest podzbiorem Q , nie mamy algorytmu określającego, który podzbiór. W konsekwencji, choć wiemy, że R jest akceptowane przez jeden z 2 | Q | możliwe FSA, nie wiemy, co to jest. Chociaż muszę wyznać, że w dużej mierze wiemy, jak to wygląda.$L$$F'$$F'$$Q$$R$$2^{|Q|}$

Jest to przykład tego, co czasami nazywa się prawie konstruktywnym dowodem, który dowodzi, że jedna ze skończonej liczby odpowiedzi jest poprawna.

Przypuszczam, że rozszerzenie tego może być dowodem na to, że jedna z wymienionych odpowiedzi jest właściwa. Ale nie znam żadnego. Nie znam też czysto niekonstruktywnego dowodu, że jakiś problem jest rozstrzygalny, na przykład używając tylko sprzeczności.

Aby rozwinąć oryginalny komentarz Hendricka, rozważ ten problem

Biorąc pod uwagę liczbę całkowitą czy istnieje ciąg n lub więcej kolejnych 7s w rozszerzeniu dziesiętnym π ?$n\ge 0$$n$$\pi$

Problem ten jest rozstrzygalny, ponieważ w jednym z dwóch przypadków można uzyskać:

1. Istnieje liczba całkowita dla której rozwinięcie dziesiętne π zawiera ciąg $N$$\pi$$N$ kolejnych 7, ale już nie biegnie.
2. Dla dowolnego rozszerzenie π ma ciąg n kolejnych 7.$n$$\pi$$n$

W przypadku (1) algorytm decyzyjny dla problemu byłby jednym z

Jeśli odpowiedz „nie”, inaczej odpowiedz „tak”.$n > N$

aw przypadku (2) algorytm byłby

Odpowiedz „tak”.

Oczywiście każdy z nich jest algorytmem decyzyjnym; po prostu nie wiemy który. To wystarcza, choć od rozstrzygalności wymaga jedynie istnienie algorytmu, a nie specyfikacji których algorytm do użycia.

Oto brak odpowiedzi. Publikuję, ponieważ uważam, że jest to pouczające, ponieważ pierwotnie twierdziłem, że jest odwrotnie, a osiem osób wyraziło zgodę na głosowanie, zanim @sdcwc wskazał błąd. Nie chciałem po prostu edytować mojej pierwszej odpowiedzi, ponieważ nie jestem pewien, jak wiele osób zagłosowałoby za nią, gdyby wiedzieli, że to jest złe.

$S$$S$

$H$$H$