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

41–50 of 88 posts

Re: Loop invariants can give you coding superpowers

#41

Post by bjourne »

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…

What the page presents is a tool for producing mathematical proofs. Proofs are really useful for mathematicians for with them you can derive lots of truths about mathematical objects. For example, it is true that if q^2 = 2, then q is not a rational number.

In the same way, using the tool on the page you can prove that 1. the while-loop terminates. 2. the invariants hold, meaning that your program is correct. Yes, you can encode the proof in a machine-checkable format but that is missing some of the point. Just like with mathematical proofs, the major use of the proof is to communicate with humans.

Also the same techniques used to prove invariants by hand can be used by compilers to implement smart optimizations. In the sum example, the compiler could deduce/prove that sum = \sum_{i=1}^n i and replace the loop body with n(n+1)/2. I don't know if any compilers do such advanced optimizations but theoretically they could (in trivial cases like these - in general, proving properties about code is as hard as solving the halting problem).

Other proof techniques involve finding upper and lower limits of variables which are used to store values in more efficient types. For example, storing an integer as an int32 instead of int64.

To really understand what's going on read https://en.wikipedia.org/wiki/Hoare_logic. The article's proof uses Hoare logic but implicitly, without the notation, so understanding how the proofs work is hard.

Re: Loop invariants can give you coding superpowers

#42

Post by Jtsummers »

asark wrote: post #34
repler wrote: post #32

Earlier quoted context omitted.

You're not missing anything - it's 100/200 level computer science. (Freshman/Sophomore)

Yeah I'm just getting "if the loop can be expressed as induction you can... write that in a comment, for some reason". Alright, that's nice. Could we express that as tests instead plzkthx? So I thought I must be missing something.

Another place to use this is if you're designing a new bit of code and want to write the design out before you write the code, rather than code first (or as the code is being produced, where at times it's non-executable because you have holes in the program that are filled with these textual descriptions).

You could put some of these into asserts or similar. Like for the three way partition. Create an assert that at each iteration the array[:low] values are all less than p, array[high:] values are each greater than p, and array[low:mid] values are each equal to p. If it doesn't hold then you know your code is wrong. This does induce a performance hit, but asserts can be turned off for deployed code.

Re: Loop invariants can give you coding superpowers

#43

Post by 0815test »

bjourne wrote: post #41
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…

What the page presents is a tool for producing mathematical proofs. Proofs are really useful for mathematicians for with them you can derive lots of truths about mathematical objects. For example, it is true that if q^2 = 2, then q is not a rational number. In the same way, using the tool on the page you can prove that 1. the while-loop terminates. 2. the invariants hold, meaning that your program is correct. Yes, yo…

> using the tool on the page you can prove that 1. the while-loop terminates

Not quite. Proving that a while loop terminates is usually done by establishing a loop variant - intuitively, a claim that the inputs to the loop become "smaller" in some sense, i.e. closer to some exit condition/base case, with each iteration of the loop. Loop invariants don't suffice on their own.

Re: Loop invariants can give you coding superpowers

#44

Post by Jtsummers »

lkuty wrote: post #5

Learned that and the "weakest precondition" stuff from Pierre-Arnoul de Marneffe in 1994 at the University of Liège (ULg). Very useful but we didn't grasp the full power of it at that time.

We had a course at Georgia Tech called "Introduction to Proofs" or something for the CS students that introduced these as well. But it was so early in our education and so separated from the programming courses that it wasn't obvious to most of us how it'd be used. It wasn't until much later that I understood these ideas and could apply them. It needed to be better integrated into the other courses (to provide motivating examples of these methods and techniques).

Re: Loop invariants can give you coding superpowers

#45

Post by skrebbel »

kyle-rb wrote: post #31
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…

Why is 'totalUpToPrevious' better than 'sum' or 'total'? I could see it being good for explaining what a reduce does, but once you know how they work, 'sum' tells you exactly which argument is the accumulator.

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 lines there's a reduce or something similar this may not be necessary, in the exact same way that nobody names a C style loop index variable "current_index". But I find that, even in many functional languages, reduces and custom recursive functions aren't that common because the libraries include so many batteries.

Re: Loop invariants can give you coding superpowers

#46

Post by skrebbel »

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.

I find that few practical folds have that property. I mean, you're not going to actually implement "sum" - there's a library function for that. Your reduces are going to be domain specific, and then order often matters, and explicitly accumulating the result on the left (or right) hand side often has a performance impact (eg when building lists).

Re: Loop invariants can give you coding superpowers

#47

Post by BeetleB »

whatshisface wrote: post #23
ummonk wrote: post #14

Earlier quoted context omitted.

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.

Which floating point operator is not commutative? Addition is.

Re: Loop invariants can give you coding superpowers

#48

Post by jonsen »

Itaxpica wrote: post #37
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…

When we covered this in my CS 101 class back in the day, our professor actually had a system he had put together built on Python's unit testing infrastructure. Really, any construct in a programming language that lets you say "assert that this thing is true and if it isn't, do something" can be used for loop invariant checking.

Loop invariant checking should assert that if the invariant is true before the loop starts, it will also be true at the end of the loop. That’s not a general capability of assert constructs.

Re: Loop invariants can give you coding superpowers

#49

Post by karmakaze »

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.

Adding smaller magnitude first gives a different result than adding larger magnitudes first due to mixing precisions.

Re: Loop invariants can give you coding superpowers

#50

Post by jonsen »

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.

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