## 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! 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 `e0-ordinalp`

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