Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

1. Problemstellung und Motivation

Separation Logic (SL) ist ein etabliertes formales Rahmenwerk zur Verifikation von Programmen, die mit dem Heap (Speicher) manipulieren. Während viele Fragmente der Separation Logic entscheidbar sind (z. B. quantorenfreie SL oder SL mit Presburger-Arithmetik unter bestimmten Einschränkungen), stellt sich die Frage nach der Entscheidbarkeit, wenn arithmetische Operationen in die Logik integriert werden.

Die Autoren untersuchen ein minimales Fragment der Separation Logic mit natürlichen Zahlen, bezeichnet als SLN. Dieses Fragment enthält nur:

• Den intuitionistischen „points-to"-Prädikat ($\to$).
• Die Konstante $0$.
• Die Nachfolgerfunktion $s$.
• Boolesche Konnektive und erste Ordnung Quantoren.

Es fehlen dabei die klassischen Trennungsoperatoren wie die trennende Konjunktion ($*$) und der magische Zauberstab ($-\ast$). Die zentrale Forschungsfrage lautet: Ist die Gültigkeitsprüfung (Validity) in diesem extrem schwachen Fragment entscheidbar?

Die Erwartung wäre, dass ein so eingeschränktes Fragment entscheidbar bleibt. Die Autoren widerlegen diese Annahme und zeigen, dass bereits die Kombination von $\to$, $0$ und $s$ ausreicht, um die gesamte Arithmetik der Peano-Arithmetik (PA) für eine bestimmte Klasse von Formeln zu kodieren, was zu Undecidability führt.

2. Methodik und Kernkonzept

Der Kern der Arbeit besteht in der Konstruktion einer Übersetzung (Translation) von Formeln der Peano-Arithmetik (insbesondere $\Pi^0_1$-Formeln) in Formeln des SLN-Fragments.

A. Heap-basierte Kodierung von Operationstabellen

Das innovative Element der Methode ist die Nutzung des Heaps selbst, um Operationstabellen für Addition, Multiplikation und Ungleichung zu speichern. Anstatt arithmetische Symbole direkt zu verwenden, werden diese durch Referenzen auf Einträge im Heap ersetzt.

• Struktur der Einträge: Der Heap speichert Einträge in Form von zusammenhängenden Zellen.
  • Tagging: Die erste Zelle eines Eintrags dient als Tag:
    • $0$: Addition
    • $1$: Multiplikation
    • $2$: Ungleichung ($\le$)
  • Offset: Um Kollisionen mit den Tags zu vermeiden, werden Argumente und Ergebnisse um $3$ verschoben (d.h. $x$ wird als $x+3$ kodiert).
  • Beispiel Addition: Ein Eintrag für $x + y = z$ wird als Sequenz von Zellen kodiert: $[0, x+3, y+3, z+3]$.
• Konsistenzbedingungen ($H$): Die Autoren definieren eine Formel $H$, die sicherstellt, dass der Heap eine konsistente Operationstabelle enthält. $H$ erzwingt induktive Regeln (z.B. $s(x) + y = s(x+y)$) über die Nachfolgerzellen im Heap. Wenn ein Heap die Bedingung $H$ erfüllt, müssen die darin gespeicherten Ergebnisse den arithmetischen Gesetzen entsprechen.

B. Normalform und Translation

Die Übersetzung erfolgt in zwei Schritten:

1. Normalform: Jede beschränkte Formel in PA wird in eine „Normalform" überführt, in der Addition und Multiplikation nur noch in speziellen Existenzquantoren vorkommen (z.B. $\exists(x = t + u)$).
2. SLN-Übersetzung ($(\cdot)^\circ$):
   • Arithmetische Ausdrücke wie $x = y + z$ werden durch Prädikate ersetzt, die auf die Operationstabelle im Heap verweisen (z.B. $Add(y, z, x)$).
   • Quantoren werden so übersetzt, dass sie die Existenz oder Universalität über die in der Tabelle gespeicherten Werte prüfen.
   • Ein wichtiger Trick ist die Behandlung von Fällen, in denen der Heap zu klein ist, um eine bestimmte Operation zu speichern. Da die Gültigkeit in SLN über alle Heaps quantifiziert wird, gilt eine Formel als wahr, wenn sie in einem „großen" Heap (der die volle Tabelle enthält) wahr ist. In kleinen Heaps, die keine Einträge für bestimmte Argumente enthalten, sind die Implikationen der Übersetzung trivialerweise wahr. Dies ermöglicht die Erhaltung der Gültigkeit für $\Pi^0_1$-Formeln.

3. Wichtige Beiträge und Ergebnisse

