# About the Admission of Recursive Definitions

About the Admission of Recursive Definitions

You can't just add any formula as an axiom or definition and expect
the logic to stay sound! For example, if we were permitted to define (APP
X Y) so that it was equal to (NOT (APP X Y)) then we could prove
anything. The purported ``definition'' of APP must have several
properties to be admitted to the logic as a new axiom.

The key property a recursive definition must have is that the recursion
terminate. This, along with some syntactic criteria, ensures us that there
exists a function satisfying the definition.

Termination must be proved before the definition is admitted. This is done
in general by finding a measure of the arguments of the function and a
well-founded relation such that the arguments ``get smaller'' every time a
recursive branch is taken.

For app the measure is the ``size'' of the first argument, x, as
determined by the primitive function `ACL2-count` .
The well-founded relation used in this example is `o-p` ,
which is the standard ordering on the ordinals less than ``epsilon naught.''
These particular choices for app were made ``automatically'' by ACL2.
But they are in fact determined by various ``default'' settings. The user of
ACL2 can change the defaults or specify a ``hint'' to the `defun`
command to specify the measure and relation.

You should now return to the Walking Tour.