Existe-t-il un algorithme qui existe de manière prouvée même si nous ne savons pas ce que c'est?

En mathématiques, il existe de nombreuses preuves d'existence non constructives, nous savons donc qu'un certain objet existe bien que nous ne sachions pas comment le trouver.

Je recherche des résultats similaires en informatique. En particulier: y a-t-il un problème que nous pouvons prouver qu'il est décidable sans lui montrer d'algorithme? C'est-à-dire que nous savons qu'il peut être résolu par un algorithme, mais nous ne savons pas à quoi ressemble l'algorithme?

Le cas le plus simple que je connaisse d'un algorithme qui existe, bien que l'on ne sache pas quel algorithme, concerne les automates à états finis.

Le quotient d'une langue L 1 par une langue L 2 est défini comme L 1 / L 2 = { x ∣ ∃ y ∈ L 2  tel que  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\}$

Il est facile de prouver que les ensembles réguliers sont fermés sous quotient par un ensemble arbitraire. En d'autres termes, si est régulier et L 2 est arbitraire (pas nécessairement régulier), alors L 1 / L 2 est régulier aussi.$L_1$$L_2$$L_1/L_2$

La preuve est assez simple. Soit un FSA acceptant l'ensemble régulier R , où Q et F sont respectivement l'ensemble des états et l'ensemble des états accepteurs, et soit L un langage arbitraire. Soit F ′ = { q ∈ Q ∣ ∃ y ∈ $M=(Q,\Sigma,\delta,q_0,F)$$R$$Q$$F$$L$ l'ensemble des étatspartir desquels un état final peut être atteint en acceptant une chaîne de L .$F'=\{q\in Q\mid \exists y\in L \;\;\delta(q,y)\in F\}$$L$

L'automate , qui diffère de M seulement dans son ensemble F ' d'états finaux reconnaît précisément R / L . (Ou voir Hopcroft-Ullman 1979, page 62 pour une preuve de ce fait.)$M'=(Q,\Sigma,\delta,q_0,F')$$M$$F'$$R/L$

Cependant, lorsque l'ensemble n'est pas décidable, il peut ne pas y avoir d'algorithme pour décider quels états ont la propriété qui définit F ' . Ainsi, alors que nous savons que l'ensemble F ' est un sous-ensemble de Q , nous n'avons pas d'algorithme pour déterminer quel sous-ensemble. Par conséquent, alors que nous savons que R est accepté par l'un des 2 | Q | possible FSA, nous ne savons pas de quoi il s'agit. Bien que je dois avouer que nous savons dans une large mesure à quoi cela ressemble.$L$$F'$$F'$$Q$$R$$2^{|Q|}$

Ceci est un exemple de ce que l'on appelle parfois une preuve presque constructive , c'est-à-dire une preuve qu'un nombre fini de réponses est la bonne.

Je suppose qu'une extension de cela pourrait être une preuve que l'un d'un ensemble énumérable de réponses est la bonne. Mais je n'en connais pas. Je ne connais pas non plus de preuve purement non constructive qu'un problème est décidable, par exemple en utilisant uniquement la contradiction.

Pour développer le commentaire original de Hendrick, considérez ce problème

$n\ge 0$$n$$\pi$

Ce problème est décidable, car l'un des deux cas peut obtenir:

1. $N$$\pi$$N$
2. $n$$\pi$$n$

Dans le cas (1), un algorithme de décision pour le problème serait l'un des

$n > N$

et dans le cas (2) l'algorithme serait

Répondez "oui".

Il est clair que chacun d'eux est un algorithme de décision; nous ne savons simplement pas lequel. Cela suffit, cependant, puisque décidabilité ne nécessite que l' existence d'un algorithme, et non la spécification qui algorithme à utiliser.

Voici une non-réponse. Je poste parce que je pense que c'est instructif, parce que j'avais à l'origine affirmé le contraire et huit personnes étaient suffisamment d'accord pour voter avant que @sdcwc ne signale l'erreur. Je ne voulais pas juste modifier ma première réponse parce que je ne suis pas sûr que beaucoup de gens l'auraient votée s'ils savaient que c'était faux.

$S$$S$

$H$$H$