Make design doc on recursion more mathematically formal #5
Description
The mathematics is essentially given at a very basic level and the amount of rigour is basically none.
More concretely :
- mention the Knaster-Tarski theorem
- show that the convergence point of the approximation sequence is also a solution to the fixpoint equation
- if time permits, actually prove the Knaster-Tarski theorem
- mention the fact our fixpoint discussion is specifically about least fixpoints
- ideally, justify the usage of least fixpoints for recursive definitions and maybe also introduce and justify the usage of greatest fixpoints for corecursive definitions (use BFS as example of corecursion)