Partial Functions in ACL2
Panagiotis Manolios and J Strother Moore.
Journal of Automated Reasoning. © Kluwer
We describe a method for introducing "partial functions" into
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.
Gzipped Postscript (79K) © Kluwer
PDF (197K) © Kluwer
Postscript (200K) © Kluwer