[mafribe]

    Iterative loops are much easier to analyze and reason about,

This is not the case. Loops and recursion can be translated into each other, hence are of equal complexity in terms of reasoning. And you see that when you write down the Hoare-logic axioms for either.

What Dijkstra had in mind was probably simple, syntactically constrained forms of loops, like for-loops where the loop variable is read-only in the loop body. They are simpler than general recursion, sure. But there are corresponding simpler forms of recursion, e.g. primitive recursion or tail recursion that are much simpler than general recursion.

[AnimalMuppet]

> Loops and recursion can be translated into each other...

True.

> ... hence are of equal complexity in terms of reasoning.

False. That's like saying that Stokes' Theorem says that the integral of a differential form over the boundary of a manifold is equal to the integral of it's derivative over the whole manifold, and therefore the two integrals are equally easy to do. In fact, the two integrals are often not equally easy to do, which is the primary practical reason that we care about Stokes' Theorem - it gives us a way to convert hard integrals into easier ones.

You cannot use formal equivalence to prove practical ease of doing the problem.

But the situation isn't even that simple. A blanket statement that "loops are much easier to analyze and reason about" is also false. It depends on the situation, and often on who's doing the reasoning. Different people think in different ways.

[Jtsummers]

> You cannot use formal equivalence to prove practical ease of doing the problem.

Agree completely, but want to bring it back to another computing topic: Technically, anything that can be computed with one Turing-complete language can be computed with another. And every language clearly is not equivalent in terms of ease of understanding and reasoning about as every other language.

Trivially, compare computations in brainfuck to computations in C. Compare the recursive definition of tree traversal available in lisps to languages without recursion (some BASIC variants and others) where you have to jump through hoops and self-manage a stack.

[mafribe]

    compare computations in brainfuck to computations in C. 

I'd suggest that this is an orthogonal issue. It's better to compare two otherwise identical languages, one where Turing-completeness is achieved by loops, another where the same is done by recursion. (Or a language that offers both). Then formal reasoning is of the same complexity.

[mafribe]

    You cannot use formal equivalence to prove 

I'm afraid I have to disagree here. There is a mechanical translation from loops to recursion and back. Likewise, there is an associated mechanical translation from Hoare-triples and associated proofs for reasoning about loops to Hoare-triples and associated proofs for reasoning about recursion and back.

So in a hard way, the complexity of formal reasoning about the correctness of loops and recursion must be the same.

[AnimalMuppet]

That doesn't mean that the reasoning in a human brain is equally difficult, or equally error-prone. If nothing else, doing the transformations (and back) adds to the cognitive burden.

[mafribe]

That depends primarily on the programmer's experience, if you are used to loops but not recursion, then obviously the former is simpler than the latter, and vice versa. If you are equally familiar with both, they then thinking about it is equally difficult.

[rer0tsaz]

Yes, that is the point I tried to make. Use simple, constrained forms such as (C) "for(int i = 0; i < n; i++) { ... }" with n an int and no modification of i in the body, or (Python) "for e in l:" where l is a list that is not modified in the body. Then your code is very easy to analyze, not just in theory but also in practice for compilers, tools and people reading your code. Many language designers have realized this and provide special syntax for this very common case. I'm not aware of any language that has special syntax for primitive recursion, but it's an interesting idea.

My apologies for making an absolute statement with unclear terms, thus inviting uncharitable interpretations.

[mafribe]

I agree, that simple loops that you describe are easier to analyse than full recursion.

But simple loops are not as expressive as full loops (where you can modify the loop variable). As a simple example, try to phrase the Euclid's algorithm for computing the GCD using "for(int i = 0; i < n; i++) { ... }" where "i" is not modified in the loop body.

[rer0tsaz]

Just use n = max(a, b). Of course that doesn't help you much unless you're adhering to strict safety standards (e.g. power of ten rules), it just shifts the burden of proof from termination to correctness. And there's no such trick with the Ackermann function.

I'm really just advocating a rule of least power. Don't go into full general recursion just because you can.

[mafribe]

Why is this being down-voted? Could somebody please explain why they think what I wrote is wrong? I'd be happy to learn something new about loops and recursion.

[conceit]

Wasn't me, but it's probably because iterative loops are believed to be easier to reason about. OTOH the recursive definition for the Fibonacci or factorial numbers seem easier, for one because they map to the literal explanation.

[mafribe]

    iterative loops are believed to be easier to reason about.

This cannot be the case, because you can translate loops into recursion and vice versa, so every reasoning problem that one finds with loops is also a problem in reasoning about recursion and vice versa. If you look at the Hoare-logic rules this shows up clearly. In both case you need a suitably invariant, and you need a termination argument.

[conceit]

Does the translation come for free? If not, it's probably complicated to reason about.