manolios@cc.gatech.edu
College of Computing
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.
Gzipped Postscript (79K) © Kluwer
PDF (197K) © Kluwer
Postscript (200K) © Kluwer
|
Last modified: Mon Jun 21 10:57:37 EDT 2004
manolios@cc.gatech.edu |
College of Computing |