Recursion and Induction: Introduction

The language we will use is a subset of Lisp called ACL2. ACL2, which stands
for *A Computational Logic for Applicative Common Lisp*, is both a
functional programming language based on Common Lisp and a first-order
mathematical theory with induction. There is a mechanical theorem prover for
ACL2, but we do not discuss it here. A good way to learn to use that theorem
prover is first to master the art of recursive definition and inductive proof.

This course on Recursion and Induction uses a tiny fragment of full ACL2. We describe just enough formal machinery to study recursion and induction in an interesting context. This document is self-contained. You'll need nothing besides this document, a pencil and paper (or a computer), and time and space to think. In the interest of scholarly completeness, we provide an annotated bibliography; see r-and-i-annotated-bibliography. But none of the documents listed there is necessary for the problems here.

These notes are meant to be read linearly, like a text book. Each section
ends with a link to the next section. For example, the link to the section
after this one looks like this,

Throughout these notes you will see see links to resources on the web and
some of those links take you out of the *Recursion and Induction* notes
and into ACL2's online manual. Those “external” links appear like
this, “(Maybe explore <<…>>?)”. These links
lead to related discussions of issues and features of the ACL2 system. You'll
need to be connected to the web to access some of these pages, unless you have
installed ACL2 on your system and built the full manual and books
documentation. See the installation instructions on the ACL2 home page [4].
We provide this material for students who want to explore further. But these
links are technically irrelevant to the student who is focused on working the
exercises here, even if your ultimate goal is to learn how to use ACL2.
First, learn how to do the exercises here. In a second pass, where you're
trying to get ACL2 to do your proofs, you might want to explore. And
remember, it is easy for explorers to get lost!

**If you are working your way through Recursion and Induction and
decide to follow one of these explorer links be sure to use the
“Back” feature of your browser to return to these notes.**

Next: