Defpun
Define a tail-recursive function symbol
Defpun is a macro developed by Pete Manolios and J Moore that
allows tail-recursive definitions, as well as some other ``partial''
definitions. Related utilities are discussed at the end of this topic.
General Form:
(defpun g (v1 ... vk)
dcl ; optional
body
:kwd1 val1 :kwd2 val2 ... :kwdn valn)
where dcl is an optional declare form and the pairs :kwdi
vali are optional (that is n can be 0). If the optional arguments are
omitted, then ACL2 will introduce a constrained function g with this
exported event:
(DEFTHM g-DEF
(EQUAL (g v1 ... vk)
body)
:RULE-CLASSES :DEFINITION)
First suppose that dcl is not present. Then the proposed definition
must have a simple tail-recursive structure (see the discussion of
defp below for a workaround if this is not the case).
If dcl is present, then the definition need not be tail-recursive, and
dcl must have one of the following three forms.
(DECLARE (XARGS :witness defpun-fn))
(DECLARE (XARGS :domain dom-expr :measure m . rest))
(DECLARE (XARGS :gdomain dom-expr :measure m . rest)).
You are encouraged to experiment by using :trans1 to see the
expansions of defpun forms that use these declare forms; but here
is a summary of what is generated.
The first form specifies a function, defpun-fn, and instructs ACL2 to
use that function as a witness for the function g to be introduced, as
follows.
(ENCAPSULATE
((g (v1 ... vk) t))
(LOCAL (DEFUN-NONEXEC g (v1 ... vk) (defpun-fn v1 ... vk)))
(DEFTHM g-DEF
(EQUAL (g v1 ... vk))
body)
:RULE-CLASSES :DEFINITION)
The remaining two declare forms introduce a function, defined
recursively, with the given measure and with a modified body:
(THE-g v1 ... vk)
=
(IF dom-expr body 'UNDEF)
The following theorem is exported.
(defthm g-DEF
(IMPLIES domain-expr
(EQUAL (g v1 ... vk)
body))
:RULE-CLASSES :DEFINITION)
If :gdomain is used (as opposed to :domain), then the following
events are also introduced, where body\{g:=THE-g} denotes the result of
replacing each call of g in body with the corresponding call of
THE-g.
(DEFUN THE-g (v1 ... vk)
(DECLARE (XARGS :MEASURE (IF dom-expr m 0)
:GUARD domain-expr
:VERIFY-GUARDS NIL))
(IF dom-expr body 'UNDEF))
(DEFTHM g-IS-UNIQUE
(IMPLIES domain-expr
(EQUAL (g v1 ... vk) (THE-g v1 ... vk))))
The optional keyword alist :kwd1 val1 :kwd2 val2 ... :kwdn valn is
attached to the end of the generated defthm event. If the
:rule-classes keyword is not specified by the keyword alist,
:definition is used.
Details of defpun are provided by Manolios and Moore in the chapter
``Partial Functions in ACL2'' published with the ACL2 2000
workshop. Also see Partial
Functions in ACL2.
Variants of defpun
A variant, defp, allows more general forms of tail recursion. If
defpun doesn't work for you, try defp by first executing the
following event.
(include-book "misc/defp" :dir :system)
Sandip Ray has contributed a variant of defpun, defpun-exec, that
supports executability. See community book
books/defexec/defpun-exec/defpun-exec.lisp:
(include-book "defexec/defpun-exec/defpun-exec" :dir :system)
He has also contributed community book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are
uniquely defined in a particular domain.
Finally, it is possible to avoid termination proofs even for functions that
are not tail-recursive. See def-partial-measure.
