Proof Techniques for Recursive Programs
Abstract
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 Kleene's 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1973
- Accession Number
- AD0772063
Entities
People
- Jean E. Vuillemin
Organizations
- Stanford University