[FOM] The unreasonable effectiveness of Nonstandard Analysis

[Grant Olney Passmore]

Hi,

On the topic of numerical meaning of infinitesimals: Let me mention a
technique and software package (z3rcf) that Leo de Moura and I developed
for computing in real closed fields of the form RealClosure(Q(t_1,...,t_k,
eps_1,...,eps_n)), where the t_i's are computable transcendentals and the
eps_i's are infinitesimals (with each eps_{i+1} infinitely smaller than
eps_{i}). The technique forms the basis of a new algorithm we've developed
for exact global nonlinear optimization. Computation over non-Archimedean
real closed fields is crucial to the method.

There's a blog post (including examples using a Python API for z3rcf) here:
https://leodemoura.github.io/blog/2013/02/02/inf-trans.html

A PDF of the paper is here:
http://www.cl.cam.ac.uk/~gp351/infinitesimals.pdf

Title: Computation in Real Closed Infinitesimal and Transcendental
Extensions of the Rationals

Abstract: Recent applications of decision procedures for nonlinear real
arithmetic (the theory of real closed fields, or RCF) have presented a need
for reasoning not only with polynomials but also with transcendental
constants and infinitesimals. In full generality, the algebraic setting for
this reasoning consists of real closed transcendental and infinitesimal
extensions of the rational numbers. We present a library for computing over
these extensions. This library contains many contributions, including a
novel combination of Thom's Lemma and interval arithmetic for representing
roots, and provides all core machinery required for building RCF decision
procedures. We describe the abstract algebraic setting for computing with
such field extensions, present our concrete algorithms and optimizations,
and illustrate the library on a collection of examples.

Best wishes,
Grant

On Sat, Sep 5, 2015 at 12:05 AM Sam Sanders <sasander at cage.ugent.be> wrote:

> Discussing Nonstandard Analysis with Harvey Friedman and Frank Waaldijk, I
> realized
> the following analogy regarding Reverse Mathematics and NSA might be
> helpful.
> This analogy is meant to dispel two commonly held myths about NSA, namely:
>
> i) NSA does not have/provide/yield any numerical meaning.
>
> ii) NSA does not bring much more to the table than short proofs of
> standard theorems (and pays a heavy logical price for that).
>
> Here we go:
>
> Reverse Mathematics (RM) is arguably a successful research program in
> FOM.  Classifying theorems according to “which axioms are needed to prove
> them”
> turns out to yield a very nice and interesting picture (Big Five, the RM
> zoo, robustness,…).  The RM classification can also be viewed as being
> based on computability, i.e.
> one wants to know "how non-computable" are the objects claimed to exist by
> a given theorem (as witnessed by the RM-equivalence class it falls into)?
>
> Two observations come to the fore here:
>
> 1) RM is neutral on whether mathematics should be finitist, computable,
> predicative, etc.  (IDEOLOGY FREE)
>
> 2) RM studies theorems from mathematics, rather than formula classes.
>  (SHIFT TO PRACTICE)
>
> Both aspects of RM have been important for its success, in my opinion.
>
>
> Essentially, I have applied these two aspects (ideology-freeness and
> shift-to-practice) to NSA, which translates to the following:
>
> I) (ideology-freeness of NSA) Yes, infinitesimals have a lot of history,
> and can have properties which apparently even instill fear in, and cause
> nightmares for, some of the more ardent platonists.
>
> In light of these properties, one could easily claim, like Errett Bishop
> and Alain Connes did, that NSA must therefore lack any numerical meaning.
>
> This ideological claim lives quite strongly in the minds of
> mathematicians, CS people, philosophers (especially), etc.
>
> This ideological claim is also COMPLETELY FALSE, as shown below.
>
>
> II) (shift-to-practice in NSA)  All flavors of NSA (ideally) come with a
> conservation result:  The NSA systems prove the same formulas (in the
> original language) as the original systems.
>
> Therefore, why should we do NSA but for some shorter proofs here and
> there?  Is all the overhead (logical and ontological) worth the hassle
> expect in a few specific areas?
>
> This would be the view Paul Halmos expressed concerning NSA.
>
> However, if we shift our attention to *theorems* of *pure* NSA (where
> “pure” means “using only the well-known definitions of nonstandard
> continuity, diff., Riemann int., compactness, …),
> we observe that such theorems “always” have a very specific normal form
> (namely “forall standard x, there is standard y, such that A(x,y)” where A
> is internal, i.e. does not involve the standardness predicate.
>
>
> These two observations lead to the following application, leading to the
> extraction, from NSA, of LOTS of computational content (the technical term
> I have heard on the other side of the pond is “up the wazoo”):
>
> There is a carefully crafted “term extraction" algorithm based on logical
> meta-theorems, among others from the above paper by van den Berg et al
> (APAL 2012).
>
> On input (proofs of) theorems of pure NSA, this term extraction algo will:
>
> a) always yield theorems of usual mathematics, i.e. not involving NSA.
>
> b) yield either theorems of constructive/comp. math, or equivalences from
> RM if the original theorem is non-constructive.  The extracted terms (prim.
> rec., i.e. Goedel’s T) witness the existential quantifiers.
>
>
> The relevant paper for all this is:  http://arxiv.org/abs/1508.07434
>
> The title of the paper is “The unreasonable effectiveness of NSA”, which
> seems apt in light of ii) and II) above.
>
>
> Best,
>
> Sam Sanders
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150905/b8f5a68a/attachment.html>