2025/07/01 by Ito, Sohei, Tatsuta, Makoto
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2507.00465
This paper investigates the expressive power of a minimal fragment of separation logic extended with natural numbers. Specifically, it demonstrates that the fragment consisting solely of the intuitionistic points-to predicate, the constant 0, and the successor function is sufficient to encode all Π01 formulas of Peano Arithmetic (PA). The authors construct a translation from PA into this fragment, showing that a Π01 formula is valid in the standard model of arithmetic if and only if its translation is valid in the standard interpretation of the separation logic fragment. This result implies the undecidability of validity in the fragment, despite its syntactic simplicity. The translation leverages a heap-based encoding of arithmetic operations - addition, multiplication, and inequality - using structured memory cells. The paper also explores the boundaries of this encoding, showing that the translation does not preserve validity for Σ01 formulas. Additionally, an alternative undecidability proof is presented via a reduction from finite model theory. Finally, the paper establishes that the validity problem for this fragment is Π01-complete, highlighting its theoretical significance in the landscape of logic and program verification.