63.460: Theory of Computing
Why induction and coinduction are important
Induction (recursion) is used to define functions that are computable by algorithms; it turns out that the recursively definable functions are precisely the ones that algorithms can compute. (Topic 5)
Induction also defines all kinds of finite structures like grammars and trees, and there are inductive proofs about a lot of these structures. (e.g., Topic 3)
Coinduction defines infinite structures, including I/O streams and representations of real numbers. The fact that reals correspond to infinite bit streams will be central to the diagonal proof by Cantor (Topic 1) that there are "more" reals than natural numbers.
Whereas algorithms compute from finite input to finite output, interaction is inherently unbounded, so we deal with streams to characterize interaction (topic 6). These streams are defined coinductively.