Böhm-Jacopini theorem

Question

According to Böhm-Jacopini theorem, an algorithm can be written using only three statements:

• sequence
• selection
• iteration

Lots of teachers, assumes that theorem as an act of faith, and they teach to not use (goto, jump, break, multiple return, etc...) because these instructions are evil.

But when I ask for an explanation, no one is able to provide a proof of theorem.

Personally I don't think that the theorem is false, but I think that it's applicability in real world is not always the better choice.

So I've done a my little search, and these are my doubts:

1. The theorem has been proven on induction on the structure of the flow chart, but it's really applicable in a computer program?
   According to wikipedia "Böhm and Jacopini's was not really practical as a program transformation algorithm, and thus opened the door for additional research in this direction".

2. A consequence of theorem prove that each "goto" can be translated into selection or iteration by induction, but what about efficiency? I can't find any proof shows that each algorithm can be rewritten preserving the same performance.

3. Recursion, a recursive algorithm can really be written using only sequence, selection and iteration? I know that some recursive algorithms can be optimized as loops (think to tail recursion), but can really be applicable to all?

4. Clean code, I know that an abuse of jumps can create a monstrous code, but I think in some case a correct use of break in a loop can improve the code readability.

Sample:

n = 0;
while (n < 1000 || (cond1 && cond2) || (cond3 && cond4) || (cond5 && cond6)) 
{  
   n++;  
   //The rest of code  
}   

Can be rewritten as :

for (n = 0; n < 1000; n++)
{
   if (cond1 && cond2) break;
   elseif (cond2 && cond3) break;
   elseif (cond4 && cond5) break;
   elseif (cond6 && cond7) break;
   //The rest of code
}

Personally I think that the theorem has not been created for write better code, and the idea that a clean code must follow this theorem has been spread into world for a strange subjective reason.

5. I found this interesting article : https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf I think this prove that real program must not be forced to follow the Jaopini Theorem.
   Do you share the same conclusions?

Summarizing the question, I need to know if a program that uses only (sequence, selection and iteration) is really better than any other that uses different statements, and if there are proves or if it's all subjective.

Heisenberg

Since virtually all programming languages have constructs beyond those in the Böhm-Jacopini paper, I don't see how anyone is "forced to follow the Jaopini Theorem". Gotos have been discussed ad nauseum since Dijkstra's original diatribe. The consensus is that they (or some more structured version like break or continue) have a place but that Dijkstra has largely won the war. The Böhm-Jacopini theorem had little to do with it (beyond providing a response to those programmers who claimed that gotos were needed in an absolute sense). The success of structured programming is what convinced. – Annunciator

Thanks @JohnColeman, aboutt Dijkstra diatribe I've found this interesting article with all original references. In particular I've found particular interesting this article of Donald E. Knuth that shows how controlled use of goto is not entirely harmful. – Heisenberg

Answer 1

The theorem has been proven on induction on the structure of the flow chart, but it's really applicable in a computer program? According to wikipedia "Böhm and Jacopini's was not really practical as a program transformation algorithm, and thus opened the door for additional research in this direction".

The operations and structure they give can easily be shown capable of replicating the function of a Turing machine. As such, it is a Turing-equivalent system of computation. By the Church-Turing thesis, this is believed to be as much computation as we can do: goto would add nothing that is not already possible.

A consequence of theorem prove that each "goto" can be translated into selection or iteration by induction, but what about efficiency? I can't find any proof shows that each algorithm can be rewritten preserving the same performance.

Performance is very likely worse for many algorithms without the use of computed goto. You can certainly show it is the case for specific problems. Whether this changes the asymptotic complexity or not is another question but not one Bohm and Jacopini have to do with as far as I am aware.

Recursion, a recursive algorithm can really be written using only sequence, selection and iteration? I know that some recursive algorithms can be optimized as loops (think to tail recursion), but can really be applicable to all?

