Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Loop invariants can give you coding superpowers

yourbasic.org

Post reply on HN
Print view View original

21–30 of 88 posts

Re: Loop invariants can give you coding superpowers

#21

Post by hooya »

GuiA wrote: post #10

The article describes the concept of a loop invariant and gives examples for a few algorithms, but unless I am missing something, it is not giving you any way to computationally verify those invariants? (I guess I am a bit surprised by the short length of this article because when I write code, I tend to think of it in those terms already, so I expected it to go further; but I guess not everyone has been exposed to t…

check out: https://en.wikipedia.org/wiki/Formal_methods

I ran into loop invariants in my CS undergrad where they were teaching "formal logic" to prove correctness of programs. At the time, it was a bit above my head and i struggled with it. i'm just beginning to understand what it was that we were studying at the time. cool stuff. wish i could go back and re-learn that stuff. Also google TLA+ - there's a book on it by Leslie Lamport.

Re: Loop invariants can give you coding superpowers

#22

Post by jonsen »

0x8BADF00D wrote: post #15
raincom wrote: post #7

Is there a list of loop invariants for algorithms that are frequently used in interviews?

Not sure what you mean by your comment. You can use loop invariants when solving problems that call for an iterative solution.

“Can you write code to reverse a linked list in place?”

“Sure, I’ll just implemment a loop according to this invariant ... “

Would be nice to have the invariant ready then.

Re: Loop invariants can give you coding superpowers

#23

Post by whatshisface »

ummonk wrote: post #14
skrebbel wrote: post #12

I think there's an opportunity to name variables after their invariant. For example, in the typical sum example, the mutated variable is usually called "sum" or "total". But you could also call it sum_from_0_to_i, and then a reader can immediately see that the result is the full sum because i equals the array length. It's like a proof-by-variable-name. The same trick tends to work as well with less trivial invariants…

I mean generally I tend to prefer operations that are commutative and associative, so it really doesn't matter which one is the accumulator. But I still really like your naming, it seems to bridge the gap in making reduces (which are conceptually cleaner) understandable to people who are used to iterative code.

Floating point sums are one example of a place where the only usable operator doesn't commute.

Re: Loop invariants can give you coding superpowers

#24

Post by [deleted] »

jonsen wrote: post #19
robotresearcher wrote: post #17

The article has invariants in comments. I like to put invariants in assertions so they get checked at run time. I know this is common practice but I haven’t seen it mentioned here and it might help someone. edit: Jonsen's reply question, for which I don't have an answer, is instructive: these loop invariants are often impossible or impractical to achieve in assertions. I modified the above to be less wrong.

How would write an assert for the sum loop invariant?

[deleted]

Re: Loop invariants can give you coding superpowers

#25

Post by maweki »

jonsen wrote: post #16
maweki wrote: post #9

I think both for sum and max a better invariant should include the uncalculated part. Sum(0..X)=Sum(0..i)+sum(i+1..X) with the moving i. So it is true at first because the unsummed part is empty and the missing part is the goal. Then we take away an i from the solution to-go pile and put it on the done pile and when the loop has done X the to-do pile is enpty and per invariant the done pile equals the goal. Including…

You are merging the invariant with the variant . The loop invariant is supposed to tell about the state of the variant at any loop start. The variant in this case is the tupple (i,sum). Your version does not say anything about the stepwise evaluation of the sum.

Of course this tells me about the state of the variant. And it's the same invariant the author uses but with the equation balanced differently.

The author's invariant is Sum = 1+2+..I Mine is Sum+(I+1)+...+X = 1+2+..I+(I+1)+...+X

That's both fine and tells us about I. I think the version that contains the value we want to obtain is easier to prove correctness for.

Re: Loop invariants can give you coding superpowers

#27

Post by raincom »

0x8BADF00D wrote: post #15
raincom wrote: post #7

Is there a list of loop invariants for algorithms that are frequently used in interviews?

Not sure what you mean by your comment. You can use loop invariants when solving problems that call for an iterative solution.

Loop variants for popular problems and popular algorithms to solve problems. This can give us inductive way of looking various problems. And classify problems/algos based on invariants.

Re: Loop invariants can give you coding superpowers

#28

Post by asark »

To sum (haha) up, I am no n00b.

However, I've looked over the page a couple times and still can't figure out the use of this, let alone what "superpowers" it may grant. It's just comments? The best parts I can see are the mostly-prose ones farther down that just say what the loop's supposed to do, but even those are just repeating the "input" and "output" info, really, which are sort of also comments I think. Some of this might be useful if you could express it in types or some other machine-checkable fashion, but in comments they're just kind of redundant and, like any comments, must be treated with suspicion anyway.

What am I missing? I just have no idea what I'm looking at here, or rather I think I do but I'm entirely missing why it should be in any sense exciting which leads me to think maybe I don't.

Re: Loop invariants can give you coding superpowers

#30

Post by 0815test »

Loop invariants are a lot more intuitive if you convert your loops into while() form and then further into tail recursion - they turn into a proof by induction.

For the first example, consider:

  go (n, i, sum): given sum = 1 + 2 + ... + i-1 returns (1 + 2 + ... + n) :
    per cases of (i  (sum + i) = 1 + 2 + ... + i)
        return go (n, i + 1, sum + i);
      } else assume (i > n) {
        note: thus i = n + 1
        then: sum = 1 + 2 + ... + i - 1 = 1 + 2 + ... + n
        return sum;
      }

  sum n: returns 1 + 2 + ... + n = {
    note: 0 = 1 + 2 + ... + (1 - 1)
    // ^^^ Need to prove our precondition for go!
    return go (n, 1, 0);
  }
The other examples are a bit more complex for sure, but structurally similar. It's nonetheless easy to see how even very limited changes in complexity (such as the choice of loop indexing) can create quite a few pitfalls for truly rigorous proof!
Post reply on HN