A Brief Informal Introduction to Non-Standard Analysis and ACL2(r)
Extra ACL2 Seminar
Matt Kaufmann, 2/3/2015

Table of Contents:

I. Introduction
   A. Goal for today's talk
   B. What is ACL2(r)?
   C. Brief introduction to the derivative in non-standard analysis
   D. Brief introduction to the derivative in ACL2(r)
   E. Remark on quantifiers

II. Foundations very briefly
   A. Two basic approaches to the foundations
   B. Non-standard reals using the Compactness Theorem
   C. Non-standard reals via an ultrapower construction
   D. Superstructures

III. Non-standard basics
   A. Basic notions
   B. The transfer principle
   C. Defun-std

IV.  ACL2(r) example

V. Sketches for cool hand proofs, time permitting

VI. Conclusion

====================

I. Introduction

----------

A. Goal for today's talk

   The goal is to provide some basic understanding and intuition for
   non-standard ("hyperreal") notions and ACL2(r).  I'll largely avoid
   rigor and details, as the real goal is to provide sufficient
   background so that next week's seminar talk by Cuong Chau will seem
   natural and make sense.

   Other introductory resources include:
   - :Doc real
   - Keisler's freshman calculus book
     (http://www.math.wisc.edu/~keisler/calc.html)
     provides a nice introduction to non-standard analysis.
     In particular, see Chapter 1 starting with Section 1.4 (page 21):
     http://www.math.wisc.edu/~keisler/chapter_1b.pdf
   - The Wikipedia article looks decent to me (after a quick scan):
     http://en.wikipedia.org/wiki/Non-standard_analysis

----------

B. What is ACL2(r)?

   (i)   The "r" in ACL2(r) stands for "reals" or "Ruben".

   (ii)  Ruben Gamboa still maintains ACL2(r), though we keep its code
         integrated with the ACL2 source code.
         To build an ACL2(r) executable, just build ACL2 this way.

           make large-acl2r LISP=<your_lisp>

         For more, see :doc real.

   (iii) ACL2(r) enables reasoning about the reals, but has a
         different ground-zero theory than ACL2.

         Example: (i-large-integer) is an integer constant that is
         greater than 1, greater than 2, etc.  So the value
         (/ 1 (i-large-integer)) is a non-zero "infinitesimal";
         more on that notion, which we often call "i-small", below.

         Example: ACL2 proves that 2 has no square root, while
         ACL2(r) allows us to define the square root of 2.

;;; Proved in ACL2
; (in books/nonstd/sqrt/no-sqrt.lisp,
;  after changing realp to real/rationalp
;  and complexp to complex-rationalp
;  to get no-sqrt-std.lisp, saved in this directory):
(include-book "no-sqrt-std")
(thm
 (not (equal (* x x) 2))
 :hints (("Goal" :use irrational-sqrt-2)))

;;; Proved in ACL2(r):
(include-book "nonstd/nsa/sqrt" :dir :system)
(thm
 (let ((x (acl2-sqrt 2)))
   (equal (* x x) 2))
 :hints (("Goal" :use ((:instance sqrt-sqrt (x 2))))))

; More generally, here is the theorem :USEd just above:
(defthm-std sqrt-sqrt ; sqrt*sqrt = the number
  (implies (and (realp x)
                (<= 0 x))
           (equal (* (acl2-sqrt x) (acl2-sqrt x)) x))
  :hints ...)

----------

C. Brief introduction to the derivative in non-standard analysis

   Looky here, we're going to avoid limits (and quantifiers)!

   Consider for example this "definition" of the derivative.

   f'(x) = [f(x+h) - f(x)]/h where h is a non-zero "infinitesimal".

   For example, if f(x) = x^2, we get:

   f'(x) "=" [x^2 + 2xh + h^2 - x^2]/h = 2x + h

   This doesn't quite work, because we really want 2x, and h isn't
   zero.

   Let's back up....
   Way back....
   The caveman only believed in natural numbers.
   Then there were integers and then rationals and then reals.
   And then complexes, matrices, arbitrary fields, blah blah blah....

   Suspend disbelief for a moment and imagine an extension of the
   reals that "fills in" little tiny "infinitesimal" numbers.

   Solution:

   f'(x) = standard-part([f(x+h) - f(x)]/h)
           where h is a non-zero "infinitesimal".

   For f(x) = x^2, this gives us
   f'(x) = standard-part(2x+h) = 2x.

   Of course, we need to get our heads around notions of
   "infinitesimal" and "standard-part".  More on that later....

----------

D. Brief introduction to the derivative in ACL2(r)

   So for fun, let's start by exploring the notion of derivative in
   ACL2(r).  (This is a simplification of the definition in
   books/nonstd/nsa/derivatives.lisp.)
   NOTE: We'll back up later and look more carefully at what's going
   on here.  But I thought it might be helpful to see some "code"
   before going all "mathy".

(encapsulate
 (((rdf *) => *)) ; real differentiable function
 (local (defun rdf (x) (declare (ignore x)) 0))
 (defthm realp-rdf
   (implies (realp x)
            (realp (rdf x))))
 (defun differential-rdf (x eps)
   (/ (- (rdf (+ x eps))
         (rdf x))
      eps))
 (defthm rdf-differentiable-1
   (implies (and (standardp x)
                 (realp x)
                 (i-small e) (not (equal e 0)))
            (i-limited (differential-rdf x e))))
 (defthm rdf-differentiable-2
   (implies (and (standardp x)
                 (realp x)
                 (i-small e1) (not (equal e1 0))
                 (i-small e2) (not (equal e2 0)))
            (i-close (differential-rdf x e1)
                     (differential-rdf x e2)))))

(defun i-small-real ()
  (declare (xargs :guard t))
  (/ (i-large-integer)))

(defthm i-small-real-is-small
  (equal (standard-part (i-small-real))
         0)
  :hints (("Goal"
           :in-theory (disable i-large-integer-is-large)
           :use i-large-integer-is-large)))

(in-theory (disable differential-rdf
                    i-small-real
                    (i-small-real)))

(defun-std rdf-prime (x)
  (standard-part
   (differential-rdf (realfix x)
                     (i-small-real))))

----------

E. Remark on quantifiers

   Notice that there are no quantifiers!  That's one reason that
   non-standard analysis a particularly nice way to reason about the
   real numbers in a system like ACL2 (i.e., with limited support for
   quantification).  As for derivatives, we do limits in general
   without quantifiers in ACL2(r).

====================

II. Foundations very briefly

----------

A. Two basic approaches to the foundations

   (1) (Essentially, Abraham Robinson's approach)
       Extend the usual reals to a bigger set of "hyperreals", which
       includes infinitesimals.  Actually extend the set of functions
       on the reals, etc. (more on that below).

   (2) Nelson's Internal Set Theory views the "reals" as "all the
       reals", including infinitesimals, and considers a subset of
       "standard" reals.

   Ruben uses (2).  But today I'll stick to (1), which I think is
   more intuitive for those not going deeply into non-standard
   analysis.

----------

B. Non-standard reals using the Compactness Theorem

   The Compactness Theorem of first-order logic says that for a set of
   first-order sentences to be satisfiable, it suffices that every
   finite subset is satisfiable.

   - Take ACL2 ground-zero theory and add these axioms:
     (integerp (i-large-integer))
     (> (i-large-integer) 0)
     (> (i-large-integer) 1)
     (> (i-large-integer) 2)
     ...
     (> (i-large-integer) 100000)
     ...
     (> (i-large-integer) 10000000000000000000000)
     ...

     CLAIM: Every finite subset of these axioms is satisfiable.

     PROOF: Given a finite subset, interpret (i-large-integer) as
     an integer larger than every integer mentioned in the finite
     subset.

----------

C. Non-standard reals via an ultrapower construction

   This construction provides some intuition.

   - Consider all functions from the naturals to the reals, with
     a suitable notion of "almost everywhere".
     - The identity function can be taken as (i-large-integer).
     - Then (/ 1 (i-large-integer)) is an infinitesimal (more below).
     - I'll elaborate using a picture as time permits.

----------

D. Superstructures

   We want to make sense of the idea that if f is a function on the
   reals, R, then there is some corresponding, "well-behaved" function
   *f on the hyperreals.

   The foundations are typically not only for the reals R, but for the
   "superstructure" over R, obtained by closing under Powerset (the
   set of all subsets operation):

     V_0(R) = R
     V_{n+1}(R) = V_n(R) U Powerset(V_n(R))
     V(R) = V_0(R) U V_1(R) U V_2(R) U ...

   We assume the existence of a one-one mapping, "*", with domain
   V(R), that has the following properties.

   In particular, since R \in V(R), *R is defined.  (R \in V(R)
   because R \subset R, so R \in V_1(R).)  We call *R the
   "hyperreals".

   Facts: R \subset *R, and moreover, *x = x for x \in R.

   A function f on R is a set of ordered pairs <x,y> = {{x},{x,y}}
   from R.
   {x}, {x,y} \in V_1(R)
   so
   <x,y> \in V_2(R)
   so
   f \in V_3(R).
   Since f \in V(R), there is a *f.

   This may seem horribly abstract at this point!  But the intuition
   is that *f agrees with f on R, but *f also maps all of *R into *R.

====================

III. Non-standard basics

----------

A. Basic notions

   R is the set of "standard reals", which include all those that can
   be defined (e.g. 1, -2, pi, sqrt(3), ...).

   Now let's consider elements x of *R.

   x is i-small (infinitesimal) iff |x|<r for all standard reals r>0.

   x is i-large iff |x|>r for all standard reals r.

   x is i-limited (finite) iff |x|<r for some standard real r.
   - Thus, x is i-limited iff x is not i-large.

   x is i-close to y iff (- x y) is i-small.

   The star function "*" maps elements of V(R) to V(*R).
   - *x = x for all x \in R.
   - R \subset *R
   - *R \= R; elements of the difference *R \ R are "non-standard".

   A key function is standard-part.
   - For x \in R, (standard-part x) = x.
   - For x i-limited, (standard-part x) is the unique real that is
     i-close to x:
       (standard-part x) \in R
     and
       (- x (standard-part x)) is i-small
   - x is i-small iff (standard-part x) = 0.

   ACL2(r) recognizes standard objects with (standardp x).

   An object is "standard" if it is in V(R).
   - The new "nonstandard" functions such as standard-part, standardp,
     and i-small are not standard.
   - We call a function symbol "classical" when it represents a
     standard function.
     - So none of standard-part, standardp, i-small, etc. are
       classical.
   - A term is "classical" iff all its function symbols are
     classical.

   Suppose f is defined by defun.  Then ACL2(r) recognizes f as
   classical when its definition's body is classical.

   Examples:

(defun f (x)
  (* (car x) (cdr x)))
(defun g (x)
  (standard-part x))

  Then:

ACL2(r) !>(classicalp 'f (w state))
T
ACL2(r) !>(classicalp 'g (w state))
NIL
ACL2(r) !>

----------

B. The transfer principle

   Statement of the transfer principle:

     The same classical first-order sentences are true for the reals R
     as for the hyperreals *R (standard+non-standard reals).

   Examples:

     (forall x) (equal (* x x) (* (- x) (- x)))

     ; Twin primes conjecture is either true for both R and *R or
     ; false for both.
     (forall x) (exists y) (and (< x y) (primep y) (primep (+ y 2)))

     ; For a classical binary function f defined by defun:
     (forall x y) (equal (f x y) (f y x))

   ACL2(r) implements the transfer principle with:

   (defthm-std name body) ; optionally, :hints

   - Applies only if the body is classical.

   - Before attempting the proof, ACL2(r) adds a hypothesis
     of (standardp x) for all variables x in the body:
     (implies (and (standardp x1) (standardp x2) ... (standardp xk))
              (... x1 x2 ... xk ...))

----------

C. Defun-std

   1. Syntax is like defun:

      (defun-std f (x1 ... xn)
        <body>)

   2. Proof obligation for the above defun-std form:

      (implies (and (standardp x1) ... (standardp xn))
               (standardp <body>))

      Note that <body> does not need to be classical!

   3. Axiom added for the above defun-std form:

      (implies (and (standardp x1) ... (standardp xn))
               (equal (f x1 ... xn)
                      <body>))

      NOTE THE HYPOTHESES!

   4. Example (worked through in Section IV): Here, think if
      (iter-sqrt x epsilon) as an ordinary, recursively-defined
      function that applies a bisection algorithm to approximate the
      square root of x within epsilon.  So if epsilon is i-small,
      iter-sqrt gives us an i-close approximation -- then we take its
      standard-part.

(defun-std acl2-sqrt (x)
  (standard-part (iter-sqrt (fix x)
                            (/ (i-large-integer)))))

   5. Sketch of soundness of defun-std:

      Let f be the function defined over R by the above definition.
      Then for all standard x1, ..., xn: (f x1 ... xn) = <body>.
      Consider *f and suppose a1, ..., an \in R.
      Let b = f(a1,...,an).
      Then by transfer, also b = *f(a1,...,an).
      We have shown the *f satisfies the axiom in C above.

**NOTE**: the resulting defined function, *f, is classical -- it's the
  * of a standard function f.

====================

IV.  ACL2(r) example

   We will go through the book sqrt-short.lisp.

====================

V. Sketches for cool hand proofs, time permitting

   - Continuity of a sum

     Let f and g be standard.

     Definition:
     f(x) is continuous at a (a standard) if and only if:
     For all a0 i-close to a, f(a0) is i-close to f(a).

     Theorem:  If f and g are continuous at standard a, so is f+g.
     Proof:  for a0 i-close to a, show that
     (f+g)(a0) is i-close to (f+g)(a), as follows.
     (f+g)(a0)       - (f+g)(a) =
     [f(a0) + g(a0)] - [f(a) + g(a)] =
     [f(a0) - f(a)]  + [g(a0) - g(a)],
     which is the sum of two infinitesimals,
     hence is infinitesimal; so (f+g)(a0) is i-close to (f+g)(a).

   - Every bounded sequence has a convergent subsequence.

   - Chain rule

====================

VI. Conclusion

   Non-standard analysis has been found to provide a nice way to do
   proofs for real analysis.

   Its reduced dependence on quantification makes non-standard
   analysis a good match for ACL2, which has resulted in Ruben
   Gamboa's ACL2(r).

   More can be found in the Community Books, in books/nonstd/.
   Also see :doc real.

   In the first ACL2 Workshop (1999), I presented a proof of the
   Fundamental Theorem of Calculus:

   books/nonstd/workshops/1999/calculus/

   Shant Harutunian wrote a Ph.D. dissertation on verifying control
   systems using ACL2(r); see community books
   books/projects/hybrid-systems/.

   But most of the ACL2(r) applications have been done by Ruben Gamboa
   (mostly in books/nonstd/).  A nice early one: Intermediate Value
   Theorem.

   Cuong will present some of his own ACL2(r) work next week.

   Thanks to Ben Selfridge for helpful comments on a preliminary
   version of these notes.

====================

[end]