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
49
50
51
52
|
<html>
<head><title>About_Types.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>About Types</h2>
The universe of ACL2 objects includes objects of many different
types. For example, <code>t</code> is a ``symbol'' and 3 is an ``integer.''
Roughly speaking the objects of ACL2 can be partitioned into the
following types:<p>
<pre>
<a href="Numbers_in_ACL2.html">Numbers</a> <code>3, -22/7, #c(3 5/2)</code>
<a href="ACL2_Characters.html">Characters</a> <code>#\A, #\a, #\Space</code>
<a href="ACL2_Strings.html">Strings</a> <code>"This is a string."</code>
<a href="ACL2_Symbols.html">Symbols</a> <code>'abc, 'smith::abc</code>
<a href="ACL2_Conses_or_Ordered_Pairs.html">Conses (or Ordered Pairs)</a> <code>'((a . 1) (b . 2))</code>
</pre>
<p>
When proving theorems it is important to know the types of object
returned by a term. ACL2 uses a complicated heuristic algorithm,
called <code><a href="TYPE-SET.html">type-set</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>, to determine what types of objects a
term may produce. The user can more or less program the
<code>type-set</code> algorithm by proving <code><a href="TYPE-PRESCRIPTION.html">type-prescription</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>
rules.<p>
ACL2 is an ``untyped'' logic in the sense that the syntax is not
typed: It is legal to apply a function symbol of n arguments to any
n terms, regardless of the types of the argument terms. Thus, it is
permitted to write such odd expressions as <code>(+ t 3)</code> which sums the
symbol <code>t</code> and the integer 3. Common Lisp does not prohibit such
expressions. We like untyped languages because they are simple to
describe, though proving theorems about them can be awkward because,
unless one is careful in the way one defines or states things,
unusual cases (like <code>(+ t 3)</code>) can arise.<p>
To make theorem proving easier in ACL2, the axioms actually define a
value for such terms. The value of <code>(+ t 3)</code> is 3; under the ACL2
axioms, non-numeric arguments to <code>+</code> are treated as though they
were 0.<p>
You might immediately wonder about our claim that ACL2 is Common
Lisp, since <code>(+ t 3)</code> is ``an error'' (and will sometimes even
``signal an error'') in Common Lisp. It is to handle this problem that
ACL2 has <b>guards</B>. We will discuss guards later in the Walking Tour.
However, many new users simply ignore the issue of guards entirely.<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>
|
