线性"大O"方程的决策过程
摘要：函数集合$F$由一个无穷集$S$到一个有序环$R$的函数组成。对于$F$中的函数$f$，$g$和$h$，断言$f = g + O(h)$表示存在常数$C$，使得对于$S$中的每个$x$，$|f(x) - g(x)| \leq C |h(x)|$成立。令$L$为一阶语言，变量范围包括这些函数，含有0、+、-、min、max的符号，以及一个三元关系$f = g + O(h)$。我们证明，在这个语言中，对于这些解释的量词无公式的集合是可判定的，且不依赖于底层集合$S$或有序环$R$。如果$R$是实数的一个子域，我们可以添加一个常数1函数，以及乘以任何可计算子域的常数。对于一些加入了表示严格增长速率的固定函数序列的符号的情况，我们还获得了进一步的可判定性结果。
作者：Jeremy Avigad and Kevin Donnelly
论文ID：cs/0701073
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23