Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: About the ACL2 Home Page, Next: About the Admission of Recursive Definitions, Prev: About Types, Up: Pages Written Especially for the Tours About the ACL2 Home Page About the ACL2 Home Page The ACL2 Home Page is integrated into the ACL2 online documentation. Over 1.5 megabytes of text is available here. The vast majority of the text is user-level documentation. For example, to find out about rewrite <> rules you could click on the word "rewrite <>." But before you do that remember that you must then use your browser's back commands to come back here. The tiny warning signs <> mark pointers that lead out of the introductory-level material and into the user documentation. If you are taking the Flying Tour, we advise you to avoid following such pointers the first time; it is easy to get lost in the full documentation unless you are pursuing the answer to a specific question. If you do wander down these other paths, remember you can back out to a page containing the Flying Tour icon to resume the tour. At the end of the tour you will have a chance to return to The Flight Plan where you can revisit the main stops of the Flying Tour and explore the alternative paths more fully. Finally, every page contains two icons at the bottom. The ACL2 icon leads you back to the ACL2 Home Page. The Index icon allows you to browse an alphabetical listing of all the topics in ACL2's online documentation. Flying Tour: *Note What Is ACL2(Q)::  File: acl2-doc-lemacs.info, Node: About the Admission of Recursive Definitions, Next: About the Prompt, Prev: About the ACL2 Home Page, Up: Pages Written Especially for the Tours About the Admission of Recursive Definitions About the Admission of Recursive Definitions You can't just add any formula as an axiom or definition and expect the logic to stay sound! The purported "definition" of APP must have several properties to be admitted to the logic as a new axiom The key property a recursive definition must have is that the recursion terminate. This, along with some syntactic criteria, insures us that there exists a function satisfying the definition. 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. For app the measure is the "size" of the first argument, x, as determined by the primitive function acl2-count <>. The well-founded relation used in this example is e0-ordinalp <>, which is the standard ordering on the ordinals less than "epsilon naught." These particular choices for app 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 defun <> command to specify the measure and relation. You should now return to the Walking Tour.  File: acl2-doc-lemacs.info, Node: About the Prompt, Next: An Example Common Lisp Function Definition, Prev: About the Admission of Recursive Definitions, Up: Pages Written Especially for the Tours About the Prompt About the Prompt The string "ACL2 !>" is the ACL2 prompt. The prompt tells the user that an ACL2 command <>is expected. In addition, the prompt tells us a little about the current state of the ACL2 command interpreter. We explain the prompt briefly below. But first we talk about the command interpreter. An ACL2 command is generally a Lisp expression to be evaluated. There are some unusual commands (such as :q <> for quitting ACL2) which cause other behavior. But most commands are read, evaluated, and then have their results printed. Thus, we call the command interpreter a "read-eval-print loop." The ACL2 command interpreter is named LD <> (after Lisp's "load"). A command like (defun app (x y) ...) causes ACL2 to evaluate the defun <> function on app, (x y) and .... When that command is evaluated it prints some information to the terminal explaining the processing of the proposed definition. It returns the symbol APP as its value, which is printed by the command interpreter. (Actually, defun is not a function but a macro which expands to a form that involves state <>, a necessary precondition to printing output to the terminal and to "changing" the set of axioms. But we do not discuss this further here.) The defun command is an example of a special kind of command called an "event." Events <> are those commands that change the "logical world" by adding such things as axioms or theorems to ACL2's data base. *Note WORLD:: <>. But not every command is an event command. A command like (app '(1 2 3) '(4 5 6 7)) is an example of a non-event. It is processed the same general way: the function app is applied to the indicated arguments and the result is printed. The function app does not print anything and does not change the "world." A third kind of command are those that display information about the current logical world or that "backup" to previous versions of the world. Such commands are called "history" <> commands. What does the ACL2 prompt tell us about the read-eval-print loop? The prompt "ACL2 !>" tells us that the command will be read with current-package <> set to "ACL2", that guard checking (*Note SET-GUARD-CHECKING:: <>) is on ("!"), and that we are at the top-level (there is only one ">"). For more about the prompt, *Note DEFAULT-PRINT-PROMPT:: <>. You should now return to the Walking Tour.  File: acl2-doc-lemacs.info, Node: An Example Common Lisp Function Definition, Next: An Example of ACL2 in Use, Prev: About the Prompt, Up: Pages Written Especially for the Tours An Example Common Lisp Function Definition An Example Common Lisp Function Definition Consider the binary trees x and y below. In Lisp, x is written as the list '(A B) or, equivalently, as '(A B . NIL). Similarly, y may be written '(C D E). Suppose we wish to replace the right-most tip of x by the entire tree y. This is denoted (app x y), where app stands for "append". We can define app with: (defun app (x y) ; Concatenate x and y. (declare (type (satisfies true-listp) x)); We expect x to end in NIL. (cond ((endp x) y) ; If x is empty, return y. (t (cons (car x) ; Else, copy first node (app (cdr x) y))))) ; and recur into next. If you defined this function in some Common Lisp, then to run app on the x and y above you could then type (app '(A B) '(C D E)) and Common Lisp will print the result (A B C D E). Walking Tour: *Note An Example of ACL2 in Use::  File: acl2-doc-lemacs.info, Node: An Example of ACL2 in Use, Next: Analyzing Common Lisp Models, Prev: An Example Common Lisp Function Definition, Up: Pages Written Especially for the Tours An Example of ACL2 in Use An Example of ACL2 in Use To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, except we will omit for the moment the declare form, which in ACL2 is called a guard. We will deal with guards later. Here is the definition again (defun app (x y) (cond ((endp x) y) (t (cons (car x) (app (cdr x) y))))) The next few stops along the Walking Tour will show you * how to use the ACL2 documentation, * what happens when the above definition is submitted to ACL2, * what happens when you evaluate calls of app, * what one simple theorem about app looks like, * how ACL2 proves the theorem, and * how that theorem can be used in another proof. Along the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works. When we complete this part of the tour we will introduce the notion of guards and revisit several of the topics above in that context. Walking Tour: *Note How To Find Out about ACL2 Functions::  File: acl2-doc-lemacs.info, Node: Analyzing Common Lisp Models, Next: Common Lisp, Prev: An Example of ACL2 in Use, Up: Pages Written Especially for the Tours Analyzing Common Lisp Models Analyzing Common Lisp Models To analyze a model you must be able to reason about the operations and relations involved. Perhaps, for example, some aspect of the model depends upon the fact that the concatenation operation is associative. In any Common Lisp you can confirm that (app '(A B) (app '(C D) '(E F))) and (app (app '(A B) '(C D)) '(E F))) both evaluate to the same thing, (A B C D E F). But what distinguishes ACL2 (the logic) from applicative Common Lisp (the language) is that in ACL2 you can prove that the concatenation function app is associative when its arguments are true-lists, whereas in Common Lisp all you can do is test that proposition. That is, in ACL2 it makes sense to say that the following formula is a "theorem." Theorem Associativity of App (implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c)))) Theorems about the properties of models are proved by symbolically manipulating the operations and relations involved. If the concatenation of sequences is involved in your model, then you may well need the theorem above in order to that your model has some particular property.  File: acl2-doc-lemacs.info, Node: Common Lisp, Next: Common Lisp as a Modeling Language, Prev: Analyzing Common Lisp Models, Up: Pages Written Especially for the Tours Common Lisp Common Lisp The logic of ACL2 is based on Common Lisp. Common Lisp is the standard list processing programming language. It is documented in: Guy L. Steele, Common Lisp The Language, Digital Press, 12 Crosby Drive, Bedford, MA 01730, 1990. ACL2 formalizes only a subset of Common Lisp. It includes such familiar Lisp functions as cons, car and cdr for creating and manipulating list structures, various arithmetic primitives such as +, *, expt and <=, and intern and symbol-name for creating and manipulating symbols. Control primitives include cond, case and if, as well as function call, including recursion. New functions are defined with defun and macros with defmacro. *Note PROGRAMMING:: <> for a list of the Common Lisp primitives supported by ACL2. 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 non-applicative. Roughly speaking, a language is applicative if it follows the rules of function application. For example, f(x) must be equal to f(x), which means, among other things, that the value of f must not be affected by "global variables" and the object x must not change over time. *Note An Example Common Lisp Function Definition:: for a simple example of Common Lisp. Walking Tour: *Note An Example Common Lisp Function Definition::  File: acl2-doc-lemacs.info, Node: Common Lisp as a Modeling Language, Next: Conversion, Prev: Common Lisp, Up: Pages Written Especially for the Tours Common Lisp as a Modeling Language Common Lisp as a Modeling Language 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 app, please proceed. Otherwise *Note Common Lisp:: for an exceedingly brief introduction to Common Lisp and then come back here. 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 run the operations and relations you define. That is, you can execute the functions on concrete data to see what results your formulas produce. If you define the function app as shown above and then type (app '(A B) '(C D E)) in any Common Lisp, the answer will be computed and will be (A B C D E). The executable nature of Common Lisp and thus of ACL2 is very handy when producing models. But executability is not enough for a modeling language because the purpose of models is to permit analysis. *Note Analyzing Common Lisp Models:: to continue.  File: acl2-doc-lemacs.info, Node: Conversion, Next: Corroborating Models, Prev: Common Lisp as a Modeling Language, Up: Pages Written Especially for the Tours Conversion Conversion to Uppercase When symbols are read by Common Lisp they are converted to upper case. Note carefully that this remark applies to the characters in *symbols*. The characters in strings are not converted upper case. To type a symbol containing lower case characters you can enclose the symbol in vertical bars, as in |AbC| or you can put a "backslash" before each lower case character you wish to preserve, as in A\bC. |AbC| and A\bC are two different ways of writing the same symbol (just like 4/2 and 1/2 are two different ways of writing the same rational). The symbol has three characters in its name, the middle one of which is a lower case b.  File: acl2-doc-lemacs.info, Node: Corroborating Models, Next: Evaluating App on Sample Input, Prev: Conversion, Up: Pages Written Especially for the Tours Corroborating Models Corroborating Models After producing a model, it must be corroborated against reality. The Falling Body Model has been corroborated by a vast number of experiments in which the time and distance were measured and compared according to the formula. In general all models must be corroborated by experiment. The Falling Body Model can be derived from deeper models, namely Newton's laws of motion and the assertion that, over the limited distances concerned, graviation exerts a constant acceleration on the object. When the model in question can be derived from other models, it is the other models that are being corroborated by our experiments. Because nature is not formal, we cannot prove that our models of it are correct. All we can do is test our models against nature's behavior. Such testing often exposes restrictions on the applicability of our models. For example, the Falling Body Model is inaccurate if air resistance is significant. Thus, we learn not to use that model to predict how long it takes a feather to fall from a 200 foot tower in the earth's atmosphere. In addition, attempts at corroboration might reveal that the model is actually incorrect. Careful measurements might expose the fact that the gravitational force increases as the body falls closer to earth. Very careful measurements might reveal relativistic effects. Technically, the familiar Falling Body Model is just wrong, even under excessive restrictions such as "in a perfect vacuum" and "over small distances." But it is an incredibly useful model nonetheless. There are several morals here. Models need not be complete to be useful. Models need not be perfectly accurate to be useful. The user of a model must understand its limitations. Flying Tour: *Note Models of Computer Hardware and Software::  File: acl2-doc-lemacs.info, Node: Evaluating App on Sample Input, Next: Flawed Induction Candidates in App Example, Prev: Corroborating Models, Up: Pages Written Especially for the Tours Evaluating App on Sample Input Evaluating App on Sample Input ACL2 !>(app nil '(x y z)) (X Y Z) ACL2 !>(app '(1 2 3) '(4 5 6 7)) (1 2 3 4 5 6 7) ACL2 !>(app '(a b c d e f g) '(x y z)) ; *Note Conversion:: for an explanation (A B C D E F G X Y Z) ACL2 !>(app (app '(1 2) '(3 4)) '(5 6)) (1 2 3 4 5 6) ACL2 !>(app '(1 2) (app '(3 4) '(5 6))) (1 2 3 4 5 6) ACL2!>(let ((a '(1 2)) (b '(3 4)) (c '(5 6))) (equal (app (app a b) c) (app a (app b c)))) T As we can see from these examples, ACL2 functions can be executed more or less as Common Lisp. The last three examples suggest an interesting property of app. Walking Tour: *Note The Associativity of App::  File: acl2-doc-lemacs.info, Node: Flawed Induction Candidates in App Example, Next: Functions for Manipulating these Objects, Prev: Evaluating App on Sample Input, Up: Pages Written Especially for the Tours Flawed Induction Candidates in App Example Flawed Induction Candidates in App Example Induction on a is unflawed: every occurrence of a in the conjecture (equal (app (app a b) c) (app a (app b c))) is in a position being recursively decomposed! Now look at the occurrences of b. The first (shown in bold below) is in a position that is held constant in the recursion of (app a b). It would be "bad" to induct on b here. (equal (app (app a b) c) (app a (app b c)))  File: acl2-doc-lemacs.info, Node: Functions for Manipulating these Objects, Next: Guards, Prev: Flawed Induction Candidates in App Example, Up: Pages Written Especially for the Tours Functions for Manipulating these Objects Functions for Manipulating these Objects Consider a typical "stack" of control frames. Suppose the model required that we express the idea of "the most recent frame whose return program counter points into MAIN." The natural expression of this notion involves function application -- "fetch the return-pc of this frame" case analysis -- "if the pc is MAIN, then ..." iteration or recursion -- "pop this frame off and repeat." The designers of ACL2 have taken the position that a programming language is the natural language in which to define such notions, provided the language has a mathematical foundation so that models can be analyzed and properties derived logically. is the language supported by ACL2. *Note Common Lisp:: for an optional and very brief introduction to Common Lisp. Flying Tour: *Note Modeling in ACL2::  File: acl2-doc-lemacs.info, Node: Guards, Next: Guessing the Type of a Newly Admitted Function, Prev: Functions for Manipulating these Objects, Up: Pages Written Especially for the Tours Guards Guards Common Lisp functions are partial; they are not defined for all possible inputs. But ACL2 functions are total. Roughly speaking, the logical function of a given name in ACL2 is a completion of the Common Lisp function of the same name obtained by adding some arbitrary but "natural" values on arguments outside the "intended domain" of the Common Lisp function. ACL2 requires that every ACL2 function symbol have a "guard," which may be thought of as a predicate on the formals of the function describing the intended domain. The guard on the primitive function car <>, for example, is (or (consp x) (equal x nil)), which requires the argument to be either an ordered pair or nil. We will discuss later how to specify a guard for a defined function; when one is not specified, the guard is t which is just to say all arguments are allowed. But guards are entirely extra-logical: they are not involved in the axioms defining functions. If you put a guard on a defined function, the defining axiom added to the logic defines the function on all arguments, not just on the guarded domain. So what is the purpose of guards? The key to the utility of guards is that we provide a mechanism, called "guard verification," for checking that all the guards in a formula are true. That is,(i-am-here) Functions in ACL2 may restrict their arguments. These restrictions take the form of formulas about the formal parameters. These formulas are called "guards." The Common Lisp primitives such as car <> and endp <> have guards. ACL2 permits you to specify restrictions on the arguments to the functions you define. To do so you use the xargs <> declaration (*Note DECLARE::<>) for defun <>. Logically speaking, guards are irrelevant. (i-am-here)  File: acl2-doc-lemacs.info, Node: Guessing the Type of a Newly Admitted Function, Next: Guiding the ACL2 Theorem Prover, Prev: Guards, Up: Pages Written Especially for the Tours Guessing the Type of a Newly Admitted Function Guessing the Type of a Newly Admitted Function When a function is admitted to the logic, ACL2 tries to "guess" what type of object it returns. This guess is codified as a term that expresses a property of the value of the function. For app the term is (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)) which says that app returns either a cons or its second argument. This formula is added to ACL2's rule base as a type-prescription <> rule. Later we will discuss how rules are used by the ACL2 theorem prover. The point here is just that when you add a definition, the data base of rules is updated, not just by the addition of the definitional axiom, but by several new rules. You should now return to the Walking Tour.  File: acl2-doc-lemacs.info, Node: Guiding the ACL2 Theorem Prover, Next: Hey Wait! Is ACL2 Typed or Untyped(Q), Prev: Guessing the Type of a Newly Admitted Function, Up: Pages Written Especially for the Tours Guiding the ACL2 Theorem Prover Guiding the ACL2 Theorem Prover Now that you have seen the theorem prover in action you might be curious as to how you guide it. The idea is that the user submits conjectures and advice and reads the proof attempts as they are produced. Most of the time, the conjectures submitted are lemmas to be used in the proofs of other theorems. Walking Tour: *Note ACL2 as an Interactive Theorem Prover (continued)::  File: acl2-doc-lemacs.info, Node: Hey Wait! Is ACL2 Typed or Untyped(Q), Next: How Long Does It Take to Become an Effective User(Q), Prev: Guiding the ACL2 Theorem Prover, Up: Pages Written Especially for the Tours Hey Wait! Is ACL2 Typed or Untyped(Q) Hey Wait! Is ACL2 Typed or Untyped? The example ACL2 !>(app 7 27) ACL2 Error in TOP-LEVEL: The guard for the function symbol ENDP, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 7). illustrates the fact that while ACL2 is an untyped language the ACL2 evaluator can be configured so as to check "types" at runtime. We should not say "types" here but "guards." *Note Undocumented Topic::for a discussion of guards. The guard on endp <> requires its argument to be a true list. Since 7 is not a true list, and since ACL2 is checking guards in this example, an error is signaled by ACL2. How do you know ACL2 is checking guards? Because the prompt tells us (*Note About the Prompt::) with its "!".  File: acl2-doc-lemacs.info, Node: How Long Does It Take to Become an Effective User(Q), Next: How To Find Out about ACL2 Functions, Prev: Hey Wait! Is ACL2 Typed or Untyped(Q), Up: Pages Written Especially for the Tours How Long Does It Take to Become an Effective User(Q) How Long Does It Take to Become an Effective User? The training time depends primarily on the background of the user. We expect that a user who * has a bachelor's degree in computer science or mathematics, * has some experience with formal methods, * has had some exposure to Lisp programming and is comfortable with the Lisp notation, * is familiar with and has unlimited access to a Common Lisp host processor, operating system, and text editor (we use Sun workstations running Unix and GNU Emacs), * is willing to read and study the ACL2 documentation, and * is given the opportunity to start with "toy" projects before being expected to tackle the company's Grand Challenge, will probably take several months to become an effective ACL2 user. Flying Tour: *Note Other Requirements::  File: acl2-doc-lemacs.info, Node: How To Find Out about ACL2 Functions, Next: How To Find Out about ACL2 Functions (continued), Prev: How Long Does It Take to Become an Effective User(Q), Up: Pages Written Especially for the Tours How To Find Out about ACL2 Functions How To Find Out about ACL2 Functions Most ACL2 primitives are documented. Here is the definition of app again, with the documented topics highlighted. <> All of the links below lead into the ACL2 online documentation, 1.5 megabytes of hyperlinked text. So follow these links around, but remember to come back here! (defun app (x y) (cond ((endp x) y) (t (cons (car x) (app (cdr x) y))))) By following the link on endp <> we see that it is a Common Lisp function and is defined to be the same as atom <>, which recognizes non-conses. But endp has a guard. Since we are ignorning guards for now, we'll ignore the guard issue on endp. So this definition reads "to app x and y: if x is an atom, return y; otherwise, app (cdr x) and y and then cons (car x) onto that." Walking Tour: *Note How To Find Out about ACL2 Functions (continued)::  File: acl2-doc-lemacs.info, Node: How To Find Out about ACL2 Functions (continued), Next: Modeling in ACL2, Prev: How To Find Out about ACL2 Functions, Up: Pages Written Especially for the Tours How To Find Out about ACL2 Functions (continued) How To Find Out about ACL2 Functions (continued) You can always use the Index <> to find the documentation of functions. Try it. Click on the Index icon below. Then use the Find command of your browser to find "endp" in that document and follow the link. But remember to come back here. The ACL2 documentation is also available via Emacs' TexInfo, allowing you to explore the hyperlinked documentation in the comfort of a text editor that can also interact with ACL2. In addition, some runtime images of ACL2 (the so-called "large image") have the hyperlinked text as a large ACL2 data structure that can be explored with ACL2's :doc command. If you have ACL2 running, try the command :doc endp. If that doesn't work, you are running the "small image." Another way to find out about ACL2 functions, if you have an ACL2 image available, is to use the command :args <> which prints the formals, type, and guard of a function symbol. Of course, the ACL2 documentation can also be printed out as 700 page book. See the ACL2 Home Page to download the Postscript. Now let's continue with app. Walking Tour: *Note The Admission of App::  File: acl2-doc-lemacs.info, Node: Modeling in ACL2, Next: Models in Engineering, Prev: How To Find Out about ACL2 Functions (continued), Up: Pages Written Especially for the Tours Modeling in ACL2 Modeling in ACL2 Below we define mc(s,n) to be the function that single-steps n times from a given starting state, s. In Common Lisp, "mc(s,n)" is written (mc s n). (defun mc (s n) ; To step s n times: (if (zp n) ; If n is 0 s ; then return s (mc (single-step s) (- n 1)))) ; else step single-step(s) n-1 times. This is an example of a formal model in ACL2. Flying Tour: *Note Running Models::  File: acl2-doc-lemacs.info, Node: Models in Engineering, Next: Models of Computer Hardware and Software, Prev: Modeling in ACL2, Up: Pages Written Especially for the Tours Models in Engineering Models in Engineering Frequently, engineers use mathematical models. Use of such models frequently lead to better designs, faster completion of acceptable products, and reduced overall cost, because models allow the trained user to study the design before it is built and analyze its properties. Usually, testing and analyzing a model is cheaper and faster than fabricating and refabricating the product. *Note The Falling Body Model:: to continue.  File: acl2-doc-lemacs.info, Node: Models of Computer Hardware and Software, Next: Name the Formula Above, Prev: Models in Engineering, Up: Pages Written Especially for the Tours Models of Computer Hardware and Software Models of Computer Hardware and Software Computing machines, whether hardware or software or some combintation, are frequently modeled as "state machines." To so model a computing machine we must represent its states as objects in our mathematical framework. Transitions are functions or relations on state objects. In what language shall we define these objects, functions, and relations? The mathematical languages we were taught in high school algebra, geometry, trignometry, and calculus are inappropriate for modeling digital systems. They primarily let us talk about numbers and continuous functions. To see what kind of expressive power we need, take a closer look at what a typical state contains. Flying Tour: *Note A Typical State::  File: acl2-doc-lemacs.info, Node: Name the Formula Above, Next: Numbers in ACL2, Prev: Models of Computer Hardware and Software, Up: Pages Written Especially for the Tours Name the Formula Above Name the Formula Above When the theorem prover explicitly assigns a name, like *1, to a formula, it has decided to prove the formula by induction.  File: acl2-doc-lemacs.info, Node: Numbers in ACL2, Next: On the Naming of Subgoals, Prev: Name the Formula Above, Up: Pages Written Especially for the Tours Numbers in ACL2 Numbers in ACL2 The numbers in ACL2 can be partitioned into the following subtypes: Rationals Integers Positive integers 3 Zero 0 Negative Integers -3 Non-Integral Rationals Positive Non-Integral Rationals 19/3 Negative Non-Integral Rationals -22/7 Complex Rational Numbers #c(3 5/2) ; = 3+(5/2)i Signed integer constants are usually written (as illustrated above) as sequences of decimal digits, possibly preceded by + or -. Decimal points are not allowed. Integers may be written in binary, as in #b1011 (= 23) and #b-111 (= -7). Octal may also be used, #o-777 = -511. Non-integral rationals are written as a signed decimal integer and an unsigned decimal integer, separated by a slash. Complex rationals are written as #c(rpart ipart) where rpart and ipart are rationals. Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash is a non-integer). Similarly, #c(4/2 0) = #c(2 0) = 2. The common arithmetic functions and relations are denoted by +, -, *, /, =, <, <=, > and >=. However there are many others, e.g., floor, ceiling, and lognot. We suggest you *Note PROGRAMMING:: <> where we list all of the primitive ACL2 functions. Alternatively, see any Common Lisp language documentation. The primitive predicates for recognizing numbers are illustrated below. The following ACL2 function will classify an object, x, according to its numeric subtype, or else return 'NaN (not a number). We show it this way just to illustrate programming in ACL2. (defun classify-number (x) (cond ((rationalp x) (cond ((integerp x) (cond ((< 0 x) 'positive-integer) ((= 0 x) 'zero) (t 'negative-integer))) ((< 0 x) 'positive-non-integral-rational) (t 'negative-non-integral-rational))) ((complex-rationalp x) 'complex-rational) (t 'NaN)))  File: acl2-doc-lemacs.info, Node: On the Naming of Subgoals, Next: Other Requirements, Prev: Numbers in ACL2, Up: Pages Written Especially for the Tours On the Naming of Subgoals On the Naming of Subgoals Subgoal *1/2 is the induction step from the scheme, obtained by instantiating the scheme with our conjecture. We number the cases "backward", so this is case "2" of the proof of "*1". We number them backward so you can look at a subgoal number and get an estimate for how close you are to the end.  File: acl2-doc-lemacs.info, Node: Other Requirements, Next: Overview of the Expansion of ENDP in the Base Case, Prev: On the Naming of Subgoals, Up: Pages Written Especially for the Tours Other Requirements Other Requirements ACL2 is distributed on the Web without fee. There is a License agreement, which is available via the ACL2 Home Page link below. ACL2 currently runs on the Unix, Linux, and Macintosh operating systems. It can be built in any of the following Common Lisps: * Allegro, * GCL (Gnu Common Lisp) [or, AKCL], * Lispworks, * Lucid, and * MCL (Macintosh Common Lisp). We recommend running ACL2 with at least 16MB of memory and prefer significantly more (e.g., 64MB). Flying Tour: *Note The End of the Flying Tour::  File: acl2-doc-lemacs.info, Node: Overview of the Expansion of ENDP in the Base Case, Next: Overview of the Expansion of ENDP in the Induction Step, Prev: Other Requirements, Up: Pages Written Especially for the Tours Overview of the Expansion of ENDP in the Base Case Overview of the Expansion of ENDP in the Base Case Subgoal *1/1 is the Base Case of our induction. It simplifies to Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we saw in the earlier proof of Subgoal *1/2.  File: acl2-doc-lemacs.info, Node: Overview of the Expansion of ENDP in the Induction Step, Next: Overview of the Final Simplification in the Base Case, Prev: Overview of the Expansion of ENDP in the Base Case, Up: Pages Written Especially for the Tours Overview of the Expansion of ENDP in the Induction Step Overview of the Expansion of ENDP in the Induction Step In this message the system is saying that Subgoal *1/2 has been rewritten to the Subgoal *1/2', by expanding the definition of endp. This is an example of simplification, one of the main proof techniques used by the theorem prover. *Note The Expansion of ENDP in the Induction Step (Step 0):: if you would like to step through the simplification of Subgoal *1/2.  File: acl2-doc-lemacs.info, Node: Overview of the Final Simplification in the Base Case, Next: Overview of the Proof of a Trivial Consequence, Prev: Overview of the Expansion of ENDP in the Induction Step, Up: Pages Written Especially for the Tours Overview of the Final Simplification in the Base Case Overview of the Final Simplification in the Base Case The But is our signal that the goal is proved. *Note The Final Simplification in the Base Case (Step 0):: to step through the proof. It is very simple.  File: acl2-doc-lemacs.info, Node: Overview of the Proof of a Trivial Consequence, Next: Overview of the Simplification of the Base Case to T, Prev: Overview of the Final Simplification in the Base Case, Up: Pages Written Especially for the Tours Overview of the Proof of a Trivial Consequence Overview of the Proof of a Trivial Consequence ACL2 !>(defthm trivial-consequence (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))) ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...): The previously added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture to Goal' (EQUAL (APP X1 (APP X2 (APP X3 (APP X4 (APP X5 (APP X6 X7)))))) (APP X1 (APP X2 (APP X3 (APP X4 (APP X5 (APP X6 X7))))))). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM TRIVIAL-CONSEQUENCE ...) Rules: ((:REWRITE ASSOCIATIVITY-OF-APP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume Time: 0.20 seconds (prove: 0.02, print: 0.00, other: 0.18) TRIVIAL-CONSEQUENCE You might explore the links before moving on. Walking Tour: *Note The End of the Walking Tour::  File: acl2-doc-lemacs.info, Node: Overview of the Simplification of the Base Case to T, Next: Overview of the Simplification of the Induction Conclusion, Prev: Overview of the Proof of a Trivial Consequence, Up: Pages Written Especially for the Tours Overview of the Simplification of the Base Case to T Overview of the Simplification of the Base Case to T Subgoal *1/1 (IMPLIES (ENDP A) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Walking Tour: *Note The End of the Proof of the Associativity of App::  File: acl2-doc-lemacs.info, Node: Overview of the Simplification of the Induction Conclusion, Next: Overview of the Simplification of the Induction Step to T, Prev: Overview of the Simplification of the Base Case to T, Up: Pages Written Especially for the Tours Overview of the Simplification of the Induction Conclusion Overview of the Simplification of the Induction Conclusion In this message the system is saying that Subgoal *1/2' has been rewritten T using the rules noted. The word "But" at the beginning of the sentence is a signal that the goal has been proved. *Note The Simplification of the Induction Conclusion (Step 0):: to step through the proof of Subgoal *1/2'.  File: acl2-doc-lemacs.info, Node: Overview of the Simplification of the Induction Step to T, Next: Perhaps, Prev: Overview of the Simplification of the Induction Conclusion, Up: Pages Written Especially for the Tours Overview of the Simplification of the Induction Step to T Overview of the Simplification of the Induction Step to T Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). But simplification reduces this to T, using the :definition APP, the :rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning. Walking Tour: *Note Overview of the Simplification of the Base Case to T::  File: acl2-doc-lemacs.info, Node: Perhaps, Next: Popping out of an Inductive Proof, Prev: Overview of the Simplification of the Induction Step to T, Up: Pages Written Especially for the Tours Perhaps Perhaps The theorem prover's proof is printed in real time. At the time it prints "Perhaps" it does not know the proof will succeed.  File: acl2-doc-lemacs.info, Node: Popping out of an Inductive Proof, Next: Proving Theorems about Models, Prev: Perhaps, Up: Pages Written Especially for the Tours Popping out of an Inductive Proof Popping out of an Inductive Proof Recall that our induction scheme (*Note The Proof of the Associativity of App:: to revisit it) had two cases, the induction step (Subgoal *1/2) and the base case (Subgoal *1/1). Both have been proved!  File: acl2-doc-lemacs.info, Node: Proving Theorems about Models, Next: Revisiting the Admission of App, Prev: Popping out of an Inductive Proof, Up: Pages Written Especially for the Tours Proving Theorems about Models Proving Theorems about Models But ACL2 is a logic. We can prove theorems about the model. Theorem. MC 'mult is a multiplier (implies (and (natp x) (natp y)) (equal (lookup 'z (mc (s 'mult x y) (mclk x))) (* x y))). This theorem says that a certain program running on the mc machine will correctly multiply any two natural numbers. It is a statement about an infinite number of test cases! We know it is true about the model because we proved it. Flying Tour: *Note What is Required of the User(Q)::  File: acl2-doc-lemacs.info, Node: Revisiting the Admission of App, Next: Rewrite Rules are Generated from DEFTHM Events, Prev: Proving Theorems about Models, Up: Pages Written Especially for the Tours Revisiting the Admission of App Revisiting the Admission of App Here is the definition of app again with certain parts highlighted. If you are taking the Walking Tour, please read the text carefully and click on each of the links below, except those marked <>. Then come back here. ACL2 !>(defun app (x y) (cond ((endp x) y) (t (cons (car x) (app (cdr x) y))))) The admission of APP is trivial, using the relation E0-ORD-< <> (which is known to be well-founded on the domain recognized by E0-ORDINALP <>) and the measure (ACL2-COUNT <> X). We observe that the type of APP is described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive type reasoning. Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) APP Walking Tour: *Note Evaluating App on Sample Input::  File: acl2-doc-lemacs.info, Node: Rewrite Rules are Generated from DEFTHM Events, Next: Running Models, Prev: Revisiting the Admission of App, Up: Pages Written Especially for the Tours Rewrite Rules are Generated from DEFTHM Events Rewrite Rules are Generated from DEFTHM Events By reading the documentation of defthm <> (and especially of its :rule-classes <> argument) you would learn that when we submitted the command (defthm associativity-of-app (equal (app (app a b) c) (app a (app b c)))) we not only command the system to prove that app is an associative function but * we commanded it to use that fact as a rewrite rule. That means that every time the system encounters a term of the form (app (app x y) z) it will replace it with (app x (app y z))! Walking Tour: *Note You Must Think about the Use of a Formula as a Rule::  File: acl2-doc-lemacs.info, Node: Running Models, Next: STATE is the Only Variable in Top-Level Forms, Prev: Rewrite Rules are Generated from DEFTHM Events, Up: Pages Written Especially for the Tours Running Models Running Models Suppose the machine being modeled is some kind of arithmetic unit. Suppose the model can be initialized so as to multiply x times y and leave the answer in z. Then if we initialize s to multiply with x=5 and y=7 and run the machine long enough, we can read the answer 35 in the final state. Because ACL2 is a programming language, our model can be run or executed. If you defined the model in ACL2 and then typed > (lookup 'z (mc (s 'mult 5 7) 29)) then ACL2 would compute 35. You can emulate or test the model of your machine. This is obvious because ACL2 is Common Lisp; and Common Lisp is a programming language. Flying Tour: *Note Symbolic Execution of Models::  File: acl2-doc-lemacs.info, Node: STATE is the Only Variable in Top-Level Forms, Next: Subsumption of Induction Candidates in App Example, Prev: Running Models, Up: Pages Written Especially for the Tours STATE is the Only Variable in Top-Level Forms STATE is the Only Variable in Top-Level Forms ACL2!>(equal (app (app a b) c) (app a (app b c)))) ACL2 Error in TOP-LEVEL: STATE is the only variable we permit to occur freely in expressions to be evaluated, but C, B and A occur freely in (EQUAL (APP (APP A B) C) (APP A (APP B C))). Embed symbols in (@ *) to access their global values. This cryptic message means: you can't evaluate terms containing unbound or free variables like a, b and c above. Actually, one free variable is permitted in top-level forms: the variable state <>, which denotes the current ACL2 state and which is given very special treatment in this applicative programming language. We do not discuss state here. ACL2 provides a way for you to use state to save values of computations at the top-level and refer to them later. See assign <> and @ <>.  File: acl2-doc-lemacs.info, Node: Subsumption of Induction Candidates in App Example, Next: Suggested Inductions in the Associativity of App Example, Prev: STATE is the Only Variable in Top-Level Forms, Up: Pages Written Especially for the Tours Subsumption of Induction Candidates in App Example Subsumption of Induction Candidates in App Example After collecting induction suggestions from these three terms (app a b) (app b c) (app a (app b c)) the system notices that the first and last suggest the same decomposition of a. So we are left with two ideas about how to induct: Decompose a as we would to unwind (app a b). Decompose b as we would to unwind (app b c).  File: acl2-doc-lemacs.info, Node: Suggested Inductions in the Associativity of App Example, Next: Symbolic Execution of Models, Prev: Subsumption of Induction Candidates in App Example, Up: Pages Written Especially for the Tours Suggested Inductions in the Associativity of App Example Suggested Inductions in the Associativity of App Example To find a plausible induction argument, the system studies the recursions exhibited by the terms in the conjecture. Roughly speaking, a call of a recursive function "suggests" an induction if the argument position decomposed in recursion is occupied by a variable. In this conjecture, three terms suggest inductions: (app a b) (app b c) (app a (app b c)) The variable recursively decomposed is indicated in bold.  File: acl2-doc-lemacs.info, Node: Symbolic Execution of Models, Next: The Admission of App, Prev: Suggested Inductions in the Associativity of App Example, Up: Pages Written Especially for the Tours Symbolic Execution of Models Symbolic Execution of Models But ACL2 is more than a programming language. Initialize x to 5 and let y be any legal value. Because ACL2 is a mathematical language, we can simplify the expression (lookup 'z (mc (s 'mult 5 y) 29)) and get (+ y y y y y). This is symbolic execution because not all of the parameters are known. Flying Tour: *Note Proving Theorems about Models::  File: acl2-doc-lemacs.info, Node: The Admission of App, Next: The Associativity of App, Prev: Symbolic Execution of Models, Up: Pages Written Especially for the Tours The Admission of App The Admission of App Here is what it looks like to submit the definition of app to ACL2: ACL2 !>(defun app (x y) (cond ((endp x) y) (t (cons (car x) (app (cdr x) y))))) The admission of APP is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of APP is described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive type reasoning. Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) APP The text between the lines above is one interaction with the ACL2 command loop. Above you see the user's input and how the system responds. This little example shows you what the syntax looks like and is a very typical successful interaction with the definitional principle. Let's look at it a little more closely. Walking Tour: *Note Revisiting the Admission of App::  File: acl2-doc-lemacs.info, Node: The Associativity of App, Next: The Base Case in the App Example, Prev: The Admission of App, Up: Pages Written Especially for the Tours The Associativity of App The Associativity of App ACL2!>(let ((a '(1 2)) (b '(3 4)) (c '(5 6))) (equal (app (app a b) c) (app a (app b c)))) T Observe that, for the particular a, b, and c above, (app (app a b) c) returns the same thing as (app a (app b c)). Perhaps app is associative. Of course, to be associative means that the above property must hold for all values of a, b, and c, not just the ones tested above. Wouldn't it be cool if you could type ACL2!>(equal (app (app a b) c) (app a (app b c)))) and have ACL2 compute the value T? Well, you can't! If you try it, you'll get an error message! The message says we can't evaluate that form because it contains free variables, i.e., variables not given values. *Note STATE is the Only Variable in Top-Level Forms:: to see the message. 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. Walking Tour: *Note The Theorem that App is Associative::  File: acl2-doc-lemacs.info, Node: The Base Case in the App Example, Next: The End of the Flying Tour, Prev: The Associativity of App, Up: Pages Written Especially for the Tours The Base Case in the App Example The Base Case in the App Example This formula is the Base Case. It consists of two parts, a test identifying the non-inductive case and the conjecture to prove. (IMPLIES (ENDP A) ; Test (:P A B C)) ; Conjecture When we prove this we can assume * A is empty and we have to prove the conjecture for A.