4 ms·

Honest question, why would you spend weeks doing proof by induction? Looking it up, I think I did that when I was 16, but I've never used it while programming.

Honest question, why would you spend weeks doing proof by induction? Looking it up, I think I did that when I was 16, but I've never used it while programming. I can't see a single benefit to knowing it for programming. Been programming professionally for 12 years now. What am I missing? Why do you think it's important?

popcorncolonel 10y ago
It's helpful for truly understanding recursion.
- mattmanser 10y ago
  If it's so useful for "truly" understanding it, why do I have to show so many CS educated juniors how to use recursion? Have to point out to them to use it instead of doing crazy nested loops or other stupid solutions to a problem simply solved using recursion? Given that I obviously don't "truly" understand it, having never done a CS degree. I'd posit that most CS students don't truly understand recursion, they just vaguely know the theoretical basis behind a practical skill they have no experience in.
  - markhkim 10y ago
    eh, I posit that you already understand induction and just don't know that you do. "So many CS educated juniors" being uncomfortable with recursion is not an argument against understanding mathematical induction. Who says they understood induction?
  - babygoat 10y ago
    You can get a CS degree without understanding induction, and you can understand induction without a CS degree.
  - data4science 10y ago
    I don't know which languages you and your CS educated juniors ("juniors") use. While "juniors" = employees subordinate to you & "so many "juniors"" = high turnover & you = positive senior employee & college educated graduates = smart: "posit that most CS students don't truly understand recusion" = False '''Smart, being distinct from intelligent, indicates a propensity to make decisions that maximize benefit for the person described as smart. A smart CS student would work for a company that valued intellectual capital instead of a company with high turnover.''' While "juniors" = employees subordinate to you & "so many "juniors"" = hyperbole & you = positive senior employee: "posit that most CS students don't truly understand recusion" = False '''It is dubious that more than 171.5k CS graduates worked subordinate to you from 2004-2010, or that an unbiased sample of CS graduates from 2004-2010 worked subordinate to you (see previous While "loop") [1] .''' The proof that the previous comment's posit is not provable follows by induction. Note_0: While loops can use "&" or "and" operators in some languages without nested loops (unless the programmer chooses to implement a break line) to achieve much of the effect of recursive functions. While statements, as implemented in the example above, offer nearly as much access to the input stack as recursive functions; about equal risk of an infinite loop; and don't risk stack overflow. Note_1: I have a bachelors in Math. So, I was likely taught a more substantial "theoretical basis," and less "practical skill" than the curriculum most CS graduates were taught. [1]: http://www.geekwire.com/2014/analysis-examining-computer-science-education-explosion/ http://www.geekwire.com/2014/analysis-examining-computer-sci...
    - mattmanser 10y ago
      10 I don't see what you added to the discussion 20 But I have to ask, if you have a bachelors in Maths, why do you not know about sample sizes? Or about the flaws in assuming perfect knowledge of actors in a system? (on reply, GOTO 10)
tarsinge 10y ago
They are the basis of recursive algorithms proofs, sure you may not need them for everyday programming but that's different for computer science
naasking 10y ago
> Looking it up, I think I did that when I was 16, but I've never used it while programming. Any reasoning about loops or recursion requires an implicit understanding of proof by induction. Making it formally explicit seems like a perfectly fine idea.
gjm11 10y ago
In some sorts of code, you can get a lot of mileage from "loop invariants" and "loop variants". Understanding these is more or less the same as understanding proof by induction. Whether you are missing anything depends on whether you ever write the sort of code that benefits from this. (Even if you do, you still might not be missing anything. You might be comfortable with loop invariants but not have connected them with proof by induction. Or you might be good at reasoning about these things in other ways that don't involve invariants.) (You can stop reading here if you're already very familiar with loop variants and invariants.) Here's the sort of thing I mean by loop variants/invariants. Suppose you're writing a binary search. (Don't write a binary search. Use someone else's that's already had the bugs taken out.) This is basically pretty simple but surprisingly easy to get subtly wrong, which means it's the sort of code it may be useful to write and document in such a way that you have an informal proof of its correctness. Like this: function find(a, x): # find x in sorted array a; return index i such that a[i]==x # or -1 if no such index exists. Takes time at most # proportional to log(#elements). lo,hi = a.index_bounds() while lo<hi: # INVARIANT: min index <= lo < hi <= max index+1 # INVARIANT: if x is in the array then lo <= its index < hi # VARIANT: D := hi-lo reduces to at most D/2 next iteration mid = lo + floor((hi-lo)/2) # may equal lo, can't equal hi if a[mid] == x: return mid # done! if a[mid] < x: lo = mid+1 else: hi = mid # INVARIANT: if x is in the array then lo <= its index < hi # now lo >= hi which means there's nowhere for x to live return -1 The above is pseudocode in no particular language. Is it correct? Those variants and invariants (1) divide that question in two and (2) provide a strategy for answering the second half of the question. First sub-question: if the (in)variants always hold, does that imply that the code is correct? Second sub-question: do they always hold? (Strategy for second sub-question: proof by induction on array size and/or number of iterations.) The first invariant implies that since mid is always between lo (inclusive) and hi (exclusive) it's safe to access a[mid]. The second, given that it holds at both start and end of the loop body, implies that if we exit the loop then indeed x isn't in the array. The only ways to leave the function are via the return in the middle, which only happens when we have explicitly found x, and via the return at the end, which only happens when x is known to be absent; therefore, if we return anything, we return the right thing. And the variant says that the quantity D, which starts by equalling the number of elements in the array, is reduced by a factor of at least 2 at each step; as it's always a (strictly) positive integer, this implies that the number of steps is at most log_2(n), so the function does return. (Note that that last bit is more or less a proof by induction on array size that the function always returns.) So if the invariants hold then the function does the right thing in the right amount of time. Proving that the invariants hold is the induction-like bit. The first invariant holds at the start (since lo,hi start out being exactly min index and max index + 1). Each time around the loop we replace either lo or hi with something in between the two, so we still have min <= lo <= hi < max+1; and we will exit the loop unless in fact lo<hi. So the first invariant always holds. The second invariant holds at the start (since lo,hi are bounds on the entire array). Because the array is sorted, our adjustments to lo/hi make this invariant true again for the next time around the loop. So the second invariant holds at the end of the loop -- and of course therefore at the start of the next iteration. (Note that those were both proofs by induction, though I wasn't super-explicit about the fact.) The variant works because if we write D = hi-lo and E = floor(D/2) then the new value of D is, depending on which branch of that if we take, either E or D-E-1; note that D-E-1<=E; so new-D <= E <= D/2 as claimed. It's probably pretty clear what sort of code this is useful for: highly "algorithmic" code that's basically doing something fairly simple but that's tricky to think about and easy to get wrong. If you're writing a language's standard library, or implementing some sort of iterative mathematical algorithm, then you're quite likely to find it useful. The less like that your code is, the less often this technique will be useful to you. (Fairly extreme example: if you are writing a CRUD webapp then it is unlikely that anything you do will benefit from this.)
jimhefferon 10y ago
You need it for a follow-on course, Theory of Computation.

popcorncolonel 10y ago

It's helpful for truly understanding recursion.

mattmanser 10y ago
If it's so useful for "truly" understanding it, why do I have to show so many CS educated juniors how to use recursion? Have to point out to them to use it instead of doing crazy nested loops or other stupid solutions to a problem simply solved using recursion? Given that I obviously don't "truly" understand it, having never done a CS degree. I'd posit that most CS students don't truly understand recursion, they just vaguely know the theoretical basis behind a practical skill they have no experience in.
- markhkim 10y ago
  eh, I posit that you already understand induction and just don't know that you do. "So many CS educated juniors" being uncomfortable with recursion is not an argument against understanding mathematical induction. Who says they understood induction?
- babygoat 10y ago
  You can get a CS degree without understanding induction, and you can understand induction without a CS degree.
- data4science 10y ago
  I don't know which languages you and your CS educated juniors ("juniors") use. While "juniors" = employees subordinate to you & "so many "juniors"" = high turnover & you = positive senior employee & college educated graduates = smart: "posit that most CS students don't truly understand recusion" = False '''Smart, being distinct from intelligent, indicates a propensity to make decisions that maximize benefit for the person described as smart. A smart CS student would work for a company that valued intellectual capital instead of a company with high turnover.''' While "juniors" = employees subordinate to you & "so many "juniors"" = hyperbole & you = positive senior employee: "posit that most CS students don't truly understand recusion" = False '''It is dubious that more than 171.5k CS graduates worked subordinate to you from 2004-2010, or that an unbiased sample of CS graduates from 2004-2010 worked subordinate to you (see previous While "loop") [1] .''' The proof that the previous comment's posit is not provable follows by induction. Note_0: While loops can use "&" or "and" operators in some languages without nested loops (unless the programmer chooses to implement a break line) to achieve much of the effect of recursive functions. While statements, as implemented in the example above, offer nearly as much access to the input stack as recursive functions; about equal risk of an infinite loop; and don't risk stack overflow. Note_1: I have a bachelors in Math. So, I was likely taught a more substantial "theoretical basis," and less "practical skill" than the curriculum most CS graduates were taught. [1]: http://www.geekwire.com/2014/analysis-examining-computer-science-education-explosion/ http://www.geekwire.com/2014/analysis-examining-computer-sci...
  - mattmanser 10y ago
    10 I don't see what you added to the discussion 20 But I have to ask, if you have a bachelors in Maths, why do you not know about sample sizes? Or about the flaws in assuming perfect knowledge of actors in a system? (on reply, GOTO 10)

tarsinge 10y ago

They are the basis of recursive algorithms proofs, sure you may not need them for everyday programming but that's different for computer science

naasking 10y ago

> Looking it up, I think I did that when I was 16, but I've never used it while programming. Any reasoning about loops or recursion requires an implicit understanding of proof by induction. Making it formally explicit seems like a perfectly fine idea.

gjm11 10y ago

In some sorts of code, you can get a lot of mileage from "loop invariants" and "loop variants". Understanding these is more or less the same as understanding proof by induction. Whether you are missing anything depends on whether you ever write the sort of code that benefits from this. (Even if you do, you still might not be missing anything. You might be comfortable with loop invariants but not have connected them with proof by induction. Or you might be good at reasoning about these things in other ways that don't involve invariants.) (You can stop reading here if you're already very familiar with loop variants and invariants.) Here's the sort of thing I mean by loop variants/invariants. Suppose you're writing a binary search. (Don't write a binary search. Use someone else's that's already had the bugs taken out.) This is basically pretty simple but surprisingly easy to get subtly wrong, which means it's the sort of code it may be useful to write and document in such a way that you have an informal proof of its correctness. Like this: function find(a, x): # find x in sorted array a; return index i such that a[i]==x # or -1 if no such index exists. Takes time at most # proportional to log(#elements). lo,hi = a.index_bounds() while lo<hi: # INVARIANT: min index <= lo < hi <= max index+1 # INVARIANT: if x is in the array then lo <= its index < hi # VARIANT: D := hi-lo reduces to at most D/2 next iteration mid = lo + floor((hi-lo)/2) # may equal lo, can't equal hi if a[mid] == x: return mid # done! if a[mid] < x: lo = mid+1 else: hi = mid # INVARIANT: if x is in the array then lo <= its index < hi # now lo >= hi which means there's nowhere for x to live return -1 The above is pseudocode in no particular language. Is it correct? Those variants and invariants (1) divide that question in two and (2) provide a strategy for answering the second half of the question. First sub-question: if the (in)variants always hold, does that imply that the code is correct? Second sub-question: do they always hold? (Strategy for second sub-question: proof by induction on array size and/or number of iterations.) The first invariant implies that since mid is always between lo (inclusive) and hi (exclusive) it's safe to access a[mid]. The second, given that it holds at both start and end of the loop body, implies that if we exit the loop then indeed x isn't in the array. The only ways to leave the function are via the return in the middle, which only happens when we have explicitly found x, and via the return at the end, which only happens when x is known to be absent; therefore, if we return anything, we return the right thing. And the variant says that the quantity D, which starts by equalling the number of elements in the array, is reduced by a factor of at least 2 at each step; as it's always a (strictly) positive integer, this implies that the number of steps is at most log_2(n), so the function does return. (Note that that last bit is more or less a proof by induction on array size that the function always returns.) So if the invariants hold then the function does the right thing in the right amount of time. Proving that the invariants hold is the induction-like bit. The first invariant holds at the start (since lo,hi start out being exactly min index and max index + 1). Each time around the loop we replace either lo or hi with something in between the two, so we still have min <= lo <= hi < max+1; and we will exit the loop unless in fact lo<hi. So the first invariant always holds. The second invariant holds at the start (since lo,hi are bounds on the entire array). Because the array is sorted, our adjustments to lo/hi make this invariant true again for the next time around the loop. So the second invariant holds at the end of the loop -- and of course therefore at the start of the next iteration. (Note that those were both proofs by induction, though I wasn't super-explicit about the fact.) The variant works because if we write D = hi-lo and E = floor(D/2) then the new value of D is, depending on which branch of that if we take, either E or D-E-1; note that D-E-1<=E; so new-D <= E <= D/2 as claimed. It's probably pretty clear what sort of code this is useful for: highly "algorithmic" code that's basically doing something fairly simple but that's tricky to think about and easy to get wrong. If you're writing a language's standard library, or implementing some sort of iterative mathematical algorithm, then you're quite likely to find it useful. The less like that your code is, the less often this technique will be useful to you. (Fairly extreme example: if you are writing a CRUD webapp then it is unlikely that anything you do will benefit from this.)

jimhefferon 10y ago

You need it for a follow-on course, Theory of Computation.