I remember I might have encountered references to problems that have been proven to be solvable with a particular complexity, but with no known algorithm to actually reach this complexity.
I struggle wrapping my mind around how this can be the case; how a non-constructive proof for the existence of an algorithm would look like.
Do there actually exist such problems? Do they have a lot of practical value?
Consider the function (taken from here)
$\qquad \displaystyle f(n) = \begin{cases} 1 & 0^n \text{ occurs in the decimal representation of } \pi \\ 0 & \text{else}\end{cases}$
Despite the looks, $f$ is computable by the following argument. Either
We do not know which it is (yet), but we know that $f \in F = \{f_\infty, f_0, f_1, \dots \}$ with
Since $F \subset \mathsf{RE}$, $f$ is computable -- but we can not say what $f$ is.
This may not be exactly what you mean, but Seth Pettie and Vijaya Ramachandran's optimal minimum spanning tree algorithm is in some sense non-constructive.
It is an open question whether there is a deterministic algorithm to compute minimum spanning trees in linear (meaning $O(n+m)$) time. Pettie and Ramachandran describe an algorithm that computes MSTs in linear time if such an algorithm exists.
Intuitively, their algorithm reduces any $n$-vertex instance of the MST problem to $O(n/k)$ smaller instances with $O(k)$ vertices in linear time, where (say) $k = O(\log\log\log\log\log\log\log n)$. Then they compute the optimal comparison tree that computes the minimum spanning tree of any $k$-vertex graph by brute force enumeration; even if this takes quintuply exponential time in $k$, that's only $O(\log\log n)$ time. Finally, they solve the small instances using this optimal decision tree.
In other words, Pettie and Ramachandran construct an optimal MST algorithm only indirectly, by constructing an algorithm that constructs an optimal MST algorithm.
Here are two examples.
Some algorithms using the Robertson-Seymour theorem. The theorem states there exits a finite obstruction for each case, but does not provide a way to find such a finite set. Therefore, although we can prove that the algorithm exists, the explicit statement of the algorithm will depend on the finite obstruction set which we don't know how to find. In other words, we know there is an algorithm, but we don't know (yet) how to find one.
A stronger example, although less natural is essentially using PEM or similar non-constructive axioms. This is stronger in the sense that we can prove the constructive existence of an algorithm would imply a non-constructive axiom (similar to Brouwer's weak counter-examples). Such an example is stronger because it not only says that we don't know right now any explicit algorithm (or any algorithmic way of finding one), but also that there is no hope of doing so.
As an example, we can use PEM to prove an algorithm exists whereas we don't know which one and a constructive way of finding one would imply a non-constructive axiom. Let me give a simple example:
Halting problem is trivially decidable for each fixed Turing machine (each TM either halts or doesn't halt, and in each case there is a TM that outputs the right answer), but how can we find an algorithm solving the problem correctly without solving (the uniform version of) the halting problem?
More formally, we cannot prove constructively that given a TM $M$, there is a TM $H_T$ that decides the halting problem for $M$. More formally, the following statement cannot be proven constructively:
$$\forall e\in \mathbb{N} \ \exists f\in \mathbb{N} \ \left[ (\{f\}( \ )=0 \land \{e\}\mathord{\downarrow}) \lor (\{f\}( \ )=1 \land \{e\}\mathord{\uparrow}) \right]$$
Here $\{e\}$ is the TM with code $e$ (in some fixed representation of TMs), $\{e\}\mathord{\downarrow}$ means $\{e\}$ halts, and $\{f\}\mathord{\uparrow}$ means $\{f\}$ doesn't halt.
Yes.
At one point in (1), the complex-weighted counting graph homomorphism dichotomy theorem for any finite domain size, Cai, Chen, and Lu only prove the existence of a polynomial-time reduction between two counting problems via polynomial interpolation. I don't know of any practical value for such an algorithm.
See Section 4 of the arXiv version. The lemma in question is Lemma 4.1, called the "First Pinning Lemma".
One way to make this proof constructive is to prove the complex-weighted version of a result of Lovasz, namely:
For all $G$, $Z_H(G, w, i) = Z_H(G, w, j)$ iff there exists an automorphism $f$ of $G$ such that $f(i) = j$.
Here, $w$ is a vertex in $H$, $i$ and $j$ are vertices in $G$, and $Z_H(G, w, i)$ is the sum over all complex-weighted graph homomorphisms from $G$ to $H$ with the added restriction that $i$ must be mapped to $w$.
(1) Jin-Yi Cai, Xi Chen and Pinyan Lu, Graph Homomorphisms with Complex Values: A Dichotomy Theorem (arXiv) (ICALP 2010)
Some early results from late 80s:
Fellows and Langston, "Nonconstructive tools for proving polynomial-time decidability", 1988
Brown, Fellows, Langston, "Polynomial-time self-reducibility: theoretical motivations and practical results", 1989
From the abstract of the second item:
Recent fundamental advances in graph theory, however, have made available powerful new nonconstructive tools that can be applied to guarantee membership in P. These tools are nonconstructive at two distinct levels: they neither produce the decision algorithm, establishing only the finiteness of an obstruction set, nor do they reveal whether such a decision algorithm can be of any aid in the construction of a solution. We briefly review and illustrate the use of these tools, and discuss the seemingly formidable task of finding the promised polynomial-time decision algorithms when these new tools apply.
An example of an infinite family of problems (of questionable practical value) for which we can show:
In other words, a provably non-constructive proof. Our family of problem (from this question) for each Turing machine $M$:
$L_{M}=\Bigl\{\langle M'\rangle \;\Big|\;\; L(M)=L(M') \text{ and } |\langle M\rangle| \geq | \langle M' \rangle| \Bigr\} $
For each $M$ this is a finite set, and thus decidable.
If we had a constructive proof $P$ (in a suitable formal system) that given a description of a Turing Machine $M$ generated a Turing Machine $P(\langle M \rangle)$ that decided $L_M$ then given two machines $M$ and $M'$ (with $|\langle M \rangle | \geq |\langle M' \rangle|$) then we could test for equality of the languages recognized by these machines by running $P(\langle M \rangle)(\langle M' \rangle)$. An impossibility by Rice's theorem; thus, such a constructive proof $P$ does not exist.
From "Bidimensionality Theory and Algorithmic Graph Minor Theory Lecture Notes" for MohammadTaghi Hajiaghayi’s Tutorial, by Mareike Massow, Jens Schmidt, Daria Schymura and Siamak Tazari.
Each minor-closed graph property can be characterized by a finite set of forbidden minors.
Unfortunately, their result is “inherently” non-constructive, i.e. there is no algorithm that can generally determine which minors are to be excluded for a given minor-closed graph property. Moreover, the number of forbidden minors can be high: For example, for graphs embeddable on the torus more than 30,000 forbidden minors are known, yet the list is incomplete.
[...]
Each minor-closed graph property can be decided in polynomial time (even in cubic time).
Algorithmic Lovász local lemma -- "the algorithmic Lovász local lemma gives an algorithmic way of constructing objects that obey a system of constraints with limited dependence. ... However, the lemma is non-constructive in that it does not provide any insight on how to avoid the bad events." On some assumptions/limitations on the distribution, a constructed algorithm is given by Moser/Tardos[1]. the Lovasz local lemma seems to have various deep connections to complexity theory eg see [2]
[1] A constructive proof of the general Lovász Local Lemma by Moser,Tardos
[2] The Lov´asz Local Lemma and Satisfiability Gebauer, Moser, Scheder, Welzl
