分离逻辑中带归纳定义的判定性蕴含的统一

分离逻辑 \cite{IshtiaqOHearn01,Reynolds02} 中的蕴含问题 $\varphi \models \psi$，介于等式（$x \iseq y$ 与 $x \not\iseq y$）、空间（$x \mapsto (y_1,\ldots,y_\rank)$）和谓词（$p(x_1,\ldots,x_n)$）原子的分离合取之间，由有限归纳规则集解释，一般是不可判定的。对归纳定义集的某些限制可导出可判定的蕴含问题类。目前存在两类这样的可判定类，分别基于称为\emph{建立性} \cite{IosifRogalewiczSimacek13,KatelaanMathejaZuleger19,PZ20} 和\emph{受限性} \cite{EIP21a} 的两种限制。两类均被 \cite{PZ20} 与 \cite{EIP21a} 各自的独立证明显示为属于 \twoexptime，且已给出从建立性蕴含问题到受限蕴含问题的多一归约 \cite{EIP21a}。本文通过区分仅分别适用于蕴含式左侧（$\varphi$）与右侧（$\psi$）的条件，严格推广了受限类。我们给出了这一称为\emph{安全性}的广义类到建立性类的多一归约。结合建立性到受限蕴含问题的归约，这一新归约闭合了环路，并表明三类蕴含问题（分别为建立性、受限性与安全性）构成一个单一的、统一的、\twoexptime-完全的类别。