<p>This may not be <em>exactly</em> what you mean, but Seth Pettie and Vijaya Ramachandran's <a href="http://www.cs.utexas.edu/~vlr/papers/optmsf-jacm.pdf">optimal minimum spanning tree algorithm</a> is in some sense non-constructive.</p>

<p>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 <em>if such an algorithm exists</em>.</p>

<p>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 <strong>the optimal comparison tree</strong> 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.</p>

<p>In other words, Pettie and Ramachandran construct an optimal MST algorithm only indirectly, by constructing an algorithm that constructs an optimal MST algorithm.</p>

CC BY-SA 3.0
2012-07-29T17:57:27.393Z
That's cool! BTW, their algorithm matches the best running time in a decision tree model, right?
Sasho Nikolov
CC BY-SA 3.0
2012-07-29T19:52:24.133Z
Yes, that's right!
Jeffε
CC BY-SA 3.0
2012-08-01T21:03:45.713Z
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
CC BY-SA 3.0
2012-07-29T16:36:42.340Z
2012-07-29T16:36:42.340Z
Jeffε
<p>Here are two examples.</p>

<ol>
<li><p>Some algorithms using <a href="http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem#Polynomial_time_recognition">the Robertson-Seymour theorem</a>. 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.</p></li>
<li><p>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 <a href="http://en.wikipedia.org/wiki/Constructive_proof#Brouwerian_counterexamples">Brouwer's weak counter-examples</a>). Such an example is stronger because it not only says that we don't <em>know right now</em> any explicit algorithm (or any algorithmic way of finding one), but also that there is no hope of doing so.</p>

<p>As an example, we can use <a href="http://en.wikipedia.org/wiki/Principle_of_excluded_middle">PEM</a> 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: </p>

<p>Halting problem is trivially decidable for each <em>fixed</em> 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? </p>

<p>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:</p>

<p>$$\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]$$</p>

<p>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.</p></li>
</ol>

CC BY-SA 3.0
2013-09-26T07:46:13.690Z
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
CC BY-SA 3.0
2012-07-31T05:56:48.830Z
2012-07-31T05:56:48.830Z
Kaveh
<p>Yes.</p>

<p>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.</p>

<p>See Section 4 of the arXiv version.  The lemma in question is Lemma 4.1, called the "First Pinning Lemma".</p>

<p>One way to make this proof constructive is to prove the complex-weighted version of a <a href="http://www.sciencedirect.com/science/article/pii/S0195669805000788" rel="nofollow">result of Lovasz</a>, namely:</p>

<p>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$.</p>

<p>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$. </p>

<p>(1) Jin-Yi Cai, Xi Chen and  Pinyan Lu, Graph Homomorphisms with Complex Values: A Dichotomy Theorem (<a href="http://arxiv.org/abs/0903.4728" rel="nofollow">arXiv</a>) (<a href="http://www.springerlink.com/content/46275700132p5250/" rel="nofollow">ICALP 2010</a>)</p>

CC BY-SA 3.0
2012-07-29T13:38:28.910Z
2012-07-31T11:53:47.183Z
2012-07-31T11:53:47.183Z
Tyson Williams
<p>Some early results from late 80s: </p>

<ul>
<li><p>Fellows and Langston, "<a href="http://dl.acm.org/citation.cfm?doid=44483.44491">Nonconstructive tools for proving polynomial-time decidability</a>", 1988</p></li>
<li><p>Brown, Fellows, Langston, "<a href="http://www.tandfonline.com/doi/abs/10.1080/00207168908803783">Polynomial-time self-reducibility: theoretical motivations and practical results</a>", 1989 </p></li>
</ul>

<p>From the abstract of the second item:</p>

<blockquote>
  <p>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. </p>
</blockquote>

CC BY-SA 3.0
2012-07-30T22:16:40.293Z
2012-08-02T11:19:40.457Z
2012-08-02T11:19:40.457Z
vzn
<p>An example of an infinite family of problems (of questionable practical value) for which we can show:</p>

<ol>
<li>That for each problem there exists an algorithm to solve it.</li>
<li>That there is no way to construct these algorithms (in general).</li>
</ol>

<p>In other words, a provably non-constructive proof. Our family of problem (from <a href="https://cs.stackexchange.com/q/3090/55">this question</a>) for each Turing machine $M$:</p>

<p>$L_{M}=\Bigl\{\langle M'\rangle \;\Big|\;\; L(M)=L(M') \text{ and } |\langle M\rangle| \geq | \langle M' \rangle| \Bigr\} $ </p>

