Partial Functions in ACL2

Panagiotis Manolios
J Strother Moore
January, 2001

Abstract

We describe a method for introducing ``partial functions'' into ACL2, i.e., functions not defined everywhere. The function ``definitions'' are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions and we discuss how such functions can be used to prove theorems about state machine models without reasoning about ``clocks'' or counting the number of steps until termination. Our macro for introducing ``partial functions'' also permits a variety of other recursive schemes and we briefly illustrate some of them.

Supporting Files

the paper (70 KB gzipped postscript): a 13 page paper.
books.tar.gz (16 KB gzipped tar file): the source files for all the ACL2 books and the script needed to re-certify them.
Source files in books.tar.gz, listed alphabetically.
- defpun.lisp: the definition of the defpun macro and its support functions.
- examples.lisp: some example proofs about the TJVM; this file has nothing per se to do with defpun.
- mod-1-property.lisp: an arithmetic theorem about mod used in report.lisp.
- report.lisp: all of the defpun examples cited in the paper. This is the top-level book in this collection.
- script: a script to re-certify all of these books in ACL2; see below.
- tjvm-examples.lisp: the TJVM-related examples of defpun.
- tjvm.lisp: the definition of the TJVM.

To certify all the books in question,

Create some directory, dir.
Download books.tar.gz to dir and then invoke
gunzip books.tar.gz
tar xvf books.tar
or, equivalently, download all the source files to dir.
In both mod-1-property.lisp and report.lisp, change the path /projects/acl2/v2-5-debian-gnu-linux/books to the pathname identifying ACL2's distribution book directory on your local system.
While standing on directory dir, type
acl2 < script > script.log &
where acl2 is the command to invoke ACL2 on your system.

These instructions should produce a script.log (about 1MB) file containing proofs of all the theorems cited, together with proofs of all of the supporting lemmas except those in the standard ACL2 distribution. Successful conclusion will be indicated by the creation of the file dir/report.cert. In addition, .cert files will be created for each of the .lisp source files above.