# Are there non-constructive algorithm existence proofs?

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

1. $0^n$ occurs for every $n$ or
2. there is a $k$ so that $0^k$ occurs but $0^{k+1}$ does not.

We do not know which it is (yet), but we know that $f \in F = \{f_\infty, f_0, f_1, \dots \}$ with

1. $f_\infty(n) = 1$ and
2. $f_k(n) = [n \leq k]$.

Since $F \subset \mathsf{RE}$, $f$ is computable -- but we can not say what $f$ is.

• This answer is good, and so are the other answers. Evidently jkff's question has more than one answer, in the sense that there exist multiple proof technologies that can non-constructively demonstrate algorithm existence. – John Sidles Jul 30 '12 at 11:25
• I am, however, marking this one as "accepted" because it is by far the simplest one and demonstrates the core idea of how a non-constructive algorithm existence proof can arise. – jkff Jul 30 '12 at 16:09
• @jkff As simple as it is, it is a great exercise for students in intro TCS courses. It took me weeks to adjust my intuition/concept of computability in the light of this function. – Raphael Jul 30 '12 at 18:30
• I would be willing to bet a million dollars that $f$ is the constant 1 function. And I do not have a million dollars. – Daniel McLaury Mar 24 '16 at 1:14

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.

• That's cool! BTW, their algorithm matches the best running time in a decision tree model, right? – Sasho Nikolov Jul 29 '12 at 17:57
• Yes, that's right! – Jeffε Jul 29 '12 at 19:52
• In some sense, this sounds more like a higher-order function (it's a function that takes another function, and the proof of its time complexity depends on complexity of the input) than a non-constructive proof. I'd take non-constructive proof to mean anything that crucially invokes classical logic (LEM, DNE, or Peirce) in constructing its proof of the existence of the algorithm, without actually providing it. It's still cool, though. – copumpkin Aug 1 '12 at 21:03

Here are two examples.

1. 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.

2. 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.

• What is "finite obstruction for each case"? I think you mean "finite obstruction set for each infinite set of minor closed graphs" also remaining is not good (I edited your answer to fix it but seems rejected, I prefer to not repeating this). – Saeed Sep 26 '13 at 7:46

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:

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:

1. That for each problem there exists an algorithm to solve it.
2. That there is no way to construct these algorithms (in general).

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\}$

1. For each $M$ this is a finite set, and thus decidable.

2. 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.

• Cute. But the practical value of this may be less questionable than you think: this is a decision version of the problem of finding the shortest program with a given output, i.e. optimal data compression. – David Eppstein Aug 11 '12 at 20:05
• I think the example is similar to the one I gave. Note that when we are saying it is not-constructive we are interpreting the word constructive as recursive/computable which is one of the schools in constructivism. – Kaveh Aug 11 '12 at 22:45

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

• It is a different sense of "constructive". Sometimes complexity theorists (ab)use the word "constructive" to mean efficiently algorithmic, and in that context anything that is not efficiently algorithmic is referred to as non-constructive. This is different from the constructive proof notion intended in the question. – Kaveh Jul 31 '12 at 5:35
• Your first sentence is misleading. The algorithmic LLL is a is entirely constructive, in the sense of a polynomial time algorithm. The original LLL had a nonconstructive proof in the sense of being an inductive argument over a potentially huge probability space. Follow up work to Moser and Tardos's paper has closed practically all gaps between the algorithmic LLL and even some strengthening of LLL, see doi.acm.org/10.1145/1993636.1993669 – Sasho Nikolov Jul 31 '12 at 7:11
• the original lemma from 1975 was nonconstructive and later researchers (decades later) found constructive algorithms for special cases but "practically all gaps" is not the same as "all gaps". its a useful example to show that its not guaranteed that a nonconstructive existence proof will always stay that way, ie nonconstructivity is not always absolute and can be "subject to change", & that further/later research can close gaps, and that even whether all the gaps are closed by an algorithm can be subtle/difficult to prove. there are other examples of this. I cited Moser/Tardos solution. – vzn Jul 31 '12 at 14:46
• all i am saying is that the way you wrote your first sentence makes it look like the "algorithmic LLL" is "non-constructive". In that quote there was a reference to the original LLL, but that reference gets skipped because of where you put the ellipses. could you edit to include more of the quote so that it's not confusing? – Sasho Nikolov Jul 31 '12 at 18:03
• o/w i think your answer is only tangentially related to the topic, but it's a good point that some theorems with non-constructive proofs also admit constructive ones (and some provably don't, depending how you define "constructive"). btw one problem with taking the constructive LLL even further is that it's not clear how to define a reasonable computational problem in all situations where the LLL applies – Sasho Nikolov Jul 31 '12 at 18:07