<ol>
<li><p>For each $M$ this is a finite set, and thus decidable. </p></li>
<li><p>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.</p></li>
</ol>

CC BY-SA 3.0
2012-08-11T20:05:02.857Z
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
CC BY-SA 3.0
2012-08-11T22:45:19.180Z
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
CC BY-SA 3.0
2012-08-11T20:01:18.213Z
2012-08-11T20:01:18.213Z
2017-04-13T12:48:30.830Z
Artem Kaznatcheev
<p>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.</p>

<p>Each minor-closed graph property can be characterized by a finite set of forbidden minors.</p>

<p>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.</p>

<p>[...]</p>

<p>Each minor-closed graph property can be decided in polynomial time (even in cubic time).</p>

CC BY-SA 3.0
2012-07-30T21:16:03.380Z
2012-07-30T21:16:03.380Z
Pål
<p><a href="http://en.wikipedia.org/wiki/Algorithmic_Lov%C3%A1sz_local_lemma" rel="nofollow">Algorithmic Lovász local lemma</a> -- "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]</p>

<p>[1] <a href="http://arxiv.org/abs/0903.0544" rel="nofollow">A constructive proof of the general Lovász Local Lemma</a> by Moser,Tardos</p>

<p>[2] <a href="http://www.inf.ethz.ch/personal/gebauerh/lllsat.pdf" rel="nofollow">The Lov´asz Local Lemma and Satisfiability</a> Gebauer, Moser, Scheder, Welzl</p>

CC BY-SA 3.0
2012-07-31T05:35:20.587Z
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
CC BY-SA 3.0
2012-07-31T07:11:47.170Z
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 http://doi.acm.org/10.1145/1993636.1993669
Sasho Nikolov
CC BY-SA 3.0
2012-07-31T14:46:31.013Z
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
CC BY-SA 3.0
2012-07-31T18:03:23.947Z
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
CC BY-SA 3.0
2012-07-31T18:07:49.277Z
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
CC BY-SA 3.0
2012-07-30T22:37:07.627Z
2012-07-30T22:42:17.073Z
2012-07-30T22:42:17.073Z
vzn
<p>Consider the function (taken from <a href="https://cs.stackexchange.com/q/367/98">here</a>)</p>

<p>$\qquad \displaystyle f(n) = \begin{cases} 1 &amp; 0^n \text{ occurs in the decimal representation of } \pi \\ 0 &amp; \text{else}\end{cases}$</p>

<p>Despite the looks, $f$ is computable by the following argument. Either</p>

<ol>
<li>$0^n$ occurs for every $n$ or</li>
<li>there is a $k$ so that $0^k$ occurs but $0^{k+1}$ does not.</li>
</ol>

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

<ol>
<li>$f_\infty(n) = 1$ and</li>
<li>$f_k(n) = [n \leq k]$.</li>
</ol>

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

CC BY-SA 3.0
2012-07-30T11:25:39.030Z
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
CC BY-SA 3.0
2012-07-30T16:09:41.000Z
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
CC BY-SA 3.0
2012-07-30T18:30:21.587Z
@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
CC BY-SA 3.0
2016-03-24T01:14:34.700Z
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
CC BY-SA 3.0
2012-07-30T08:52:55.277Z
2012-07-30T08:52:55.277Z
2017-04-13T12:48:30.830Z
Raphael
<p>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.</p>

<p>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.</p>

<p>Do there actually exist such problems? Do they have a lot of practical value?</p>

