• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Recursion-and-induction

R-and-i-introduction

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, Data Types; but don't go there yet!

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: Data Types (or Table of Contents)