The Logic of Functional Recursion

Abstract

Recursive definitions of functions abound in mathematics and logic: in the classical theory of recursive functions on the set ℕ of natural numbers—of course; in (so-called) abstract or generalized recursion theory; and, most significantly, in programming languages, where (especially since the work of Scott [9]) it has become clear that the main “programming construct” is definition by recursion. And so it is important to understand how properties of recursively defined functions—follow logically from their definitions. The paper could be called the logic of programs, but the title above is more specific, more general (in some ways), and also more honest, since the austere, mathematical formulation in which the problem is best understood is quite removed from actual programming practice. The formal proof systems and completeness results of this paper are related to “program verification” very much like predicate logic and its completeness are related to axiomatic set theory; they are certainly relevant, but not of much help in establishing specific, concrete results.

During the preparation of this paper the author was partially supported by an NSF Grant.