Non-constructive proofs vs. efficient algorithms - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-20T07:10:57Z http://mathoverflow.net/feeds/question/117574 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms Non-constructive proofs vs. efficient algorithms Sam Hopkins 2012-12-30T00:25:39Z 2013-04-05T08:17:41Z <p>My question concerns what is meant by "nonconstructive", and whether it has ever been defined in terms of computational complexity.</p> <p>The wikipedia article on <a href="http://en.wikipedia.org/wiki/Constructive_proof" rel="nofollow">constructive proof</a> begins, "a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object." On the other hand, the wiki article on <a href="http://en.wikipedia.org/wiki/Probabilistic_method" rel="nofollow">the probabilistic method</a> states, "the probabilistic method is a nonconstructive method [...] for proving the existence of a prescribed kind of mathematical object." I believe these two statements are at odds with one another.</p> <p>Consider Erdős's celebrated proof of the lower bound of the Ramsey number. This proof shows that as long as $\binom{n}{r} &lt; 2^{\binom{r}{2} - 1}$, there is some coloring of the edges of $K_n$ with $2$ colors that has no monochromatic sub-$K_r$. The proof offers no idea what such a coloring looks like; however, it <em>does</em> lead to a "method for creating" the object in question: try all possible colorings. The proof guarantees that this naive algorithm terminates. Of course, this algorithm quickly becomes computationally infeasible. But in principle, via exhaustive search, any proof of the existence of an object in some finite collection admits of a "method for creating" the object.</p> <p>Imagine now that we had a different proof of the lower bound of the Ramsey number. This new proof constructs two possible edge-$2$-colorings of $K_n$ and shows that at least one must result in no monochromatic sub-$K_r$, although it remains silent about which of the two colorings works. I think this would also qualify as a "non-constructive" proof (based on analogy to the wiki example with $\sqrt{2}^{\sqrt{2}}$), and yet it would lead to a wonderfully efficient method for finding such colorings. For any $r$, this hypothetical proof says we have to check only two candidates to get the object we're looking for. I think this even gives us a polynomial time algorithm for finding such a coloring (but this depends on how quickly we can verify a coloring.) At any rate, I hope the distinction I am trying to draw is clear.</p> <p>Does it makes sense to say that a constructive proof is a proof that leads to an efficient algorithm for creating an object with a desired set of properties? Has there been any work related to such a definition? The above is most relevant to statements in discrete math.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/117580#117580 Answer by Alexandre Eremenko for Non-constructive proofs vs. efficient algorithms Alexandre Eremenko 2012-12-30T02:07:56Z 2012-12-30T02:34:40Z <p>The terms "constructive" and "non-constructive" proofs have much wider application than discrete mathematics and algorithms for finite sets. And they can have have several meanings. A non-constructive proof proves that something exists but gives no way to construct the object. For example, one can prove existence of transcendentasl numbers by a simple countability argument. This proof does not give you a single example, it is non-constructive. And such proofs are actually abundant in mathematics. See, for example MR1852188 M. Kontsevich, D. Zagier, Periods. </p> <p>Liouville's proof of existence of transcendental numbers is constructive. Some results do not have any constructive proof at all, I mean the things related to Hahn-Banach. For example, every vector space has a basis. But you cannot really give an example of a basis of the vector space R over Q. By giving an example, I mean you define the set in the sense that for every number you can tell whether it is in the set or not.</p> <p>Another example, of different sort. There are famous theorems in number theory which say that certain inequalities or equations have finitely many solutions. But sometimes the proof does not tell in principle how to obtain ANY upper estimate. These are non-constructive proofs. Then people spend a lot of efforts to give an explicit estimate. Here constructive proofs sometimes exist, sometimes not. </p> <p>In Analysis, we all know that every continuous function on a compact set has a maximum. But there are plenty of interesting continuous functions on interesting compact sets, for which we know nothing else (how many maxima? Is the absolute maximum less than 10 or not, and don't know how to answer these questions). Here existence of a maximum is a typical non-constructive proof.</p> <p>In the beginning of XX century some mathematicians did not recognize non-constructive proofs as valid. In particular, they did not accept unlimited application of the axiom of choice. Some did not accept uncountable sets at all.</p> <p>This gave the origin to a kind of mathematics which in known under the names Constructive mathematics in USSR and Intuitionism elsewhere. Roughly speaking in Intuitionism only those existence proofs are recognized which give an algorithm to construct them. For example, in Intuitionist mathematics it is not always true that a bounded increasing sequence has a limit.</p> <p>If you are interested, there is a nice little book </p> <p>MR0075147 Heyting, A. Intuitionism. An introduction. North-Holland Publishing Co., Amsterdam, 1956. viii+133 pp.</p> <p>which gives a very readable introduction.</p> <p>When I was a student in 1970-s, some ordinary mathematicians (I mean non-logicians) in some places were still concerned with these issues.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/117600#117600 Answer by Yuichiro Fujiwara for Non-constructive proofs vs. efficient algorithms Yuichiro Fujiwara 2012-12-30T08:55:30Z 2012-12-30T09:23:27Z <p>Not a very serious answer, but maybe there is a little more than "how fast you can construct" to it when it comes to constructive proofs in some cases.</p> <p>A typical combinatorial design is often described as a set $\mathcal{B}$ (called <em>block</em> set) of subsets of some other set $V$ (called <em>point</em> set). The size of $V$ is the <em>order</em> of the design.</p> <p>If you use some probabilistic method to prove the existence of a design with certain properties, it's typically considered nonconstructive while good constructive proofs ideally give good algorithms to explicitly list the elements of $\mathcal{B}$ that satisfies the required conditions.</p> <p>Now it's not rare that it's easier to give a good constructive proof if order $\vert V \vert$ is prime because we have more combinatorial/algebraic/number theoretic tools. So you may be able to give a good constructive proof that for any prime order, there exists a design with the desired properties.</p> <p>One approach to solving the remaining cases (i.e., the case when the order is a composite number) is to give a certain product type construction, where if you have a pair of designs of order $v_0$ and $v_1$, you can systematically construct a new design with the desired properties of order $v_0v_1$. In other words, you prove that if there exist the kind of design you want of order $v_0$ and $v_1$, there also exists the same kind of design of order $v_0v_1$ by giving an algorithm. This way, in an ideal world, you can cover all possible orderes because you already have the kind of design you want for all prime orders.</p> <p>If everything worked out like magic, your construction for prime orders and product type one are both super fast algorithms that give explicit examples very quickly.</p> <p>Now you tell an engineer that you found super fast and explicit constructions for the kind of design he wanted. You say your proofs are perfectly constructive and very fast algorithms that work for any order he likes.</p> <p>The engineer gets excited and asks you to get him the design of $\vert V \vert = 12873891274647018937561708356916501047777612653914909670721635802187$ real quick. And you don't have a quantum computer to factor that number into primes yet.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/117615#117615 Answer by Aaron Meyerowitz for Non-constructive proofs vs. efficient algorithms Aaron Meyerowitz 2012-12-30T12:19:18Z 2012-12-30T12:19:18Z <p>Here is my very personal perspective, particularly as applied to the examples given. Constructive mathematics can be a technique of value to understanding. It is possible to use it sometimes and not others. Sometimes being constructive amounts to no more than more carefully examining what it is that your proof proves.</p> <p>The diagonal argument on reals <strong>really</strong> proves that given a countable list of real numbers it can not be that every real number is on the list. Less turgidly (but also less precisely) you give me the list and I will provided you a number not on the list, my exception will be provided to you as quickly as you provide the list. You must provide the members of the list as decimals (or at least appropriate nested intervals), however I will allow you to give the members of the list to a finite precision, say the $k$th accurate to $10^{-k}$. Thinking about that for a while you generalize to saying: Given a countable list of open intervals, each inside $(0,1)$, with the $k$th one of diameter $10^{-k}$, over $88\%$ of that interval is uncovered. I feel that I got an important insight into the difference between $\mathbb{Q}$ and the rest of $\mathbb{R}$ when I realized that, not only is there an irrational between every two rationals and vice versa, in fact we can cut out all the open intervals $(p/q-1/(2q)^3,p/q+1/(2q)^3)$ and still leave "most" of the real line behind. What is left is only irrational numbers and each one is actually <em>separated</em> from each rational. I would not have that insight unless I struggled with the "real" meaning of the diagonal argument.</p> <p>As I remarked, you don't have Erdős's probabilistic result quite right. The result is that when $\binom{n}{r} &lt; 2^{\binom{r}{2} - 1}$ there is a $2$-coloring of the edges of $K_n$ with no monochromatic $K_r$. So a graph with $5001$ vertices can be $2$-colored to avoid a monochromatic $K_{20}$. Of course there are over $12,500,000$ edges there so just getting a coloring would take a very long time, let alone checking it. Actually you could get close to $n=6000$. With $n=5000$ there is a better than $95\%$ chance that a "random" coloring will avoid a monochromatic $K_{20}.$ But if I tell you that I colored a random $K_{20}$ red and then colored the other edges randomly, you would have a very hard time deciding within a year if I was telling the truth.</p> <p>It is known that $n=\binom{38}{19} \gt 10^{10}$ is enough to be sure of a monochromatic $K_{20}.$ That would be a lot of edges.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/119562#119562 Answer by Peter for Non-constructive proofs vs. efficient algorithms Peter 2013-01-22T12:46:54Z 2013-01-22T12:46:54Z <p>As a personal view - there are lots of different meanings to 'constructive'. At one end, there is the distinction between objects which can be proven to exist in ZFC but not ZF (with finer distinctions if you like logic). At the other, one has the Erdos-idea of constructive, which isn't really formally defined but should certainly imply a polynomial time algorithm which further doesn't apply brute force checking in its running. In particular this excludes for example taking a Szemeredi partition of a graph and then brute-force testing the associated (bounded size) cluster graph for some property, even though this is a valid polynomial algorithm. And then there are all the shades in between - one definition of 'constructive' is 'I know it when I see it'.</p> <p>Usually the meaning of 'constructive' is just 'useful for my further proof' - so an object constructed via the axiom of choice will probably not come with any extra properties one can use to prove further facts, while an object which comes from some number-theoretical construction, even one which isn't polynomial-time constructible, usually comes with a host of extra facts one can use. And an object which has a nice cubic time algorithm to construct, but where the cubic algorithm uses brute force on a Szemeredi partition somewhere, is probably not easy to work with. A probabilistic construction is somewhere intermediate - if it's really an easy construction (take a random graph and with high probability it works) then you can read off a bunch of extra properties, but more complex constructions (nibble method, or local lemma, et cetera) don't necessarily keep properties and one has to check that the proof goes through with the extra conditions.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/124544#124544 Answer by katz for Non-constructive proofs vs. efficient algorithms katz 2013-03-14T17:43:53Z 2013-03-14T17:43:53Z <p>I would like to elaborate a bit on Alexandre Eremenko's answer. He cited Heyting's book on intuitionistic mathematics. From this point of view, the simplest definition of a constructive proof is a proof that does not rely on the Law of Excluded Middle (LEM for short). </p> <p>LEM is a key ingredient in every proof by contradiction. One may or may not agree with such a definition of constructive proof, but it's the most common one in the literature. To give an example, a probabilistic proof of the existence of a certain object will show that if there is no such object, a contradiction results. From this one customarily deduces that the object does exist. The step mentioned in the last sentence involves a use of LEM. To put it another way, if $P$ is a proposition, then in classical logic $\neg\neg P$ is the same as $P$. However, in an intuitionistic logic, they are different.</p> <p>Some constructive mathematicians have compared the suppression of LEM from the background logic, to the suppression of the axiom of commutativity in passing from abelian group theory to the theory of arbitrary groups. The argument is that sometimes the suppression of an axiom results in a more interesting theory. Whether or not this is the case for LEM is of course controversial.</p> http://mathoverflow.net/questions/117574/non-constructive-proofs-vs-efficient-algorithms/126582#126582 Answer by Kaveh for Non-constructive proofs vs. efficient algorithms Kaveh 2013-04-05T03:19:26Z 2013-04-05T08:17:41Z <p>As others have noted there are several different meanings for constructive. </p> <p>I. <strong>Constructive proof in the sense of constructive mathematics</strong></p> <p>This meaning views an object as existing if we have a description of how to <em>construct</em> the objects (though we don't really need to carry it out), and there are several distinct constructive views. Saying a proof is constructive or not can be ambiguous without specifying which school of constructive mathematics we are talking about. </p> <p>By the way, it can be the case that we can convert a non-constructive proof to a constructive one (Georg Kreisel's unwinding program or Ulrich Kohlenbach's <a href="http://en.wikipedia.org/wiki/Proof_mining" rel="nofollow">proof mining program</a>). That does <strong>not</strong> make the original proof constructive!</p> <p>Note that <em>algorithmic computability</em> is just one of several constructive perspectives. For example, in intuitionism there are objects which are <em>not</em> algorithmically computable. A way of understanding this is to remember that Churth-Turing thesis is not an axiom that is accepted by all constructivist, there can be constructions which are not algorithmic in the instuitionistic view.</p> <p>II. <strong>Constructive in the sense of complexity theory</strong></p> <p>This is a more recent meaning. We mean a proof of existence of an object is constructive if it gives directly a method of <em>efficiently</em> computing/constructing the object. This is the more common meaning of the word in combinatorics these days, e.g. in Robin A. Moser's <a href="http://arxiv.org/abs/0810.4812" rel="nofollow">"A constructive proof of the Lovasz Local Lemma"</a> paper from 2008.</p> <p>Constructive is used in the sense of efficient algorithms in complexity theory, for example, constructive in Alexander Razborov and Steven Rudich's "<a href="http://dx.doi.org/10.1006%252Fjcss.1997.1494" rel="nofollow">Natural Proofs</a>" paper means that the property used in the lower-bound proof is efficiently computable.</p> <p>Note that the proof itself can be non-constructive in the sense of meaning I while remaining constructive in this sense. You can give an efficient algorithm to compute some object and the correctness and efficiency proofs can be non-constructive. We don't have many interesting examples, but a good example would be <a href="http://en.wikipedia.org/wiki/Robertson%25E2%2580%2593Seymour_theorem#Polynomial_time_recognition" rel="nofollow">the Robertson-Seymour theorem</a>. See also <a href="http://cstheory.stackexchange.com/questions/12162/are-there-non-constructive-algorithm-existence-proofs" rel="nofollow">Are there non-constructive algorithm existence proofs?</a></p> <p>III. <strong>Proof complexity perspective</strong></p> <p>This is kind of the intersection of the previous two, though I don't recall anyone refer to it as "constructive proof" (probably because they are aware of both previous meanings and don't want to confuse people further :).</p> <p>Here not only the object should be computable efficiently but the correctness and efficiency proofs must use only efficient concepts. The Robertson-Seymour theorem is an example of an efficient algorithm where we don't have a proof using only efficient concepts. I can give more artificial examples to distinguish between this and the meaning in the previous section but I don't recall any other natural ones.</p>