4 ms·
I still remember the first time I started to grok recursive definitions in a functional language. At the time it was Scheme and I remember going through all the
by tel 13y ago
I still remember the first time I started to grok recursive definitions in a functional language. At the time it was Scheme and I remember going through all the effort to track the various bits of state and operation as they "reboot" and begin again in each recursive call.
It made me think that recursion, no matter how short the code looked, was terrible.
Now I realize that recursion, thought about properly, requires so much less mental overhead. All those lines of code that vanished were really whole concepts and ideas which could vanish as well.
Of late, my style has been refined by working with theorem provers which make the ultimate connection. Recursion is absolutely nothing more than mathematical induction. Each recursive call is just you invoking the inductive hypothesis.
What that connection really drives home is that when writing a recursive definition you need to do so very few things. First, you need to make sure your definition has a good foundation—you must list all of the conditions where it terminates and ensure that they truly found and support the algorithm/proof. Then you must write the inductive engine that will burn away whatever inputs you receive down to the foundation you just made.
The release is in noticing that those inductive engines can be primed on the very tiniest actions—and those tiny actions are all you, the implementer, are responsible for.
When writing your inductive step consider only the things that are novel about this case. If I'm working with an input list and inducting on `cons` then all I must do is consider what happens to the head and tail of the list. Everything else will be handled by the turning of the inductive engine.
Now a good algorithm just feels like someone walked me into a room with a gigantic domino structure. I walk around it slowly and determine the ends and then just flick the single domino which will churn away inevitably the rest of the algorithm.
- lomnakkus 13y agoInteresting! I had the exact same experience where recursion really clicked -- proof by induction === recursion. Obviously (in hindsight)! :) And, by extension, structural induction === sum & product types + pattern matching destructuring for recursive functions. The fact that the type checker can make sure you've got your base cases covered is just gravy.
- platz 13y agoAlthough I think loops and recursion aren't so different: here's a snippet from meijer: "The goal of recursion and loops is exactly the same, you want to define something in terms of itself. That's what the loop does; it repeats a computation and something gets smaller... the loop variable or when you for each over a loop you're picking out the next element.. That's exactly what a recursive definition tries to do, you're trying to define a function, in terms of a smaller version of it's argument." http://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Functional-Programming-Fundamentals/C9-Lectures-Dr-Erik-Meijer-Functional-Programming-Fundamentals-Chapter-6-of-13 http://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Func...
- tel 13y agoLoops are generally special cases of recursion. You can always derive an iterator from a recursor by forgetting things, but you need product types or ambient state to go the opposite way. In Turing complete languages they're both special cases of fixed-point equations, though, so in that sense they both have the same goal.