1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
<html>
<head><title>About_the_Admission_of_Recursive_Definitions.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>About the Admission of Recursive Definitions</h2>
You can't just add any formula as an axiom or definition and expect
the logic to stay sound! The purported ``definition'' of <code>APP</code>
must have several properties to be admitted to the logic as a new
axiom
<p>
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.<p>
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.<p>
For <code>app</code> the measure is the ``size'' of the first argument, <code>x</code>,
as determined by the primitive function <code><a href="ACL2-COUNT.html">acl2-count</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>. The
well-founded relation used in this example is <code><a href="O-P.html">o-p</a></code>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>, which is the standard ordering on the ordinals less than
``epsilon naught.'' These particular choices for <code>app</code> 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 <code><a href="DEFUN.html">defun</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> command to
specify the measure and relation.<p>
You should now return to <a href="Revisiting_the_Admission_of_App.html">the Walking Tour</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
