Proof Techniques for Recursive Programs.

摘要

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. (Author)