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

71–80 of 88 posts

Re: Loop invariants can give you coding superpowers

#71

Post by jonsen »

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.

  -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.

Re: Loop invariants can give you coding superpowers

#72

Post by ramtatatam »

mabbo wrote: post #54
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…

I believe the superpower is the ability to prove correctness of the program easily. For most of us, this isn't a big deal. But let's say you're writing a subroutine that will control part of a pacemaker, rocket, fighter jet, satellite- anything where bugs are deadly or expensive- then this is a Very Big Deal.

But this comment does not prove the program will execute correctly, or does it?

Re: Loop invariants can give you coding superpowers

#73

Post by ramtatatam »

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?

Re: Loop invariants can give you coding superpowers

#74

Post by jacobajit »

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?

Test cases do not establish proof.

There could always be another rare edge case.

Re: Loop invariants can give you coding superpowers

#75

Post by BeetleB »

Someone wrote: post #66
BeetleB wrote: post #47

Earlier quoted context omitted.

Which floating point operator is not commutative? Addition is.

Technically, addition is mostly commutative (a phrase I just made up) in IEEE 754. On the one hand, we have: NaN + 1 = NaN 1 + NaN = NaN but we also have: NaN ≠ NaN , so that’s an example where a + b ≠ b + a

Heh. You got me thinking on that one!

I do know that with the floating point standard, NaN ≠ NaN returns True. But what does it mandate for NaN == NaN? Is this always false? If so, you're right. If not, I'd argue I'm still right, as that means that NaN + 1 == 1 + NaN would still be true.

Re: Loop invariants can give you coding superpowers

#76

Post by dbaupp »

jonsen wrote: post #62
dbaupp wrote: post #58

Earlier quoted context omitted.

That is due to associativity. You're implicitly relying on a consistent left-to-right evaluation order, but the fundamental problem can be phrased as (using s for small and b for big): (((b + s) + s) + s) + s Can be different to b + (s + (s + (s + s))) This re-parenthesising is related to associativity, not commutivity.

You're implicitly relying on a consistent left-to-right evaluation order, That’s standard, I think.

Indeed, it is standard, but eliding the parentheses doesn't mean they aren't implicitly there, and doesn't turn non-associativity into non-commutativity. Commutivity means that these are equal:

   (((b + s) + s) + s) + s
   ==
   s + (s + (s + (s + b)))

Re: Loop invariants can give you coding superpowers

#77

Post by [deleted] »

jonsen wrote: post #68
BeetleB wrote: post #65

Earlier quoted context omitted.

We are now lost in a semantic discussion, as it is clear that all parties agree on the content, just not the terminology. In that spirit, I will disagree. In mathematics, commutativity is always about two operands. My textbook on floating point arithmetic[1] (probably the most famous one) states that addition and multiplication in floating point is commutative. They use examples similar to yours as an example of asso…

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…

[deleted]

Re: Loop invariants can give you coding superpowers

#78

Post by dragonwriter »

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.

> How does this rely on associativity? It does not rely on parenthetical associativity.

It's exactly the combination of commutivity of addition, associativity of addition, and equivalence of subtraction with addition of the additive inverse, that allows the general rearrangement of symbols you are discussing.

Re: Loop invariants can give you coding superpowers

#79

Post by heartofgold »

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?

What jacobajit said. Or here's what Dijkstra said:

"Program testing can be used to show the presence of bugs, but never to show their absence!"

    Dijkstra (1970)

Re: Loop invariants can give you coding superpowers

#80

Post by smichel17 »

geoelectric wrote: post #55
skrebbel wrote: post #45

Earlier quoted context omitted.

Because it underlines that it's the sum of all elements seen so far. It does not just say "yo, this one here is the accumulator", it also implicitly defines the meaning of "accumulator" by saying "and the code that follows will guarantee that it is always the sum of the elements that have been seen so far". It's almost like a spec for the body of the combining function. I recognize that in a codebase where every 10 l…

I wonder if totalSoFar would be a good tradeoff of precision for conciseness. It's how you're consistently explaining it in plain English, which is a powerful indicator it might be adequate. I do normally call this sort of thing acc or accumulator though. I feel like an understanding of what that specific term means comes with the field expertise, sort of like we can say "LinkedList" and not "ObjectWithPointerToNextO…

I was thinking a similar thing, but with "runningSum"/"runningTotal".
Post reply on HN