|
|
|---|
|
|
|
|---|
Recursion and Induction
These notes are for teaching yourself how to prove theorems about recursively defined functions using mathematical induction. Think of this as a college-level practical math course that just happens to focus on issues of concern in computing. We assume you're passingly familiar with notions from formal mathematical logic, like “axioms” and “rules of inference” (like instantiation and substitution of equals for equals) to derive “new” truths from “old” ones. We describe a very simple logical system and present many exercises for you to do.
Our presentation is less formal than formal logicians would expect, and the “proofs” we expect of you would be considered just “proof sketches” by formal logicians. But we believe we're precise enough that if you follow our rules your “proofs” could be turned into formal proofs in conventional first-order mathematical logic.
Unlike a traditional course in logic, we do not focus on metatheory but on lots of proofs about elementary algorithms expressed recursively. It helps if you're familiar with computer programming because our logic is a subset of the programming language Lisp and the exercises involve conjectures about simple list processing algorithms like member, union, reverse, etc. We do not assume prior familiarity with Lisp.
In fact, the logic is a subset of the mechanized logic of the ACL2 system. ACL2 stands for “A Computational Logic for Applicative Common Lisp” and the ACL2 system includes a programming language and an “automatic” theorem prover. But this is not a course in mechanical theorem proving or how to use ACL2. In fact, we recommend that you not use the ACL2 system while doing these exercises. A good way to learn to use ACL2 — or any of today's mechanical proof systems — is to learn to do proofs by hand. It will teach you how to define functions that are convenient to analyze, how to state inductively provable theorems, how to decompose theorems into simpler “lemmas”, and how to simplify terms using previously proved results.
If your goal is to learn to prove theorems about recursively defined functions, work your way through these notes and do the exercises. It can help if you partner with someone else so you have someone to double-check your proofs. If your goal is learn to use the ACL2 system to prove theorems, we recommend that you start exactly the same way: work through these exercises by hand (ideally, all of them). Only then should you fire up the prover and try to use it to prove the same theorems you've proved by hand. It will be educational. The ACL2 system is a very attentive partner.
Our answers to all the exercises are available in the Answer Key, which may
be found in the community-books, file
This document started as course notes for CS389R Recursion and Induction, in the Department of Computer Science of the University of Texas at Austin. The course was created in 1981 by Robert S. Boyer and J Strother Moore. It has been offered almost every year since 1981, taught by Boyer, Moore, or Warren A. Hunt, Jr. Initially, the course used a subset of the logic of the Nqthm theorem prover [0], but around 2000 it was changed to a subset of the logic of the ACL2 prover [1,2,4]. (See r-and-i-annotated-bibliography for an annotated bibliography that elaborates references in square brackets, such as “[0]”.) Mechanical theorem proving tools were not taught or used in the course.
In the early 1980s, when Boyer and Moore co-taught the course, the logic was presented in a bare-bones style in a few pages. Several more pages listed problems for the students to work on. Students were expected to formalize concepts and come to the blackboard and present definitions and proofs. Their classmates were expected to question and critique what was being said. Often these classroom discussions just raised new problems that the students addressed in subsequent class meetings.
Over time, the course notes were expanded to include explanations, examples, and more problems. Moore wrote the first version of this ACL2-based document in the early 2000s, building on joint work with Matt Kaufmann. That document was edited still further by Kaufmann, Moore, and Hunt after Hunt began teaching the course in 2004. In 2022, Kaufmann converted it from LaTeX pdf to the hypertext format of ACL2's online documentation and tied it into ACL2's documentation.
Finally, we thank the many sponsors and supporters of the Nqthm and ACL2 projects over the last 40 years, as well as the many students who have so carefully studied and corrected these notes and the many users of Nqthm and ACL2. See the ACL2 Acknowledgments page.
Next: