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

To certify all the books in question, 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.