Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

翻译：分离逻辑在堆操作程序的软件验证中取得了成功。对于数值重要的实际软件验证，需将数值添加到分离逻辑中。然而，含数值的分离逻辑的可判定性、复杂性等有效性性质尚未得到充分研究。本文提出将皮亚诺算术中的Π₀₁公式翻译为含数值的分离逻辑小片段中的公式，该片段仅由直觉主义指向谓词、0和后继函数组成。继而证明：皮亚诺算术中的公式在标准模型中有效，当且仅当其在该片段中的翻译在标准解释下有效。作为推论，本文还给出了该片段有效性不可判定性的透视性证明。由于Π₀₁公式可描述逻辑系统的一致性与计算的不终止性，该结果同时表明，皮亚诺算术中讨论的这些性质亦可在含数值的分离逻辑的该小片段中进行讨论。