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.
app the measure is the ``size'' of the first argument,
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
to specify the measure and relation.
You should now return to the Walking Tour.