Recursive Programs as Definitions in First-Order Logic
Robert Cartwright · SIAM Journal on Computing · 1984
Despite the reputed limitations of first order logic, it is easy to state and prove almost all interesting properties of recursive programs within a simple first order theory, by using an approach we call “first order programming logic”. Unlike higher order logics based on fixed-point induction, first order programming logic is founded on deductive principles that are familiar to most programmers. Informal structural induction arguments (such as termination proofs for LISP append, McCarthy’s 91-function, and Ackermann’s function) have direct formalizations within the system. The essential elements of first order programming logic are: (1) The data domain D must be a finitely generated set that explicitly includes the “undefined” object $ \bot $ (representing nontermination) as well as ordinary data objects. (2) Recursive programs over D are treated as logical definitions augmenting a first order theory ofthe data domain. (3) The interpretation of a recursive program is the least fixed-point of the functional corresponding to the program. Since the data domain D is a finitely generated set, the first order axiomatization of D includes a structural induction axiom scheme. This axiom scheme serves as the fundamental “proof rule” of first order program-ming logic. The major limitation of first order programming logic is that every fixed-point of the functional corresponding to a recursive program is an acceptable interpretation for the program. The logic fails to capture the notion of least fixed-point. To overcome this limitation, we present a simple, effective procedure for transforming an arbitrary recursive program into an equivalent recursive program that has a unique fixed-point, yet retains the logical structure of the original. Given this transformation technique, it is our experience that first order programming logic is sufficiently powerful to prove almost any property of practical interest about the functions computed by recursive programs.