SCIENCE@home

A Decision Procedure for Linear “Big O” Equations

J. Avigad,K. Donnelly

Published 2007 in Journal of automated reasoning

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.

PUBLICATION RECORD

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-17 of 17 references · Page 1 of 1

CITED BY

Showing 1-7 of 7 citing papers · Page 1 of 1