Partial Functions in ACL2
J Strother Moore
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.
To certify all the books in question,
- 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.
the definition of the
defpun macro and its support functions.
some example proofs about the TJVM; this file has nothing per se
to do with
an arithmetic theorem about
mod used in
all of the
defpun examples cited in the paper. This is the top-level
book in this collection.
a script to re-certify all of these books in ACL2; see below.
the TJVM-related examples of
the definition of the TJVM.
These instructions should produce a
- Create some directory, dir.
books.tar.gz to dir and then invoke
tar xvf books.tar
or, equivalently, download all the source files to dir.
- In both
change the path
/projects/acl2/v2-5-debian-gnu-linux/books to the
pathname identifying ACL2's distribution book directory on your
- While standing on directory dir, type
acl2 < script > script.log &
is the command to invoke ACL2 on your system.
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
/report.cert. In addition,
files will be created for each of the
.lisp source files above.