一句话：将 Peano 算术 Π⁰₁ 公式编码到仅含直觉 points-to、0 与后继的分离逻辑片段，证明有效性等价与不可判定。
分离逻辑已成功用于堆操作程序的软件验证，但为验证实际程序需加入数值；然而含数分离逻辑的有效性、可判定性与复杂度尚未被充分研究。本文把 Peano 算术中的 Π⁰₁ 公式翻译到含数分离逻辑的一个极小片段，该片段仅包括直觉主义 points-to 谓词、常量 0 和后继函数。论文证明：Peano 算术公式在标准模型中有效，当且仅当其翻译在该片段的标准解释下有效。作为推论，这一翻译还给出了该片段有效性不可判定的一个视角证明。由于 Π⁰₁ 公式可描述逻辑系统的一致性和计算的不终止性，该结果也表明这些性质可以在如此小的含数分离逻辑片段中讨论。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ItoT26,
title = {Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic},
author = {Sohei Ito and Makoto Tatsuta},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:22)2026}
}