4 ms·

Interestingly, I had never heard the phrase "loop invariant" despite having taken math courses on proofs and a lower-level (300-level, quicksort, etc) algorithm

Interestingly, I had never heard the phrase "loop invariant" despite having taken math courses on proofs and a lower-level (300-level, quicksort, etc) algorithms course. I'm curious. Is this like a "supper vs dinner" or "pop vs soda" variation that depends on the region your university is located?

dill_day 12y ago
I wouldn't guess so, for example it's used in the CLRS textbook. What did you call it instead?
- 27182818284 12y ago
  I don't remember it ever being named. It isn't the same as the "inductive step" when learning proofs by induction, is it?
  - deleted 12y ago
    [deleted]
  - williadc 12y ago
    In the linked article, the author points to an explanation of loop invariants. Click the link "Last Week"
  - casion 12y ago
    I understand your confusion, because the author didn't properly cover what he's talking about. It appears to be written to teach people who already know the material. In the previous article, the closest thing to an explanation or definition of a loop invariant is, "We can make it less so by writing down a specific claim that applies to our particular loop. Such a claim is called a loop invariant." Not a very good description, and he doesn't try to do any better elsewhere. I ended up having to do a bunch of googling after reading the articles to piece together what is trying to be explained, since I had never heard of loop invariants in that terminology either. Simply put, a loop invariant is a condition or set of conditions that is true through the loop. This makes it akin to inductive proofs. The loop invariant must prove true for n and n+1 for it to be true for the entirety of the loop. Noting how similar this is to inductive reasoning, you can apply an inductive proof to a loop invariant to prove it. The easiest way I've seen to explain it is in the body of the executing loop you ask yourself, "What has the loop done so far." An answer to that question should yield a loop invariant.
vilhelm_s 12y ago
Maybe? There is a sort of cultural split in theoretical computer science between "A theory" (algorithms and complexity) and "B theory" (logic/semantics/program verification).[1] And these in turn are sortof geographically divided, with complexity being popular in the US and logic in Europe. The concept of loop invariants comes from the program verification tradition, I guess it gets less emphasis when focusing on complexity. [1] http://cstheory.stackexchange.com/questions/1521/origins-and-applications-of-theory-a-vs-theory-b http://cstheory.stackexchange.com/questions/1521/origins-and...
toolslive 12y ago
It used to be the standard way of teaching control structures. "so you want to write a 'while' loop? Then what's the invariant?". Also, the invariant is the best comment/documentation you can add to a complex loop.
Roboprog 12y ago
I went to a little school in the CSU system in the 80s, but at least one of our professors used the term "loop invariant" (as well as induction) in our freshman "Pascal" class. I admit I liked the recursive version of the author's example better, though, especially when he gets into "oldr" and "newr" to track the mutated state of things in each loop pass. Along a similar line, I remember reading on my own about Eiffel and "class invariants" in the very early 90s. Then came the internet gold rush to dumb things down, though. Now, we have King Java and its idiotic "bean" anti-pattern. Just make a useless crap object, whack on it enough (mutate it) until you hope it's in a useful state and slog onward! State of the art brain damage :-(

dill_day 12y ago

I wouldn't guess so, for example it's used in the CLRS textbook. What did you call it instead?

27182818284 12y ago
I don't remember it ever being named. It isn't the same as the "inductive step" when learning proofs by induction, is it?
- deleted 12y ago
  [deleted]
- williadc 12y ago
  In the linked article, the author points to an explanation of loop invariants. Click the link "Last Week"
- casion 12y ago
  I understand your confusion, because the author didn't properly cover what he's talking about. It appears to be written to teach people who already know the material. In the previous article, the closest thing to an explanation or definition of a loop invariant is, "We can make it less so by writing down a specific claim that applies to our particular loop. Such a claim is called a loop invariant." Not a very good description, and he doesn't try to do any better elsewhere. I ended up having to do a bunch of googling after reading the articles to piece together what is trying to be explained, since I had never heard of loop invariants in that terminology either. Simply put, a loop invariant is a condition or set of conditions that is true through the loop. This makes it akin to inductive proofs. The loop invariant must prove true for n and n+1 for it to be true for the entirety of the loop. Noting how similar this is to inductive reasoning, you can apply an inductive proof to a loop invariant to prove it. The easiest way I've seen to explain it is in the body of the executing loop you ask yourself, "What has the loop done so far." An answer to that question should yield a loop invariant.

vilhelm_s 12y ago

Maybe? There is a sort of cultural split in theoretical computer science between "A theory" (algorithms and complexity) and "B theory" (logic/semantics/program verification).[1] And these in turn are sortof geographically divided, with complexity being popular in the US and logic in Europe. The concept of loop invariants comes from the program verification tradition, I guess it gets less emphasis when focusing on complexity. [1] http://cstheory.stackexchange.com/questions/1521/origins-and-applications-of-theory-a-vs-theory-b http://cstheory.stackexchange.com/questions/1521/origins-and...

toolslive 12y ago

It used to be the standard way of teaching control structures. "so you want to write a 'while' loop? Then what's the invariant?". Also, the invariant is the best comment/documentation you can add to a complex loop.

Roboprog 12y ago

I went to a little school in the CSU system in the 80s, but at least one of our professors used the term "loop invariant" (as well as induction) in our freshman "Pascal" class. I admit I liked the recursive version of the author's example better, though, especially when he gets into "oldr" and "newr" to track the mutated state of things in each loop pass. Along a similar line, I remember reading on my own about Eiffel and "class invariants" in the very early 90s. Then came the internet gold rush to dumb things down, though. Now, we have King Java and its idiotic "bean" anti-pattern. Just make a useless crap object, whack on it enough (mutate it) until you hope it's in a useful state and slog onward! State of the art brain damage :-(