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
|
<html>
<head><title>Common_Lisp.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Common Lisp</h2>
<p>
<img src=common-lisp.gif><p>
The logic of ACL2 is based on Common Lisp.<p>
Common Lisp is the standard list processing programming language.
It is documented in: Guy L. Steele, <b>Common Lisp The Language</B>,
Digital Press, 12 Crosby Drive, Bedford, MA 01730, 1990. See
also http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html.<p>
ACL2 formalizes only a subset of Common Lisp. It includes such
familiar Lisp functions as <code>cons</code>, <code>car</code> and <code>cdr</code> for creating
and manipulating list structures, various arithmetic primitives such
as <code>+</code>, <code>*</code>, <code>expt</code> and <code><=</code>, and <code>intern</code> and <code>symbol-name</code> for
creating and manipulating symbols. Control primitives include
<code>cond</code>, <code>case</code> and <code>if</code>, as well as function call, including
recursion. New functions are defined with <code>defun</code> and macros with
<code>defmacro</code>. See <a href="PROGRAMMING.html">programming</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> for a list of the Common
Lisp primitives supported by ACL2.<p>
ACL2 is a very small subset of full Common Lisp. ACL2 does not
include the Common Lisp Object System (CLOS), higher order
functions, circular structures, and other aspects of Common Lisp
that are <b>non-applicative</B>. Roughly speaking, a language is
applicative if it follows the rules of function application. For
example, <code>f(x)</code> must be equal to <code>f(x)</code>, which means, among other
things, that the value of <code>f</code> must not be affected by ``global
variables'' and the object <code>x</code> must not change over time.<p>
Click <a href="An_Example_Common_Lisp_Function_Definition.html">here</a> for a simple example of Common Lisp.<p>
<a href="An_Example_Common_Lisp_Function_Definition.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>
|
