Recycling Outputs as Inputs: Induction and Recursion

Abstract

This chapter introduces induction and recursion, which are omnipresent in computer science and logic. The simplest context in which they arise is in the domain of the positive integers, and that is where we begin. We explain induction as a method for proving facts about the positive integers, and recursion as a method for defining functions on the same domain, and describe two different methods for evaluating such functions. From this familiar terrain, the basic concepts of recursion and induction are extended to the forms known as structural induction and recursion, to which we give special attention. We look at structural recursion as a way of defining sets, structural induction as a way of proving things about those sets, and then structural recursion once more, as a way of defining functions with recursively defined domains when a special condition of unique decomposability is satisfied. The broadest kind of induction/recursion may be formulated for any set at all, provided it is equipped with a relation that is well-founded in a sense we explain.