A decision procedure for linear "big O" equations
| dc.creator | Avigad, Jeremy | |
| dc.creator | Donnelly, Kevin | |
| dc.date | 2007-01-10 | |
| dc.date.accessioned | 2026-07-07T07:39:38Z | |
| dc.date.available | 2026-07-07T07:39:38Z | |
| dc.description | 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)| \leq 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. | |
| dc.identifier | https://arxiv.org/abs/cs/0701073 | |
| dc.identifier | http://arxiv.org/abs/cs/0701073 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/121521 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1; I.2.3 | |
| dc.title | A decision procedure for linear "big O" equations | |
| dc.type | text |