next up previous contents
Next: Register-Transfer Logic Up: Contents Previous: Preface   Contents


Preface to the Hypertext Edition

This edition is intended primarily as an on-line user's manual for the associated ACL2 library of register-transfer logic and computer arithmetic, which is publicly available as a part of the standard ACL2 release through the University of Texas Web site, at

http://www.cs.utexas.edu/~moore/acl2.
Specifically, it may be found in the /books/rtl subdirectory of the ACL2 sources.

This document was generated using the LaTeX2HTML translator in order to facilitate its navigation with a Web browser. One feature provided by LaTeX2HTML is a hypertext link associated with every reference to a definition, lemma, or other labeled location in the text, thereby providing for its immediate retrieval. For example, this link to Lemma 6.2.1 of Chapter 6 may be followed with a click of the mouse, after which the browser's back button may be used to return the user to this preface.

Furthermore, for the purpose of this document, the HTML translation has been extended with a second pass, consisting of several Perl scripts that generate Javascript code and embed it in the HTML. This code implements a number of navigation features that are not provided by LaTeX2HTML. The most important of these is a facility for connecting the results appearing in this exposition with corresponding events in the ACL2 code. Each chapter of this document corresponds to a book, i.e., a file of events, in the ACL2 library, and each definition or lemma that is listed here relates to one or more ACL2 events. In most cases, this correspondence is one-one and the order of events in a book is preserved in the corresponding chapter.

Every definition or result is preceded by the name of the corresponding ACL2 event, as illustrated below.

  (flt-4) There exist no positive integers $ x$ , $ y$ , and $ z$ such that

$\displaystyle x^4 + y^4 = z^4.$

PROOF: This result is easily established by the method of infinite descent. 

Definition 0.0.1   (primep) A prime is an integer greater than 1 that has no proper divisors.

  (flt-prime) If p is an odd prime, then there exist no positive integers $ x$ , $ y$ , and $ z$ such that

$\displaystyle x^p + y^p = z^p.$

PROOF: I have discovered a marvelous proof to this theorem, which this margin is too narrow to contain. 

  (flt) If $ n$ is an integer greater than 2, then there exist no positive integers $ x$ , $ y$ , and $ z$ such that

$\displaystyle x^n + y^n = z^n.$

PROOF: Suppose we have a counterexample, $ x^n + y^n = z^n$ , where $ n>2$ . Then either $ n$ is a power of 2, in which case it is divisible by 4, or $ n$ is divisible by an odd prime $ p$ . In the first case, we may write $ n=4k$ and hence,

$\displaystyle (x^k)^4 + (y^k)^4 = (z^k)^4,$

contradicting Lemma 0.0.1. Similarly, in the second case, $ n=pk$ and

$\displaystyle (x^k)^p + (y^k)^p = (z^k)^p,$

contradicting Theorem 0.1. 


Note that these event names are mouse-sensitive. When the user clicks on an event name in this window, the event appears in a second window, which is automatically created for the purpose of displaying ACL2 code. Similarly, clicling on the name of an event in the code window causes the informal version to appear in this window.

The events of interest are of two classes: defun and defthm. Definitions in the text usually correspond to defun events (although there are exceptions, e.g., Definition 1.1.1), and all derived results correspond to defthm events. Most results are labelled as lemmas, but several are classified instead as theorems for the sake of emphasis, and some as corollaries to suggest their dependence on preceding results. This classification is somewhat arbitrary has no significance from the formal (ACL2) perspective.

It is an important aspect of the theory that it has been completely formalized in the ACL2 logic. Consequently, every result appearing in the text is represented in the ACL2 code. In general, the formalization is straightforward, as illustrated by the foregoing example. In some cases, however, the user will notice the the hypotheses of defthm events are weaker than the informal versions. For example, a hypothesis in the text version of a lemma stipulating that a variable $ n$ is integer-valued might be replaced in the formalization by (rationalp n), or even omitted altogether. Thus, the statement that was proved mechanically is actually stronger than that which is claimed in the text. When this occurs, it may be assumed that the text version captures the cases of interest while the weakening of hypotheses in the formal version serves to speed up the application of the lemma by simplifying the task of the rewriter.

Moreover, the correspondence between informal results and defthm events is not quite bijective. Some events that are included for technical reasons are not sufficiently interesting from the user's perspective to be represented in the text. In other cases, for the sake of readability, several ACL2 events are combined into a single lemma. When this occurs, the events are grouped together in the ACL2 file and the text lemma is linked to the first event in the group.

Another Javascript enhancement to the HTML translation is a facility for enabling and disabling the display of proofs. It is understood that some users may be interested in reading and applying the results contained in this exposition without being encumbered by their proofs. Therefore, no proofs are displayed when a section is first read into the browser window. In order to exhibit the proof of a result, the reader may click on its name, e.g., Corollary 0.0.2 above. The display of a proof may then be disabled by clicking on the red box () appearing at its end.

This effort is my first experience with each of three languages--LaTeX2HTML, Perl, and Javascript--all of which continue to hold considerable mystery for me. It all seems to work well enough with the Konqueror Web browser, which was used in its development, but I suspect that other browsers may yield different results. Mozilla has a known bug that causes many LaTeX2HTML-generated images to be improperly aligned, but I have been advised that this will be fixed soon. Please report any other problems to david@russinoff.com.

D.M.R.
Block Island, Rhode Island
November, 2005

next up previous contents
Next: Register-Transfer Logic Up: Contents Previous: Preface   Contents
David Russinoff 2007-01-03