# 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.