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

61–70 of 88 posts

Re: Loop invariants can give you coding superpowers

#61

Post by jonsen »

dbaupp wrote: post #58
jonsen wrote: post #50

Earlier quoted context omitted.

(small number)+(small number)+ ... +(small number)+(much bigger number) may not give the same result as (much bigger number)+(small number)+(small number)+ ... +(small number)

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.

Rearranging operands with their operations is commuting. Rearranging parentheses is associating. Yes, floating point operations are also not in general associative.

Re: Loop invariants can give you coding superpowers

#62

Post by jonsen »

dbaupp wrote: post #58
jonsen wrote: post #50

Earlier quoted context omitted.

(small number)+(small number)+ ... +(small number)+(much bigger number) may not give the same result as (much bigger number)+(small number)+(small number)+ ... +(small number)

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.

Re: Loop invariants can give you coding superpowers

#63

Post by [deleted] »

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…

[deleted]

Re: Loop invariants can give you coding superpowers

#64

Post by jonsen »

thfuran wrote: post #60
jonsen wrote: post #22

Earlier quoted context omitted.

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

Why not just keep the implementation of the solution to any question you might be asked in your pocket?

A given pocket can contain many more invariants than implementations.

Re: Loop invariants can give you coding superpowers

#65

Post by BeetleB »

jonsen wrote: post #53
BeetleB wrote: post #51

Earlier quoted context omitted.

You are confusing associativity with commutativity. The IEEE floating point standard guarantees commutativity for addition.

I think you are confusing commutativity in general with commutativity of binary operations.

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 associativity being violated, and point out that commutativity is preserved.

Putting FP aside: In mathematics, no one disputes that addition is commutative. Yet, they all agree that for infinite sums, if you rearrange the order of the terms, you can get different results. They don't say that addition is commutative only for finite sums. They say it is commutative for all addition, and that associativity is the property that fails for infinite sums. See the discussion here[2] for example:

>The commutative property of addition is that a+b=b+a. Technically, it applies only to sums of two numbers!

>Actually, commutivity does hold for infinite sums. Glossing over a few technicalities, commutivity says that you get the same answer whenever you interchange any two terms in a sum.

Although I'll grant that when I look at some other answers in StackExchage, they do generalize to "repeated use of commutativity", and that if commutativity is applied a finite number of times, the sum is preserved, but not if applied an infinite number of times. The common refrain in both cases, though, is that commutativity applies only to two operands.

[1] https://www.springer.com/us/book/9780817647056

[2] https://math.stackexchange.com/questions/646665/why-does-com...

Re: Loop invariants can give you coding superpowers

#66

Post by Someone »

BeetleB wrote: post #47
whatshisface wrote: post #23

Earlier quoted context omitted.

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

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

Re: Loop invariants can give you coding superpowers

#67

Post by earthicus »

I don't think the utility of invariants is restricted to proving program correctness, as is suggested by a number of commenters in this thread. Instead, they identify some underlying structure in your problem, and that structure can be exploited to simplify your method of calculation.

Another great example of exploiting a (not-really-loop) invariant to design an algorithm is Sean Parent's implementation of a generic 'gather' algorithm, which takes advantage of the fact that the set of objects below/above the gathering point is unchanged, allowing you to split the problem into two easier sub-problems. Here's his explanation and implementation (video should be linked to 16:50):

https://youtu.be/IzNtM038JuI?t=1009

Re: Loop invariants can give you coding superpowers

#68

Post by jonsen »

BeetleB wrote: post #65
jonsen wrote: post #53

Earlier quoted context omitted.

I think you are confusing commutativity in general with commutativity of binary operations.

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 unfortunately lost in most modern math expositions.

Re: Loop invariants can give you coding superpowers

#69

Post by earthicus »

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've linked [1] to another example of exploiting an invariant that you might find more compelling. The presenter takes a multi-page mess of UI code from Chrome containing something like 8 loops, then solves an even harder version of that problem in ... 2 lines of code, by exploiting an invariant associated with the problem (and a well placed library call!).

[1] https://news.ycombinator.com/item?id=19567671

Re: Loop invariants can give you coding superpowers

#70

Post by 0815test »

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…

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.
Post reply on HN