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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
<html>
<head><title>The_Associativity_of_App.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The Associativity of App</h2>
<p>
<img src=green-line.gif><p>
<pre>
ACL2!><b>(let ((a '(1 2))</B>
<b>(b '(3 4))</B>
<b>(c '(5 6)))</B>
<b>(equal (app (app a b) c)</B>
<b>(app a (app b c))))</B>
T
</pre>
<p>
<img src=green-line.gif><p>
Observe that, for the particular <code>a</code>, <code>b</code>, and <code>c</code> above,
<code>(app (app a b) c)</code> returns the same thing as <code>(app a (app b c))</code>.
Perhaps <code>app</code> is <b>associative</B>. Of course, to be associative means
that the above property must hold for all values of <code>a</code>, <code>b</code>, and <code>c</code>,
not just the ones <b>tested</B> above.<p>
Wouldn't it be cool if you could type
<pre>
ACL2!><b>(equal (app (app a b) c)</B>
<b>(app a (app b c)))</B>
</pre>
and have ACL2 compute the value <code>T</code>? Well, <b>you can't!</B> If you try
it, you'll get an error message! The message says we can't evaluate
that form because it contains <b>free</B> variables, i.e., variables
not given values. Click <a href="Free_Variables_in_Top-Level_Input.html">here</a> to see the
message.<p>
We cannot evaluate a form on an infinite number of cases. But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.<p>
<a href="The_Theorem_that_App_is_Associative.html"><img src=walking.gif></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>
|
