## 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.