Can an algorithm be part of a proof?

Question

I am an undergraduate student. I have read several papers in graph theory and found something may be strange: an algorithm is part of a proof. In the paper, except the last two sentences, other sentences describe a labeling algorithm.

Can an algorithm be part of a proof? I do not understand why it can be part of a proof. I asked my supervisor but he did not explain it.

LEMMA$\,\,\,\bf 1.$ If $B(G)-b$, then $B(G+e)<2b$.

Proof: Let $f$ be an optimal numbering of $G$, and let $V(G)-\{v_1,\ldots,v_n\}$, numbered so that $f(v_i)-i$. Let $v_lv_m$ be the added edge. We define a new numbering $f'$ such that $|f'(x)-f'(y)|<2|f(x)-f(y)|$, and also $|f'(v_l)-f'(v_m)|-1$. Let $r-\lfloor(l+m)/2\rfloor$, and set $f'(v_r)-1$ and $f'(v_{r+1})-2$. For every other $v_i$ such that $|i-r|<\min\{r-1,n-r\}$, let $f'(v_i)-f'(v_{i+1})+2$ if $i<r$ and $f'(v_i)-f'(v_{i-1})+2$ if $i>r$. This defines $f'$ for all vertices except a set of the form $v_i,\ldots,v_k$ or $v_{n+1-k},\ldots,v_n$, depending on the sign of $r-\lfloor(n+1)/2\rfloor$. In the first case, we assign $f'(v_i)-n+1-i$ for $i<k$; in the second, we assign $f'(v_i)-i$ for $i>n-k$. The renumbering $f'$ numbers the vertices outward from $v_r$ to achieve $|f'(x)-f'(y)|<2|f(x)-f(y)|$. Since we begin midway between $v_l$ and $v_m$, we also have $|f'(v_l)-f'(v_m)|-1$.

Answer 1

Yep! Proofs sometimes involve elaborate calculations: presenting an algorithm to do the calculation is a good way to show that the calculation can be done, and to analyze the results of the calculation.

In some fields -- e.g. graph theory -- algorithms are used very frequently. Often, the easiest way to prove that something can be done is to actually write down an algorithm that does it, and prove the algorithm works.

You might think of this approach as a systematic and convenient way to develop and organize complicated inductive proofs. But I would actually think of it the other way: induction is just a rather simplistic kind of algorithm for generating a proof. i.e. the algorithm is "use the argument I called the "base case" to prove it for one $1$, then iteratively apply the argument I called the "inductive step" to prove it for each successive positive integer".

Answer 2

I confess that I have not read the paragraph enclosed (which contains some unexplained notation; anyway I am not an expert on graph theory), so this is an answer to your general question.

Absolutely yes an algorithm can be part of a proof. In certain situations (and for those with certain inclinations) an algorithm can be the best possible kind of proof. Let me give a simpler example.

In my linear algebra class recently I told the students that any permutation of $\{1,\ldots,n\}$ can be obtained as a composition of transpositions -- i.e., swapping two elements at a time. This is not an obvious fact if you haven't thought about it before. What was my proof? Well, I said that in fact you can choose the transpositions to be adjacent elements, and then I told the students that the easiest way to see this is to think about how to actually do it in practice. It is easy to give an algorithm: start with the element that you want to go in the $n$th place. If it's there already, great. If it isn't, then keep making a sequence of adjacent swaps bringing it one step closer to the $n$th position every time. Do this until it gets into the $n$th position. Now we can view what we have left as a permutation of $\{1,\ldots,n-1\}$ and work by induction.

The above argument is definitely an algorithm: it is something that a CS student would have little trouble programming. And it is a convincing proof. What's convincing about it of course is that you can see why the algorithm is doing what it's supposed to do. We could write it more formally if we wanted to, as a global induction argument, and then we could use the well-ordering principle to argue that moving the element one step closer each time to where it wants to go means that it will eventually get there, but that seems like overkill in the present case.

In summary: an algorithm can definitely be part of a proof, but except for completely trivial cases an algorithm -- written in the form that a computer would accept, for instance -- should not be the entirety of the proof. The other important part is an explanation for why the algorithm is doing what it is claimed to do. Sometimes that's simple; sometimes it isn't. There are in fact some amazing theorems that say (roughly) in general it is impossible to figure out what an algorithm will do, so the algorithms that are part of proofs need to be of the relatively simple kind whose workings can be explained to a human being.

Afterthought: By the way, "When is an algorithmic proof preferred and when is a pure thought/existence proof preferred?" would be a fantastic question, in my opinion.

Answer 3

The proof shows how to renumber the vertices with the integers $1,\ldots,n$ in such a way that $|f\,'(v_\ell)-f\,'(v_m)|=1$, where $e=v_\ell v_m$ is the new edge, and $$|f\,'(x)-f\,'(y)|\le 2|f(x)-f(y)|$$ for each edge $xy$ of $G$. You have to think through the construction to see that it actually does this, but that’s not too hard to do. This shows that $G+e$ has a numbering $f\,'$ such that

$$\max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2\max_{xy\in E(G)}|f(x)-f(y)|\;,\tag{1}$$

where $E(G)$ is the set of edges of $G$.

I assume from the context that $B(G)$ is the minimum over all numberings $g$ of $$\max_{xy\in E(G)}|g(x)-g(y)|\;;$$ $f$ is a numbering that achieves this minimum. Thus, $(1)$ shows that $G+e$ has a numbering $f\,'$ such that

$$\max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2B(G)\;.$$

It follows that if $f''$ is an optimal numbering, meaning one that achieves the minimum possible value of

$$\max_{xy\in E(G)\cup\{e\}}|g(x)-g(y)|\;,$$

then

$$B(G+e)=\max_{xy\in E(G)\cup\{e\}}|f''(x)-f''(y)|\le \max_{xy\in E(G)\cup\{e\}}|f\,'(x)-f\,'(y)|\le 2B(G)\;,$$

which is what the lemma claims.

It’s true that this renumbering scheme can be thought of as an algorithm, but that’s really beside the point: the real point is that it makes clear to the reader why the lemma is true, which is precisely what a proof is supposed to do. It’s also true that just describing the scheme doesn’t fill in all of the details of the proof; as I said, you still have to convince yourself that it works as stated. But that’s true of all proofs outside of the very limited realm of formal theorem-proving: you always have to fill in some of the details for yourself.

Answer 4

Here is a short answer to the question in your title. Typically, when one gives a constructive proof, in essence, the constructive argument forms the algorithm. An example that comes to my mind is again from combinatorics: Stable marriage theorem. The easiest way to prove the existence of a stable marriage is to provide an algorithm to construct one.

Answer 5

By the Curry-Howard correspondence, any logical proposition in intuitionistic logic can be taken as the type signature of a lambda calculus expression. Equivalently one might use combinators rather than lambdas, and have one combinator corresponding to each logical axiom or inference rule.

Lambda calculus with types is powerful enough to be a real programming language; indeed there are several programming languages in use today which are little more than lambda calculus with additional types such as machine integers and efficient data structures, and a healthy dose of syntactic sugar.

Lambda calculus is also turing complete, meaning you can use a turing machine for a proof of a logical statement too.

Therefore, an algorithm (which has been proven correct) is a proof.

Answer 6

If you ask me, I would say that everything can be part of a proof as long as you bring a convincing reasonable argument. When I listen to my colleagues topologist, they make a few drawings (generally sketches of knots) on the blackboard and they claim it's a proof. Thus, a drawing or an algorithm, there is no big difference, the most important at the end of the day is that you are sure of what you assert, and leave nothing in the darkness.

Have a nice day :-)