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

81–88 of 88 posts

Re: Loop invariants can give you coding superpowers

#81

Post by fizixer »

asark wrote: post #28

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…

It's a badly written post. That's what you're missing.

In the first example, author didn't even indicate what the loop invariant is in the code, before moving on to a second example.

Re: Loop invariants can give you coding superpowers

#83

Post by mabbo »

ramtatatam wrote: post #73
mabbo wrote: post #56

I think what many commenters are missing is why this is important. Invariants like this allow one to prove the correctness of their code. That may not seem like a big deal most of the time, but imagine you're working on a satellite that's going to Jupiter, where a bug in the code could mean 10 years from now a billion dollar project gets scuttled. Imagine you're building subroutines that will go into 10,000 pacemaker…

To prove the correctness of your code you would write tests in similar way as SQLite does, no? They have, like, 100x more lines of code for tests than actual code they test?

Unit tests demonstrate correctness. That's another useful tool in the tool box. But proofs are more than just that.

Imagine trying to unit test all possible cases of Pythagorean theorem being correct vs a single proof in a few lines of descriptive logic.

Re: Loop invariants can give you coding superpowers

#84

Post by JadeNB »

jonsen wrote: post #57
BeetleB wrote: post #52

Earlier quoted context omitted.

If I read you right, you are saying that if you compute a+b, you'll get a different result than if you compute b+a, if a is tiny and b is huge. I believe this is incorrect. Feel free to show me a counterexample.

a + b commutes all right, but some-start-value +a +b ... +x does not necessarily.

As rhimenoceros points out, that is a failure of associativity, not commutativity.

Re: Loop invariants can give you coding superpowers

#85

Post by dllthomas »

0815test wrote: post #70
jonsen wrote: post #68

Earlier quoted context omitted.

Take subtraction. The binary operator - is not commutative in the sense that a - b is not equal to b - a. But a - b commutes to - b + a. Any number of +or-with-operand can be arranged in any order. This is commutativity in general. See the start of Chapter 1 in Part 1: https://onlinebooks.library.upenn.edu/webbin/book/lookupid?k... This is a very practical semantics of commutativity when programming. It’s unfortunate…

But this relies on associativity - without associativity, you just don't have a consistent definition of e.g. (a + b + c + d) but only, e.g. + + + / \ / \ / \ + + a + a + / \ / \ / \ / \ a b c d + d b + / \ / \ b c c d and others as well. There would be practically no point in trying to find a definition of "commutative" for these structures that don't involve associativity.

I think there may be a mismatch in terminology here.

Above, "associativity" was used in the sense of "the property that any re-association produces the same answer". It's used that way when talking about properties of an operation, often in an algebraic context.

I think you're using it in the sense of "an understanding of how operands should be associated". It's often used that way when describing a language in practice, like "(+) is right-associative".

If we're going to be working with expressions like (a + b + c), then whenever + is not (sense 1) associative we clearly need some understanding about what that expression means. But we can restrict ourselves to dealing with fully-parenthesized expressions and not need any sort of "this associates to the left", and still properties like associativity and commutativity can be interesting.

In the case of your trees, associativity means any trees with the same ordering in the leaves (with an in-order traversal) must be equivalent. Commutativity means any trees that differ by swapping the left/right children of a parent node must be equivalent. You can have neither property, either property, or both properties.

Re: Loop invariants can give you coding superpowers

#86

Post by [deleted] »

jonsen wrote: post #71
0815test wrote: post #70

Earlier quoted context omitted.

But this relies on associativity - without associativity, you just don't have a consistent definition of e.g. (a + b + c + d) but only, e.g. + + + / \ / \ / \ + + a + a + / \ / \ / \ / \ a b c d + d b + / \ / \ b c c d and others as well. There would be practically no point in trying to find a definition of "commutative" for these structures that don't involve associativity.

-6-7-8 == -8-7-6 == -7-8-6 == ... How does this rely on associativity? It does not rely on parenthetical associativity. The operator is of course associated with an operand, but that’s not what is meant by associativity.

[deleted]

Re: Loop invariants can give you coding superpowers

#87

Post by newen »

40acres wrote: post #26

Udi Manber's book on algorithms and induction is also a great resource to learn about invariants. Invariants and induction go hand in hand.

Great book. Much better than CLRS for learning. Coming from a math background, this book made learning algorithms easy for me.

Re: Loop invariants can give you coding superpowers

#88

Post by raincom »

hackermailman wrote: post #8

Lot's of material around on invariants for anybody interested Cornell: Invariants Playlist: https://www.youtube.com/playlist?list=PLTD_NtzzD4VC6l2uLdzbsm9wW21mMaWwj http://www.cs.cornell.edu/courses/cs2110/2017sp/online/loops/01aloop1.html https://www.cs.cornell.edu/courses/cs1110/2018sp/materials/loop_invariants.pdf CMU: https://www.cs.cmu.edu/~15122/handouts/01-contracts.pdf http://www.cs.cmu.edu/%7Efp/courses/1512…

http://cseweb.ucsd.edu/classes/sp05/cse101/JeffEdmondsBook.p... Jeff Edmonds' "How to Think About Algorithms: Loop Invariants and Recursion" is a nice book.
Post reply on HN