15 lines
9.5 KiB
Plaintext
15 lines
9.5 KiB
Plaintext
|
<html>
|
||
|
|
<head></head>
|
||
|
|
<body>
|
||
|
|
* Machine reasoning about machines: ACL2 theorem prover J. Strother Moore, (University of Texas, Austin) PADL2002 Invited Talk, January 20, 2002. J. Strother Moore <http: www.cs.utexas.edu users moore /> is well-known for the Boyer-Moore string matching algorithm and the Boyer-Moore theorem prover. The talk was quite different from the paper (published in LNCS 2257). The paper, entitled "Single-Threaded Objects in ACL2", deals with ACL2's "version" of Haskell monads. The PADL talk was about history, abilities and lessons of the ACL2 prover. ACL2 stands for "A Computational Logic for Applicative Common Lisp". It is the second incarnation of "The Boyer-Moore Theorem Prover (NQTHM)". The original NQTHM project started back in the 1971, when Moore was a PhD student at the U. of Edinburgh after graduating from MIT, and when he met Boyer. They were influenced by Woody Bledsoe and an insight that proving theorems by resolution was actually _programming_ in predicate calculus. The collaboration between Moore and Boyer continued for twenty years. Both moved around the country, and ended up at the U. of Texas (Austin). And then all of the sudden Boyer got interested in philosophy. He is now a professor in the Dept of philosophy at U.Texas (Austin), and teaches Plato and Socrates as well as the introductory Set theory for CS majors. J. Moore mentioned that his department still receives letters addressed to "Professor Boyer-Moore". NQTHM uses Lisp code as logic, to express theorems. The prover is written also in (a home-grown dialect of) Lisp. The logic is first order and has no quantifiers. The prover however is adept in inductive proofs. The first result of the Boyer-Moore prover was the proof of the existence of a list with three elements. Then they proved that the list append is associative, and the prime factorization is unique. The prover got smarter and acquired the knowledge of natural, integral and rational numbers (along with their equality and inequality properties), binary decision diagrams (BDDs), and congruence-based re-writing. http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/innovations.html Each proven lemma is automatically added to the database of known true facts -- and can immediately be used in proving other theorems. We can also prove re-writing rules and reasoning strategies -- and add them to the database for later use. The prover becomes smarter with every successful proof. The brief ACL2 tutorial http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html gives the flavor of the logic and the prover. In the 80s, Boyer, Moore and their students proved undecidability of the halting problem, and the Goedel First incompleteness theorem. The latter proof required 2000 lemmas. They proceeded to prove the design of a sample microprocessor, the correctness of the assembler for the micro-processor, and even the correctness of a simple OS. See http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/index.html for the complete list of proved results. One of the notable results of ACL2 was a proof that the floating-point unit (FPU) of the AMD Athlon processor executes elementary FP operations (additions, subtraction, multiplication, division and the square root) strictly according to the IEEE specification. To be precise, they proved that the unit that operates 'extended precision' FP numbers is correct. The regular FP numbers are converted to the extended format by a separate hardware unit, which also deals with unnormalized numbers, NaNs and infinities. This was at a time of a Pentium FDIV scandal. AMD management was terrified to think that the upcoming Athlon may have some rare but immensely embarrassing bug. The FP unit was specified in a Register Transfer Language (RTL) -- a common hardware description language that describes registers of various logical/arithmetical components and data transfers. To prove the correctness of FPU, Moore and his group had to develop a translator from RTL to ACL2, the input language of the prover. Moore had to convince the AMD management that the translation is sound. Alas, RTL
|
||
|
|
<pre>ACL2 !>(defun rev (x)
|
||
|
|
(if (endp x)
|
||
|
|
nil
|
||
|
|
(append (rev (cdr x))
|
||
|
|
(list (car x)))))
|
||
|
|
</pre> The system responds with
|
||
|
|
<blockquote>
|
||
|
|
The admission of REV 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 REV is described by the theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)). We used primitive type reasoning and the :type-prescription rule BINARY- APPEND.
|
||
|
|
</blockquote> Note how the system figured out the type of rev. The type is formulated as a theorem, which can be proved by ACL2 and then used as a side condition whenever function rev is applied. Curry-Howard isomorphism in action! For that reason, a static type system is not necessary. Still, J. Moore keeps an open mind. When asked what he would do if he started with an empty Emacs buffer now, he replied that he would give Haskell a very hard look. One of his (former) students is playing with Haskell to this end; so far, Moore said, he was able to closely and elegantly emulate in ACL2 all the Haskell code that person sent him. J. Moore is a bit concerned how Haskell will play out in terms of performance. He didn't mention any studies though. The speaker couldn't avoid a question about Boyer-Moore string matching algorithm. He said that its discovery was one of the "Aha" moments -- one day in California.
|
||
|
|
</body>
|
||
|
|
</html>
|