We study the problem of deciding universal termination of linear and affine loops over the reals in the bit-model of real computation. We show that both problems are as close to decidable as one can expect them to be: there exist sound partial algorithms that halt on all problem instances whose answer is robust under all sufficiently small perturbations. We further show that in each case the set of non-robust problem instances has Lebesgue measure zero.
翻译:我们在实数计算的比特模型下研究判定实数域上线性与仿射循环的全称终止性问题。我们证明这两个问题在可判定性上已接近最优:存在完备的部分算法,能够对所有在足够小扰动下保持鲁棒性的问题实例停机。进一步,我们证明每一类非鲁棒问题实例的勒贝格测度均为零。