REAL

ACL2(r) support for real numbers 
Major Section:  ACL2 Documentation

ACL2 supports rational numbers but not real numbers. However, starting with Version 2.5, a variant of ACL2 called ``ACL2(r)'' supports the real numbers by way of non-standard analysis. ACL2(r) was conceived and first implemented by Ruben Gamboa in his Ph.D. dissertation work, supervised by Bob Boyer with active participation by Matt Kaufmann. The makefile provided with ACL2 has targets small-acl2r and large-acl2r for building ACL2(r) images. To see which image you have, see if the prompt includes the string ``(r)'', e.g.: 

ACL2(r) !>
Or, look at *acl2-version* and see if ``(r)'' is a substring.

In ACL2 (as opposed to ACL2(r)), when we say ``real'' we mean ``rational.''

Caution: ACL2(r) should be considered experimental as of Version 2.5: although we (Kaufmann and Moore) have carefully completed Gamboa's integration of the reals into the ACL2 source code, our primary concern to date has been to ensure unchanged behavior when ACL2 is compiled in the default manner, i.e., without the non-standard extensions. As for every release of ACL2, at the time of this release we believe ACL2 Version 2.5 is sound. We are confident that ACL2(r) will behave much as it does now and will ultimately be sound; but we have not yet argued the soundness of every detail of the integration.

There is only limited documentation on the non-standard features of ACL2(r). We hope to provide more documentation for such features in future releases. Please feel free to query the authors if you are interested in learning more about ACL2(r). Gamboa's dissertation may also be helpful.












































































I-CLOSE

ACL2(r) test for whether two numbers are infinitesimally close 
Major Section:  REAL

(I-close x y) is true if and only if x-y is an infinitesimal number. This predicate is only defined in ACL2(r) (see real).














































































I-LARGE

ACL2(r) recognizer for infinitely large numbers 
Major Section:  REAL

(I-large x) is true if and only if x is non-zero and 1/x is an infinitesimal number. This predicate is only defined in ACL2(r) (see real).














































































I-LIMITED

ACL2(r) recognizer for limited numbers 
Major Section:  REAL

(I-limited x) is true if and only if x is a number that is not infinitely large. This predicate is only defined in ACL2(r) (see real).














































































I-SMALL

ACL2(r) recognizer for infinitesimal numbers 
Major Section:  REAL

(I-small x) is true if and only if x is an infinitesimal number (possibly 0). This predicate is only defined in ACL2(r) (see real).














































































REAL-LISTP

ACL2(r) recognizer for a true list of real numbers 
Major Section:  REAL

The predicate real-listp tests whether its argument is a true list of real numbers. This predicate is only defined in ACL2(r) (see real).














































































STANDARD-NUMBERP

ACL2(r) recognizer for standard numbers 
Major Section:  REAL

(Standard-numberp x) is true if and only if x is a ``standard'' number. This notion of ``standard'' comes from non-standard analysis and is discussed in Ruben Gamboa's dissertation. In brief, all the familiar real number are standard, but non-zero infinitesimals are not standard, nor are numbers that exceed every integer that you can express in the usual way (1, 2, 3, and so on). The set of standard numbers is closed under the usual arithmetic operations, hence the sum of a standard number and a non-zero infinitesimal is not standard, though it is what is called ``limited'' (see i-limited).

This predicate is only defined in ACL2(r) (see real).














































































STANDARD-PART

ACL2(r) function mapping limited numbers to standard numbers 
Major Section:  REAL

(Standard-part x) is, for a given i-limited number x, the unique real number infinitesimally close (see i-close) to x. This function is only defined in ACL2(r) (see real).