Proof Techniques for Recursive Programs
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The concept of least fixed-point of a continuous function can be considered as the unifying thread of the report. The connections between fixed- points and recursive programs are detailed in Chapter 2, providing some insights on practical implementations of recursion. There are two usual characterizations of the least fixed-point of a continuous function. To the first characterization, due to Knaster and Tarski, corresponds a class of proof techniques for programs, as described in Chapter 3. The other characterization of least fixed points, better known as Kleenes first recursive theorem, is discussed in Chapter 4. It has the advantage of being effective and it leads to a wider class of proof techniques.
- Theoretical Mathematics
- Computer Programming and Software