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
|
<html>
<head><title>Common_Lisp_as_a_Modeling_Language.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Common Lisp as a Modeling Language</h2>
<p>
<img src=common-lisp.gif><p>
In ACL2 we have adopted Common Lisp as the basis of our modeling language.
If you have already read our brief note on Common Lisp and recall
the example of <code>app</code>, please proceed. Otherwise
click <a href="Common_Lisp.html">here</a> for an exceedingly brief introduction to
Common Lisp and then come <b>back</B> here.<p>
In Common Lisp it is very easy to write systems of formulas that
manipulate discrete, inductively constructed data objects. In building
a model you might need to formalize the notion of sequences and define
such operations as concatenation, length, whether one is a permutation
of the other, etc. It is easy to do this in Common Lisp. Furthermore,
if you have a Common Lisp ``theory of sequences'' you can <b>run</B>
the operations and relations you define. That is, you can execute
the functions on concrete data to see what results your formulas produce.<p>
If you define the function <code>app</code> as shown above and then type
<pre>
(app '(A B) '(C D E))
</pre>
in any Common Lisp, the answer will be computed and will be
<code>(A B C D E)</code>.<p>
The <b>executable</B> nature of Common Lisp and thus of ACL2 is very handy
when producing models. <p>
But executability is not enough for a modeling language because the purpose
of models is to permit analysis. <p>
Click <a href="Analyzing_Common_Lisp_Models.html">here</a> to continue.
<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>
|
