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.