Search code examples
computer-sciencetheory

Coinduction - clear, concise description

I am studying coinduction(not induction) as part of a class on static analysis. Rummaging around the internet, I am simply not finding clear, concise description of:

  • What coinduction is
  • How coinduction actually proves something(it seems that coinduction is like waving a magic hand in the treatments I've read)
  • What propositions require coinductive proof
  • How to operate a coinductive proof
Solution

  • Coinduction is induction along the steps of a computation or process. If something holds for every step, then it holds for the infinite computation and its possibly infinite resulting data structure.