Many scientific problems can be phrased as existential formulas over the real numbers. For example: For a fixed parameter a, are there x≥y such that x2+y≤a? Quantifier elimination solves such questions by case distinctions, for example: If a<0, take x=0 and y=a; If a≥0, take y=0 and let x be the square root of a. In general, one has to distinguish between the guards (if a<0) and the answers (take x=0 and y=a). Because the answers should be expressions in the language of real numbers and variables, one can use regular back-substitution to get them. The guards, however, should just involve real numbers, so one has to keep them formal, that is, use virtual back-substitution. (Incidentally, formulas involving higher powers of variables, such as x3, can be reduced by the technique of degree shift, but in section 5, this paper shows how virtual back-substitution incorporates this reduction automatically.)
When the formula involves strict inequalities (x>y) in addition to weak inequalities (x≥y), the guards can involve open intervals, posing a problem for back-substitution. This problem was traditionally handled by introducing infinitesimal numbers. The contribution of this paper is to convert such a nonstandard solution into a standard one that involves only real numbers. The main results are achieved in section 4. Section 6 improves the solutions to solutions involving only rational numbers. The authors implemented their procedure in Redlog.
The use of these techniques is demonstrated by taking examples from a variety of fields--computational geometry, motion planning, biological networks, chemical reaction networks, and electrical networks--and showing how to turn solutions using infinitesimals into solutions using only rational numbers. These examples justify the pun in the paper’s title.