CC BY-SA 3.0
2012-07-29T07:18:33.113Z
algorithms based on [the Robertson-Seymour theorem](http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem#Polynomial_time_recognition)? Or more simply, using PEM to prove an algorithm exists where we don't know which one (halting problem is trivially decidable for each fixed Turing machine, but how can we find an algorithm solving the problem correctly without solving (the uniform version of) the halting problem?) ps: what do you mean by "practical value"?
Kaveh
CC BY-SA 3.0
2012-07-29T13:38:07.117Z
Common in practice is the converse problem: we are given an algorithm (commonly source code) and an assurance (commonly empirical) that it runs correctly within a certain complexity class, and yet it commonly happens that we cannot feasibly prove that the algorithm runs correctly or that it belongs to that complexity class. The question of whether such "cryptic" algorithms exist in an absolute sense is open, and is the subject of "[Does P contain languages whose existence is independent of PA or ZFC?](http://cstheory.stackexchange.com/q/11691/1519)", which is a TCS Community wiki.
John Sidles
CC BY-SA 3.0
2012-07-29T15:56:25.370Z
Why, there are also [simpler examples](http://cs.stackexchange.com/q/367/98).
Raphael
CC BY-SA 3.0
2012-07-29T16:06:38.930Z
Raphael, it seems to me that [your comment](http://cstheory.stackexchange.com/questions/12162/are-there-non-constructive-algorithm-existence-proofs#comment33391_12162) might plausibly be upgraded to an answer.  Perhaps you (or someone) might attempt this?
John Sidles
CC BY-SA 3.0
2012-07-29T16:43:08.197Z
Raphael, I agree, please upgrade your comment to an answer. It's a very good example.
jkff
CC BY-SA 3.0
2012-07-29T17:52:49.117Z
Kaveh and Raphael give the same example btw (in Kaveh's comment PEM = principle of excluded middle)
Sasho Nikolov
CC BY-SA 3.0
2012-07-29T21:43:35.083Z
I think this is a possible duplicate of [Are there problems without efficient algorithms, where existence theorems have proved such algorithms must exist?](http://cstheory.stackexchange.com/q/4777/1037)
Artem Kaznatcheev
CC BY-SA 3.0
2012-07-30T08:53:39.940Z
@JohnSidles,jkff Done. (Note that using `@name` notifies the user you talk to.)
Raphael
CC BY-SA 3.0
2012-08-02T11:12:19.043Z
I removed 4 non-constructive comments. Please don't use comments for expressing opinions on other things. For information about usage of comments please see [this](http://cstheory.stackexchange.com/privileges/comment).
Kaveh
CC BY-SA 3.0
2016-08-29T14:13:03.697Z
This is [on Wikipedia now](https://en.wikipedia.org/wiki/Non-constructive_algorithm_existence_proofs).
Raphael
CC BY-SA 4.0
2022-11-04T20:41:05.583Z
[This paper](https://www.sciencedirect.com/science/article/pii/S0890540108001570) by Martín Escardó and Ho Weng Kin contains a proof that some program exists; and this proof is *necessarily* non-constructive (the program depends on some parameters, but can't be computed from them) because of an undecidability result. Escardó explains this further in these Twitter threads:
https://twitter.com/EscardoMartin/status/1580631501527343105
https://twitter.com/EscardoMartin/status/1580639421111549952
Lê Thành Dũng 'Tito' Nguyễn
CC BY-SA 4.0
2024-11-14T13:48:50.557Z
Let A be the set of integers that have a certain property P. Suppose that I have proved that A is finite and nonempty but nobody knows any members of A nor #A. Let N = max A. Then, the problem "What is N?" is solved by the program "Print(N)". Can I say that I have provided a non-constructive algorithm for the problem? And that it runs in constant time?
If not, what is the difference?
Indeed, to me all answers here look a bit like that.
Convexity
<ds.algorithms><soft-question><lo.logic><proofs>
Are there non-constructive algorithm existence proofs?
jkff
# Are there non-constructive algorithm existence proofs?

(Asked by: username_0 on 2012-07-29)

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?

**Tags:** ds.algorithms, soft-question, lo.logic, proofs
> **Comments:**
> **username_1**: algorithms based on [the Robertson-Seymour theorem](http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem#Polynomial_time_recognition)? Or more simply, using PEM to prove an algorithm exists where we don't know which one (halting problem is trivially decidable for each fixed Turing machine, but how can we find an algorithm solving the problem correctly without solving (the uniform version of) the halting problem?) ps: what do you mean by "practical value"?  
> **username_2**: Common in practice is the converse problem: we are given an algorithm (commonly source code) and an assurance (commonly empirical) that it runs correctly within a certain complexity class, and yet it commonly happens that we cannot feasibly prove that the algorithm runs correctly or that it belongs to that complexity class. The question of whether such "cryptic" algorithms exist in an absolute sense is open, and is the subject of "[Does P contain languages whose existence is independent of PA or ZFC?](http://cstheory.stackexchange.com/q/11691/1519)", which is a TCS Community wiki.  
> **username_3**: Why, there are also [simpler examples](http://cs.stackexchange.com/q/367/98).  
> **username_2**: Raphael, it seems to me that [your comment](http://cstheory.stackexchange.com/questions/12162/are-there-non-constructive-algorithm-existence-proofs#comment33391_12162) might plausibly be upgraded to an answer.  Perhaps you (or someone) might attempt this?  
> **username_0**: Raphael, I agree, please upgrade your comment to an answer. It's a very good example.  
> **username_4**: Kaveh and Raphael give the same example btw (in Kaveh's comment PEM = principle of excluded middle)  
> **username_5**: I think this is a possible duplicate of [Are there problems without efficient algorithms, where existence theorems have proved such algorithms must exist?](http://cstheory.stackexchange.com/q/4777/1037)  
> **username_3**: @JohnSidles,jkff Done. (Note that using `@name` notifies the user you talk to.)  
> **username_1**: I removed 4 non-constructive comments. Please don't use comments for expressing opinions on other things. For information about usage of comments please see [this](http://cstheory.stackexchange.com/privileges/comment).  
> **username_3**: This is [on Wikipedia now](https://en.wikipedia.org/wiki/Non-constructive_algorithm_existence_proofs).  
> **username_6**: [This paper](https://www.sciencedirect.com/science/article/pii/S0890540108001570) by Martín Escardó and Ho Weng Kin contains a proof that some program exists; and this proof is *necessarily* non-constructive (the program depends on some parameters, but can't be computed from them) because of an undecidability result. Escardó explains this further in these Twitter threads: https://twitter.com/EscardoMartin/status/1580631501527343105 https://twitter.com/EscardoMartin/status/1580639421111549952  
> **username_7**: Let A be the set of integers that have a certain property P. Suppose that I have proved that A is finite and nonempty but nobody knows any members of A nor #A. Let N = max A. Then, the problem "What is N?" is solved by the program "Print(N)". Can I say that I have provided a non-constructive algorithm for the problem? And that it runs in constant time? If not, what is the difference? Indeed, to me all answers here look a bit like that.  

---

## 8 answers

### Answer by username_3 on 2012-07-30. Score: 41 | Accepted answer

Consider the function (taken from [here](https://cs.stackexchange.com/q/367/98))

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

> **Comments:**
> **username_2**: 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.  
> **username_0**: 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.  
> **username_3**: @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.  
> **username_15**: I would be willing to bet a million dollars that $f$ is the constant 1 function.  And I do not have a million dollars.  

---

### Answer by username_8 on 2012-07-29. Score: 28

This may not be *exactly* what you mean, but Seth Pettie and Vijaya Ramachandran's [optimal minimum spanning tree algorithm](http://www.cs.utexas.edu/~vlr/papers/optmsf-jacm.pdf) 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.

> **Comments:**
> **username_4**: That's cool! BTW, their algorithm matches the best running time in a decision tree model, right?  
> **username_8**: Yes, that's right!  
> **username_9**: 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.  

---

### Answer by username_1 on 2012-07-31. Score: 13

Here are two examples.

1. Some algorithms using [the Robertson-Seymour theorem](http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem#Polynomial_time_recognition). 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](http://en.wikipedia.org/wiki/Constructive_proof#Brouwerian_counterexamples)). 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](http://en.wikipedia.org/wiki/Principle_of_excluded_middle) 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.

> **Comments:**
> **username_10**: 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).  

---

### Answer by username_11 on 2012-07-29. Score: 8

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](http://www.sciencedirect.com/science/article/pii/S0195669805000788), 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](http://arxiv.org/abs/0903.4728)) ([ICALP 2010](http://www.springerlink.com/content/46275700132p5250/))


---

### Answer by username_12 on 2012-07-30. Score: 7

Some early results from late 80s:

* Fellows and Langston, "[Nonconstructive tools for proving polynomial-time decidability](http://dl.acm.org/citation.cfm?doid=44483.44491)", 1988
* Brown, Fellows, Langston, "[Polynomial-time self-reducibility: theoretical motivations and practical results](http://www.tandfonline.com/doi/abs/10.1080/00207168908803783)", 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.


---

### Answer by username_5 on 2012-08-11. Score: 6

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](https://cs.stackexchange.com/q/3090/55)) 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.

> **Comments:**
> **username_13**: 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.  
> **username_1**: 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.  

---

### Answer by username_14 on 2012-07-30. Score: 3

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


---

### Answer by username_12 on 2012-07-30. Score: 0

[Algorithmic Lovász local lemma](http://en.wikipedia.org/wiki/Algorithmic_Lov%C3%A1sz_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](http://arxiv.org/abs/0903.0544) by Moser,Tardos

[2] [The Lov´asz Local Lemma and Satisfiability](http://www.inf.ethz.ch/personal/gebauerh/lllsat.pdf) Gebauer, Moser, Scheder, Welzl

> **Comments:**
> **username_1**: 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.  
> **username_4**: 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 http://doi.acm.org/10.1145/1993636.1993669  
> **username_12**: 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.  
> **username_4**: 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?  
> **username_4**: 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  

---