A. Darstellungssatz (Representation Theorem)

Das Hauptergebnis ist ein Darstellungssatz, der zeigt, dass für jede $\Pi^0_1$-Formel $A$ der Peano-Arithmetik gilt:
$$A \text{ ist gültig in PA} \iff A^\circ \text{ ist gültig in SLN}$$
Dies bedeutet, dass das SLN-Fragment die volle Ausdruckskraft von $\Pi^0_1$-Formeln der Arithmetik besitzt.

B. Undecidability (Unentscheidbarkeit)

Als direkte Konsequenz des Darstellungssatzes folgt, dass das Gültigkeitsproblem für SLN unentscheidbar ist. Da das Halteproblem (und damit die Gültigkeit von $\Pi^0_1$-Formeln in PA) unentscheidbar ist, muss auch die Gültigkeit in SLN unentscheidbar sein.

• Dies ist überraschend, da das Fragment ohne arithmetische Konstanten ($0, s$) entscheidbar ist und auch Fragmente mit trennender Konjunktion ($*$) oft unentscheidbar sind, aber hier wird gezeigt, dass selbst ohne $*$ und mit nur einem Feld ($1$-field) die Undecidability erreicht wird.

C. Grenzen der Übersetzung ($\Sigma^0_1$ vs. $\Pi^0_1$)

Die Autoren zeigen, dass die Übersetzung nicht für $\Sigma^0_1$-Formeln funktioniert. Ein Gegenbeispiel ($\exists x (x + 0 \neq x)$) demonstriert, dass eine in PA falsche Formel in SLN gültig sein kann. Der Grund liegt in der Semantik: In einem kleinen Heap, der keine Einträge für $x$ enthält, ist die Bedingung für die Addition trivialerweise erfüllt, was die Existenz eines „falschen" $x$ in der Übersetzung erlaubt, obwohl es in der Arithmetik nicht existiert.

D. Alternative Unentscheidbarkeitsbeweise

Neben der Kodierung der PA wird ein alternativer Beweis für die Undecidability präsentiert, der auf einer Reduktion aus der endlichen Modelltheorie (Trakhtenbrot-Theorem) basiert. Dabei wird eine endliche Struktur (Menge und Relation) direkt in einen Heap kodiert, um die Gültigkeit von Formeln über endlichen Strukturen zu simulieren.

E. $\Pi^0_1$-Vollständigkeit

Das Paper etabliert, dass das Gültigkeitsproblem für SLN $\Pi^0_1$-vollständig ist.

• Untere Schranke ($\Pi^0_1$-hart): Folgt aus der Reduktion von PA.
• Obere Schranke ($\Pi^0_1$): Wird bewiesen, indem gezeigt wird, dass das Modell-Checking-Problem (Gegeben $\sigma, h, A$, gilt $\sigma, h \models A$?) entscheidbar ist.
  • Die Entscheidbarkeit des Modell-Checkings ergibt sich daraus, dass die Suche nach Werten für Variablen in $\to$-Atomen durch die Größe des Heaps beschränkt werden kann. Variablen, die nicht in $\to$-Atomen vorkommen, unterliegen nur der Nachfolgerarithmetik (ein Fragment der Presburger-Arithmetik), die entscheidbar ist.
  • Da Modell-Checking entscheidbar ist, kann die Gültigkeit (Gültigkeit für alle $\sigma, h$) als $\Pi^0_1$-Formel ausgedrückt werden.

4. Signifikanz und Implikationen

• Theoretische Grenzen: Die Arbeit definiert eine scharfe Grenze für die Ausdruckskraft von Separation Logic. Sie zeigt, dass selbst das schwächste mögliche räumliche Prädikat ($\to$) in Kombination mit minimaler Arithmetik ($0, s$) ausreicht, um komplexe arithmetische Eigenschaften (wie Konsistenz von Logiksystemen oder starke Normalisierung) zu kodieren.
• Verifikation: Für die Softwareverifikation bedeutet dies, dass man sehr vorsichtig sein muss, wenn man arithmetische Constraints in Separation Logic einfügt. Selbst scheinbar harmlose Erweiterungen können die Entscheidbarkeit zerstören.
• Methodischer Beitrag: Die Technik der „Heap-basierten Operationstabellen" ist ein eleganter Weg, um Arithmetik in Logiken ohne native arithmetische Operatoren zu simulieren.

Zusammenfassend beweist das Paper, dass die Trennung zwischen räumlicher Logik und Arithmetik in der Separation Logic nicht so scharf ist wie oft angenommen: Schon eine minimale Integration von Zahlen führt zur vollen Komplexität der Peano-Arithmetik und damit zur Unentscheidbarkeit.