Since Bohm and Jacopini's system is Turing equivalent, then you are correct, recursion adds no new power. It may certainly add readability.

Hyps

Thanks @Hyps I'll wait some days before accept this as an answer to see if anyone can provide a more complete explanation. – Heisenberg

Answer 2

According to Böhm-Jacopini theorem, an algorithm can be written using only three statements:

• sequence
• selection
• iteration

The While language has the following constructs:

1. Assignment, V := E
2. Empty program, skip
3. Sequence, S1;S2
4. Selection, if B then S1 [elsif Si] else Sn fi, and
5. Iteration. while B do S od

You omitted the assignment and skip, which is a neutral element, like the 0 in arithmetic. There are other structures which I have omitted. Those have to do with Procedural abstraction, which names sequences of statements, i.e. functions and procedures. But I don't want extend this too much now.

I found this interesting article : https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf I think this prove that real program must not be forced to follow the Jacopini Theorem. Do you share the same conclusions?

Kozen is a very good author, he is rigorous and clear.

Kozen showed a limitation of propositional calculus in proving the Böhm-Jacopini theorem. The original article used predicate calculus. He gives a correct proof of the theorem using techniques not available in the 1960s. The problem arise because the transformation use variables, something that can not be handled within propositional calculus. Other transformation exists, which use a loop with breaks instead of the While language. All that discussion about GOTO is now well understood. The article is interesting because it is an example on how to use the newer techniques in an old well known problem.

You can use the Böhm-Jacopini theorem, because it produces an equivalent program.

Personally I don't think that the theorem is false, but I think that it's applicability in real world is not always the better choice.

That result supports structured programming. But you should not use it because you should not use data-flow diagrams to design programs. You should not even use While pseudo-code to design programs.

The best practice is to use an abstract specification language which is more adequate to represent the problem that you want to solve. Prove your solution and then write a document that can be transformed into your programming language code. That is the idea behind literate programming. Explain precisely what you know about the domain of the problem, state how you represent your problem in an abstract specification language, and transform it systematically into the programming language. All the explanation should in natural language and math formulas, and the pieces of code should be separable to produce the program code. For that you can use a program like CWeb and LaTeX.

The new declarative languages are very close to specification languages, but better stick to the above advice. Although those languages infer types, some times the details in the data structures are distracting in the design process. Later the types should be detailed in order to implement the program in a statically typed programming languages. That is a better programming practice.

Madrid

Answer 3

Any program that looks like Type 1 /2 /3 can be transformed to

Intransitive

Answer 4

Personally I think that the theorem has not been created for write better code,

Well, it never was. The theorem wasn't created (theorems aren't just created). The theorem was found as a model of computation, as a way to demonstrate that a GOTO statement is not an absolute necessity for coding an algorithm.

We need to understand the context in which the theorem was first proposed. At the time, programmers were using GOTO rather savagely and without structure, adamantly believing that GOTO statements were essential.

The theorem demonstrates that this is not the case. Now, the theorem doesn't mean that a program structured by it is inevitably superior (as there are cases where deviation from the proposed structure is the better/more elegant/efficient way to go.)

What the theorem served back then was as the nail in the coffin to the argument that GOTO statements were a must for creating complex programs (they aren't.)

The greatest benefit from the theorem is that it offered a new (and in the general case, better) way to formulate, analyze and codify algorithms.

and the idea that a clean code must follow this theorem has been spread into world for a strange subjective reason.

In the general case, this is true, and for no subjective reason. The theorem is the basis for structured programming, and in general, this has been much better than its predecessor alternatives.

I repeat myself, the whole thing about the theorem is that FOR THE GENERAL CASE

1. you do not need to rely on GOTO for sequential logic
2. sequential logic can be uniformly described by this method
3. the resulting codification of sequential logic can be formally analyzed (try that with a GOTO soup.)

This is how the theorem is supposed to be looked at, objectively speaking.

Sericeous