Is there an algorithm that provably exists although we don't know what it is?

Problem Detail: 

In mathematics, there are many existence proofs that are non-constructive, so we know that a certain object exists although we don't know how to find it.

I am looking for similar results in computer science. In particular: is there a problem that we can prove it is decidable without showing an algorithm for it? I.e. we know that it can be solved by an algorithm, but we don't know what the algorithm looks like?

Asked By : Erel Segal-Halevi

Answered By : babou

The simplest case I know of an algorithm that exists, though it is not known which algorithm, concerns finite state automata.

The quotient $L_1/L_2$ of a language $L_1$ by a language $L_2$ is defined as $L_1/L_2=\{x \mid \exists y\in L_2 \text{ such that } xy\in L_1\}$.

It is easily proved that regular set are closed under quotient by an arbitrary set. In other words, if $L_1$ is regular and $L_2$ is arbitrary (not necessarily regular), then $L_1/L_2$ is regular, too.

The proof is quite simple. Let $M=(Q,\Sigma,\delta,q_0,F)$ be a FSA accepting the regular set $R$, where $Q$ and $F$ are respectively the set of states and the set of accepting states, and let $L$ be an arbitrary language. Let $F'=\{q\in Q\mid \exists y\in L \;\;\delta(q,y)\in F\}$ be the set of states from which a final state can be reached by accepting a string from $L$.

The automaton $M'=(Q,\Sigma,\delta,q_0,F')$, which differs from $M$ only in its set $F'$ of final states recognizes precisely $R/L$. (Or see Hopcroft-Ullman 1979, page 62 for a proof of this fact.)

However, when the set $L$ is not decidable, there may be no algorithm to decide which states have the property that defines $F'$. So, while we know that the set $F'$ is a subset of $Q$, we have no algorithm to determine which subset. Consequently, while we know that $R$ is accepted by one of $2^{|Q|}$ possible FSA, we do not know which it is. Though I must confess we know to a large extent what it looks like.

This is an example of what is sometimes called an almost constructive proof, that is a proof that one of a finite number of answers is the right one.

I suppose an extension of that could be a proof that one of an enumerable set of answers is the right one. But I do not know any. Nor do I know a purely non-constructive proof that some problem is decidable, for example using only contradiction.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/32325