Journal of Automated Reasoning

, Volume 38, Issue 4, pp 353–373

# A Decision Procedure for Linear “Big O” Equations

Article

## Abstract

Let F be the set of functions from an infinite set, S, to an ordered ring, R. For f, g, and h in F, the assertion f = g + O(h) means that for some constant C, |f(x) − g(x)| ≤C |h(x)| for every x in S. Let L be the first-order language with variables ranging over such functions, symbols for 0, +, −, min , max , and absolute value, and a ternary relation f = g + O(h). We show that the set of quantifier-free formulas in this language that are valid in the intended class of interpretations is decidable and does not depend on the underlying set, S, or the ordered ring, R. If R is a subfield of the real numbers, we can add a constant 1 function, as well as multiplication by constants from any computable subfield. We obtain further decidability results for certain situations in which one adds symbols denoting the elements of a fixed sequence of functions of strictly increasing rates of growth.

## Keywords

Decision procedures Asymptotic equations Big O

## Preview

Unable to display preview. Download preview PDF.

## References

1. 1.
Apt, K.: Principles of Constraint Programming. Cambridge University Press, Cambridge (2003)Google Scholar
2. 2.
Avigad, J., Donnelly, K.: Formalizing O notation in Isabelle/HOL. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning: Second International Joint Conference, IJCAR 2004, pp. 357–371. Springer, Berlin Heidelberg New York (2004)Google Scholar
3. 3.
Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem (to appear in ACM Transactions on Computational Logic)Google Scholar
4. 4.
Avigad, J., Friedman, H.: Combining decision procedures for the reals. Logical Methods in Computer Science 2(4:4), 1–42 (2006)
5. 5.
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’art: The Calculus of Inductive Constructions. Springer, Berlin Heidelberg New York (2004)
6. 6.
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-order Logic. Cambridge University Press, Cambridge (1993)
7. 7.
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics: A Foundation for Computer Science, 2nd ed. Addison-Wesley, Reading, MA (1994)
8. 8.
Hall Jr., M.: Combinatorial Theory, 2nd ed. Wiley, New York (1986)
9. 9.
Karmarkar, N.: A new polynomial time algorithm for linear programming. Combinatorica 4, 373–395 (1984)
10. 10.
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-aided Reasoning: An Approach. Kluwer, Boston (2000)Google Scholar
11. 11.
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal 36, 450–461 (1993)
12. 12.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer, Berlin Heidelberg New York (2002)
13. 13.
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Proceedings of the 11th International Conference on Automated Ceduction (CADE), pp. 748–752. Springer, Berlin Heidelberg New York (1992)Google Scholar
14. 14.
Papadimitriou, C.H., Steiglitz, K.: Combinatorial Optimization: Algorithms and Complexity. Dover, Mineola, NY (1998) (Corrected reprint of the 1982 original, Prentice-Hall, New Jersey)
15. 15.
Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5, 3–27 (1988)
16. 16.
Weispfenning, V.: Parametric linear and quadratic optimization by elimination. Technical report MIP-9404, Universität Passau (1994)Google Scholar