带求和运算符的实数存在理论

为刻画概率推理与 Pearl 因果等级系统中满足问题的计算复杂性, arXiv:2305.09508 [cs.AI] 引入了新型复杂类 succ-$\exists$R。该类可视为基于实数存在理论 (ETR) 的紧凑变体。类似于 $\exists$R，succ-$\exists$R 位于 NEXP 与 EXPSPACE 之间（即 NP 与 PSPACE 的指数版本）。本文的主要贡献有三点: 首先, 我们以非确定性实数 RAM 机器刻画 succ-$\exists$R 类, 并发展了实数 RAM 的结构复杂性理论, 包括翻译定理与层级定理。值得注意的是, 我们证明了 $\exists$R 与 succ-$\exists$R 的不可区分性。其次, 我们考察了二阶逻辑片段和概率独立逻辑的模型检查与满足性问题的复杂性。我们证明了这些问题的多个实例是 succ-$\exists$R 完备的, 其最佳已知的复杂性下界和上界分别为 NEXP-hardness 和 EXPSPACE。最后, 尽管 succ-$\exists$R 依据普通（非紧凑）ETR 实例（增添指数求和并用于索引指数级变量的机制）进行刻画, 本文证明仅增添指数求和对应的类 $\exists$R^{\Sigma} 包含于 PSPACE. 我们推测该包含是严格的, 因为该类等价于将 VNP-oracle 加到多项式时间非确定性实数 RAM 上。相反, 将指数乘积增添到 ETR 上, 则得到 PSPACE。此外, 我们研究了带小模型要求的概率推理满足问题, 并证明该问题是 $\exists$R^{\Sigma} 完备的。