		Search-engine friendly clone of the ACL2 documentation.

About-ACL2

Soundness

Correctness property claimed for ACL2

What can we conclude when we use ACL2 to prove a formula or to compute the value of an expression? This topic provides a high-level sketch of an answer.

Overview of the ACL2 logic

Any notion of correctness of ACL2 necessarily depends on the logic that it is intended to implement. At its core, the ACL2 logic is just classical first-order logic. The first-order theory for a given ACL2 session, which we may call the “prover's theory”, is the result of extending its set of built-in axioms according to events that have been executed in the session.

The built-in axioms describe properties of the ACL2 data types, such as the following.

ACL2 !>:pe car-cons
       -8139  (DEFAXIOM CAR-CONS
                (EQUAL (CAR (CONS X Y)) X))
ACL2 !>

A key extension principle is the Principle of Definition, which, for a definition (defun <fn> <args> <body>), introduces an axiom equating <body> with application of <fn> to <args>. This principle permits recursion, and even mutual-recursion, provided a suitable measure conjecture is provable.
Other events come with extension principles too, including encapsulate, defchoose, defpkg, and include-book. Note that from a logical perspective, defstobj and defabsstobj just provide definitional extensions.
Each ACL2 theory is closed under induction: that is, every instance of induction (in the language of the theory) below the ordinal epsilon-0 (see ordinals) is also in the theory. In practical terms, this is what allows ACL2 to prove theorems by induction.

For more about the ACL2 logic see the following publications by Matt Kaufmann and J Moore.

“A Precise Description of the ACL2 Logic” (April, 1998).
“Structured Theory Development for a Mechanized Logic”, Journal of Automated Reasoning 26, no. 2 (2001) 161-203.

The soundness property for ACL2 sessions

The following soundness property is key for a given ACL2 session.

The theorem prover proves only formulas that are theorems in the corresponding prover's theory in that session.

Note that the theorem prover uses evaluation during proofs. The soundness property thus encompasses the following: when such evaluation of a term tm produces a value v, then (equal tm 'v) is provable from the context of that evaluation. Evaluation in the top-level loop has such a property as well, but because of attachments (see defattach) and apply$, provability is with respect to a larger “evaluation theory”; see guarantees-of-the-top-level-loop.

Constraints on the soundness guarantee

Here is a list of constraints on the soundness guarantee.

The prover's theory of a session is construed to include all axioms introduced by hidden defpkg events. See hidden-death-package.
There is no soundness guarantee for a session in which there is raw Lisp evaluation with side effects. (ACL2 normally avoids putting the user into raw Lisp, but this can happen with an interrupt, the use of break$, or explicitly leaving the top-level loop with :q.) “Side effects” should be interpreted as generously as possible: this certainly includes redefining a function or assigning to a variable, but not merely evaluating an arithmetic expression, for example.
There is no soundness guarantee for a session in which any trust tag has been installed (see defttag). The absence of trust tags is guaranteed by the absence of “TTAG NOTE” being printed to standard output (that is, to *standard-co*).
The soundness guarantee only applies when a set of books is certified from scratch, including community-books, in a single environment — in particular, with the same Lisp implementation and operating system. (In practice this is often not an issue.)

Examples of divergence among Lisp implementations

Next, we provide examples illustrating the last point above, restricting to the use of a single Lisp.

Example 1: Divergences involving character and string operations.

Consider the following log in raw Lisp using SBCL, which introduces versions of characters “A” and “a” that are augmented with an “acute” accent.

* (code-char 193)
#LATIN_CAPITAL_LETTER_A_WITH_ACUTE
* (code-char 225)
#LATIN_SMALL_LETTER_A_WITH_ACUTE
*

While most Lisps that host ACL2 consider these two characters to be alphabetic characters with case (upper and lower, respectively), GCL does not (at least, a version available as of this writing).

(alpha-char-p (code-char 193)) ; T except NIL in GCL
(alpha-char-p (code-char 225)) ; T except NIL in GCL
(upper-case-p (code-char 193)) ; T except NIL in GCL
(lower-case-p (code-char 225)) ; T except NIL in GCL
(char-code (char-downcase (code-char 193))) ; 225 except 193 in GCL
(char-code (char-upcase (code-char 225)))   ; 193 except 225 in GCL
(let ((s (string-downcase (string (code-char 193)))))
  (char-code (char s 0)))      ; 225 except 193 in GCL
(let ((s (string-upcase (string (code-char 225)))))
  (char-code (char s 0)))      ; 193 except 225 in GCL

Example 2: Another divergence for alpha-char-p.

; True in SBCL 2.4.2, about the character it calls #MICRO_SIGN,
; but false in LispWorks 8.0.1:
(alpha-char-p (code-char 181))

; False in SBCL 2.4.2, about the character it calls #CENT_SIGN,
; but true in Allegro CL 10.1:
(alpha-char-p (code-char 162))

Example 3: A divergence involving a floating-point computation.

Here is another example illustrating the requirement on a single Lisp. In ACL2 built on most host Lisp implementations, one can admit the following event. (See df for background on floating-point computations with ACL2.)

(defthm usual-sin-2pi
  (equal (df-sin (df* 2 *df-pi*))
         #d-2.4492935982947064E-16))

But in ACL2 built on LispWorks, one can instead admit the following.

(defthm lispworks-sin-2pi
  (equal (df-sin (df* 2 *df-pi*))
         #d-2.4492127076447545E-16))

Clearly one could prove nil by including two books, one containing each of these theorems. (Aside: This does not violate the IEEE-754 spec, since it does not make specific requirements for trigonometric functions.)

Subtopics

Guarantees-of-the-top-level-loop: Guarantees provided by top-level evaluation