Accession Number:

AD0772063

Title:

Proof Techniques for Recursive Programs

Descriptive Note:

Technical rept.

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1973-10-01

Pagination or Media Count:

106.0

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 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.

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE