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. You get long variable names, but not horribly so.
You can do the same for the accumulator in a reduce/fold operation. Way too often variables in reduce calls (and other recursive functions) have horrible names, making the entire reduce needlessly hard to understand. Naming the accumulator properly solves this:
So much easier to follow! I've often had to look up, when reading a reduce, which argument is the accumulator in this particular language or library. When you use the invariant for the accumulator name, you fix this entirely.
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).
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.
It's an associativity problem and not a commutative one, however, that is relevant to the original point about folding floating point operations over lists.
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.
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)))
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.
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:
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.
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.
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.
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 "ObjectWithPointerToNextObject" and know exactly what that pattern should look like. A lot of CS skill comes down to expanding simple standard names.
That's not to say that your approach doesn't have value. It might just be that the toy example doesn't show it off very well. But if you were juggling that 3-way partition, for example, your naming scheme starts making a lot of sense for naming the boundary variables.
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.
> be useful if you could express it in types or some other machine-checkable fashion
I think this is as close to the answer you can get in the paradigm in which you're asking. It is useful in the formal but non-machine-checkable realm to design the algorithm. Every invariant you can encode into the type system is a double win, but invariants you can't specify in the type system are still a win.
FWIW, direct exposure to abstract concepts like this is a benefit of a CS education. They're eminently learnable outside of a classroom (bottom-up), but you have to work to keep an open mind to recognize the trail of breadcrumbs that leads past your practicality-tailored preconceptions. Think of yourself as learning math, not programming.
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?
For the rare languages that support invariants (or has a library that implements invariants) you would write it as code rather than a comment and the compiler will compile time error if the compiled code is capable of violating the invariant.
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.
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.
> 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.
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.
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!).
The Invariant Principle was formulated by Robert W. Floyd at Carnegie Tech in 1967. (Carnegie Tech was renamed Carnegie-Mellon University the following year.) Floyd was already famous for work on the formal grammars that transformed the field of programming language parsing; that was how he got to be a professor even though he never got a Ph.D. (He had been admitted to a PhD program as a teenage prodigy, but flunked out and never went back.)
In that same year, Albert R. Meyer was appointed Assistant Professor in the Carnegie Tech Computer Science Department, where he first met Floyd. Floyd and Meyer were the only theoreticians in the department, and they were both delighted to talk about their shared interests. After just a few conversations, Floyd’s new junior colleague decided that Floyd was the smartest person he had ever met.
Naturally, one of the first things Floyd wanted to tell Meyer about was his new, as yet unpublished, Invariant Principle. Floyd explained the result to Meyer, and Meyer wondered (privately) how someone as brilliant as Floyd could be excited by such a trivial observation. Floyd had to show Meyer a bunch of examples before Meyer understood Floyd’s excitement — not at the truth of the utterly obvious
Invariant Principle, but rather at the insight that such a simple method could be so widely and easily applied in verifying programs.
If you're interested in playing around with loop invariants for non-trivial programs, I recommend the Dafny programming language which can automatically verify the invariants using SMT solvers. (Dafny is much more convenient that messing around with operational semantics in Coq.)
There's a tutorial + web interface at: https://rise4fun.com/Dafny/tutorial/Guide. The official repository is here: https://github.com/Microsoft/dafny -- you might want to switch to a local installation once the online tutorial whets your appetite. A good initial challenge, once you've gotten past the baby stuff in the tutorial, is implementing insertion and deletion on a binary search tree with appropriate pre- and post-conditions.
Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually verified, they might as well be filler text!
If there's anything I hope the mainstream adopts at some point, it is some variation of what Dafny offers here.
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 pacemakers next year. Imagine you're writing the navigation logic for a cruise missile.
There are many times where proving your code correct is taken very, very seriously. Invariants are a tool to do so more easily.
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?
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 <= n)
assume (i <= n) {
note: (sum = 1 + 2 + ... i-1 -> (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!
This is a great technique; I learned it in David Gries' Intro to CS at Cornell, but a lot of my classmates didn't think so, which elevated this to meme status at Cornell: https://quotes.cs.cornell.edu/quote/1369/
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 the goal in the invariant sometimes gives you nicer properties. The equivalence relation often also implies an algorithm.
For max I would say the equivalence is: Max(0..X)=Max(Max(0..I),max(I+1..X))
This of course only easier if the max of empty is negative infinity.
Then you can move the i from 0 to X.
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.
On a similar note, for max and min algorithms you actually do have a sensible initial element, which is the min or the max integer for the integer type in question. However, you have to make sure this value can't escape into the caller's context (unless it really is the max value); calling max or min with an empty list ought to be an error in whatever the appropriate local error idiom is. The article (reasonably appropriately) glossed over that.
This isn't necessarily a new idea. Tony Hoare discussed the idea for a while with his creation of Hoare triples; we are learning about the application right now in my Software Foundations course. It has a lot of interesting application within Coq for the analysis of the validity of programs, though. A good place to learn more about the application is here: https://softwarefoundations.cis.upenn.edu/current/plf-curren...
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).
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.
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):
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 that idea or taught to program like that in the first place so I realize that that's my own bias).
What should I check out if I want to be able to formally check invariants for e.g. my Python or Swift code?
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.
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.
I discovered the power of loop invariants during a course at university. A professor even developed a compiler like this, starting by defining invariants and writing the code accordingly. Really inspiring!
I wonder, are there such techniques tailored to functional programming? (immutability, recursion,...)
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.
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. You get long variable names, but not horribly so.
You can do the same for the accumulator in a reduce/fold operation. Way too often variables in reduce calls (and other recursive functions) have horrible names, making the entire reduce needlessly hard to understand. Naming the accumulator properly solves this:
Eg
So much easier to follow! I've often had to look up, when reading a reduce, which argument is the accumulator in this particular language or library. When you use the invariant for the accumulator name, you fix this entirely.