💻 computer science

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Dit artikel bewijst dat de validiteit van Π₀¹-formules in Peano-aritmetiek equivalent is aan die in een minimaal fragment van scheidinglogica met getallen, wat de onbeslisbaarheid van laatstgenoemde bevestigt en aantoont dat fundamentele eigenschappen zoals consistentie en niet-terminatie ook binnen dit beperkte kader kunnen worden onderzocht.

Oorspronkelijke auteurs: Sohei Ito, Makoto Tatsuta

Gepubliceerd 2026-03-20

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Sohei Ito, Makoto Tatsuta

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een taal hebt die is ontworpen om te vertellen hoe een computer zijn geheugen gebruikt. Deze taal heet Scheidinglogica (Separation Logic). Het is als een heel slimme, precieze instructiehandleiding voor een robot die moet weten: "Hier ligt een doosje met een nummer, en daar ligt een andere doos."

Normaal gesproken is deze taal heel goed te begrijpen en makkelijk voor computers om te checken of de instructies kloppen. Maar wat gebeurt er als we deze taal een klein beetje uitbreiden? Wat als we er een paar simpele wiskundige regels aan toevoegen, zoals "dit is nul" en "dit is het volgende getal"?

Dat is precies wat dit paper onderzoekt. De auteurs, Sohei Ito en Makoto Tatsuta, hebben ontdekt dat je met maar heel weinig extra wiskunde al een heel gevaarlijk, onoplosbaar probleem creëert.

Hier is de uitleg in simpele taal, met een paar analogieën:

1. De Simpele Taal (Het Startpunt)

Stel je hebt een taal die alleen kan zeggen: "Op adres 1 ligt een doos met nummer 5."

Symbool: 1 → 5 (Lees: "Adres 1 wijst naar 5").
Als je alleen dit gebruikt, is het voor een computer heel makkelijk om te checken of zinnen kloppen. Het is als een simpel raadsel dat altijd opgelost kan worden.

2. De Magische Toevoeging (De Wiskunde)

De auteurs zeggen: "Laten we twee dingen toevoegen:

Het getal 0.
De opvolger-functie (dat is gewoon 'plus 1').

Dus nu kunnen we zeggen: "Dit is 0, en dit is het getal dat 1 groter is dan 0."
Je zou denken: "Oh, dat is toch niet zo moeilijk? Dat is gewoon tellen."

3. De "Geheime Code" (De Oplossing)

Hier wordt het spannend. De auteurs hebben een slimme truc bedacht. Ze gebruiken het computergeheugen (de "heap") als een gigantische naslagtafel.

Stel je voor dat je een heel groot bord hebt met vakjes.

Als je wilt weten wat 2 + 3 is, kijkt de computer niet in zijn hoofd, maar zoekt hij in het geheugen naar een rijtje vakjes die er zo uitziet: [0, 2, 3, 5].
- Het eerste getal (0) zegt: "Dit is een optel-rijtje."
- De volgende twee (2 en 3) zijn de getallen die we optellen.
- Het laatste getal (5) is het antwoord.

Op dezelfde manier maken ze rijtjes voor vermenigvuldigen en kleiner/groter dan.

[1, 2, 3, 6] betekent: "Dit is een vermenigvuldig-rijtje. 2 keer 3 is 6."
[2, 2, 3] betekent: "Dit is een 'kleiner dan'-rijtje. 2 is inderdaad kleiner dan 3."

4. Het Grote Geheim (Waarom is dit belangrijk?)

Het paper laat zien dat je met deze simpele "naslagtafel" in het geheugen alle wiskundige problemen kunt nabootsen die je in de standaard rekenkunde (Peano Arithmetic) kunt stellen.

Zelfs de allerzwaarste wiskundige problemen, zoals: "Is het mogelijk dat een computerprogramma oneindig blijft draaien?" of "Klopt dit hele wiskundige systeem?"

De conclusie is schokkend simpel:
Als je deze simpele taal (Scheidinglogica + 0 + 1) gebruikt, wordt het voor een computer onmogelijk om altijd te zeggen of een zin waar of onwaar is.

Vroeger: "Klopt deze zin?" -> Computer denkt even -> "Ja, dat is waar." (Oplosbaar).
Nu: "Klopt deze zin?" -> Computer denkt, denkt, denkt... en stopt nooit. (Onoplosbaar).

5. De Analogie van de "Onoplosbare Puzzel"

Stel je voor dat je een puzzel hebt met blokken.

Als je alleen blokken mag gebruiken die "A" en "B" heten, kun je elke puzzel oplossen.
Maar als je mag zeggen: "Dit blok is '0', en dit blok is 'de volgende'", dan kun je ineens een puzzel bouwen die precies zo complex is als het probleem van het Halting Problem (het probleem van of een computerprogramma ooit stopt).

Omdat niemand in de wereld een algoritme heeft dat voor elk computerprogramma kan zeggen of het stopt, kan niemand ook een algoritme hebben dat voor elke zin in deze nieuwe taal kan zeggen of die waar is.

6. Wat betekent dit voor de wereld?

Dit paper is een waarschuwing voor software-ontwikkelaars en wiskundigen.

Vroeger dachten we: "Als we alleen heel simpele wiskunde toevoegen aan onze verificatietools, blijft het veilig en oplosbaar."
Nu weten we: "Zelfs met de allerminste wiskunde (alleen 0 en 'plus 1') wordt het systeem al te complex om volledig te controleren."

Het is alsof je dacht dat je een huis veilig kon houden met alleen een simpele slot. Maar je ontdekt dat als je er maar één extra sleutelgat bijzet, de hele deur ineens open kan worden gemaakt door een onzichtbare, onoplosbare code.

Samenvatting in één zin

De auteurs bewijzen dat zelfs de aller-eenvoudigste vorm van "computergeheugen-taal" met een klein beetje tellen, al zo krachtig is dat hij alle zware wiskundige mysteries kan bevatten, waardoor het voor computers onmogelijk wordt om te weten of alles klopt.

Probleemstelling

Separation Logic (SL) is een krachtig formalisme voor het verifiëren van programma's die geheugenmanipulatie uitvoeren. Traditioneel wordt SL uitgebreid met arithmetische theorieën (zoals Presburger-arithmetiek) om numerieke berekeningen te kunnen verifiëren. Een centrale vraag in dit domein is de beslisbaarheid van de geldigheid (validity) van formules onder standaardinterpretaties.

Over het algemeen wordt aangenomen dat het combineren van een decidable fragment van Separation Logic met een decidable arithmetische theorie (zoals Presburger) leidt tot een decidable systeem. Dit artikel daagt deze veronderstelling uit. De auteurs onderzoeken een minimaal fragment van Separation Logic, genaamd SLN, dat slechts de volgende elementen bevat:

Het intuïtionistische "points-to" predikaat ( $\to$ ).
De constante $0$.
De opvolgerfunctie $s$ (waarbij $s(x) = x + 1$ ).

Het probleem is of dit uiterst beperkte fragment, dat geen gescheiden conjunctie ( $*$ ) of magische wand ( $-\ast$ ) bevat en geen volledige arithmetische operatoren (zoals optellen of vermenigvuldigen) als primitieven heeft, toch voldoende expressief is om complexe rekenkundige problemen te simuleren, en of dit leidt tot onbeslisbaarheid.

Methodologie

De auteurs ontwikkelen een vertalingstransformatie van formules uit de Peano Arithmetic (PA), specifiek de klasse van $\Pi^0_1$ -formules, naar formules in het SLN-fragment. De kern van hun methode is het coderen van arithmetische operaties (optellen, vermenigvuldigen en ongelijkheid) binnen de structuur van de heap (het geheugen).

Heap-gebaseerde Operationstabellen:
In plaats van arithmetische operatoren direct te gebruiken, construeren de auteurs een "operationstabel" in het geheugen. Een heap wordt gezien als een eindige functie $h: \mathbb{N} \to_{fin} \mathbb{N}$ .
- Tags: De auteurs gebruiken de waarden $0$, $1$ en $2$ als tags om het type operatie te onderscheiden:
  - $0$: Optelling ( $+$ )
  - $1$: Vermenigvuldiging ( $\times$ )
  - $2$: Ongelijkheid ( $\leq$ )
- Offset: Argumenten en resultaten worden gecodeerd met een offset van $3$ (bijv. $x+3$ ) om botsingen met de tags te voorkomen.
- Structuur: Een vermelding voor optelling ziet er bijvoorbeeld uit als een opeenvolging van geheugencellen: $[0, x+3, y+3, x+y+3]$ .
De Formule $H$ (Table Heap Condition):
De auteurs definiëren een formule $H$ die eist dat de heap consistent is met de inductieve definities van optelling en vermenigvuldiging.
- $H$ forceert dat als er een entry is voor $x + y = z$ , dan moet de volgende entry (voor $s(x) + y$ ) de waarde $s(z)$ bevatten.
- Dit zorgt ervoor dat de heap fungeert als een geldige rekenmachine voor de gedefinieerde operaties, zolang de heap groot genoeg is om de benodigde invoerwaarden te bevatten.
Vertalingstransformatie:
Een PA-formule wordt vertaald naar een SLN-formule door:
- Arithmetische termen ( $x+y$ , $x \times y$ ) te vervangen door predikaten die verwijzen naar de operationstabel in de heap (bijv. Add(x, y, z)).
- Kwantoren en logische connectieven behouden, maar de semantiek aanpassen zodat de geldigheid afhangt van de aanwezigheid van de juiste tabellen in de heap.
- Specifiek voor $\Pi^0_1$ -formules (van de vorm $\forall x. B$ ) wordt bewezen dat de geldigheid in PA equivalent is aan de geldigheid in SLN onder standaardinterpretatie.
Behoud van Validiteit:
Het bewijs maakt gebruik van het concept van een "simple table heap" ( $h_n$ ), een heap die operationstabellen bevat voor alle getallen tot een bepaalde grootte $n$ . De auteurs tonen aan dat als een formule waar is in de standaardmodellen van PA, deze ook waar is in SLN voor alle heaps (inclusief die met volledige tabellen), en vice versa.

Belangrijkste Bijdragen en Resultaten

Expressiviteit van een Minimaal Fragment:
Het artikel bewijst dat het fragment SLN, dat slechts bestaat uit $\to$ , $0$ en $s$ , voldoende krachtig is om alle $\Pi^0_1$ -formules van Peano Arithmetic te simuleren. Dit is verrassend omdat het fragment geen gescheiden conjunctie bevat en de arithmetiek slechts via de heap-structuur wordt "gehackt".
Onbeslisbaarheid van Validiteit:
Als directe consequentie van de vertaling van PA naar SLN, concluderen de auteurs dat het validiteitsprobleem voor SLN onbeslisbaar is. Omdat het halting-probleem (of het geldigheidsprobleem van PA) onbeslisbaar is, en dit kan worden gereduceerd tot de validiteit in SLN, kan er geen algoritme bestaan dat voor elke SLN-formule bepaalt of deze geldig is.
$\Pi^0_1$ -completheid:
De auteurs tonen aan dat het validiteitsprobleem voor SLN $\Pi^0_1$ -compleet is.
- Ondergrens ( $\Pi^0_1$ -hard): Bewezen via de vertaling van PA.
- Bovengrens ( $\Pi^0_1$ ): Bewezen door te tonen dat het model-checking probleem (gegeven een heap en een formule, is de formule waar?) beslisbaar is. Omdat de zoekruimte voor variabelen in de "points-to" predikaten beperkt kan worden tot de grootte van de heap, en de overige logica valt onder de beslisbare successor-arithmetiek, kan geldigheid worden uitgedrukt als een $\Pi^0_1$ -formule (voor alle $\sigma$ en $h$ geldt $A$ ).
Beperkingen van de Vertaling:
De auteurs tonen aan dat deze vertaling niet werkt voor $\Sigma^0_1$ -formules (existential quantificatie). Voor een $\Sigma^0_1$ -formule kan een heap die "te klein" is (geen volledige tabel bevat) de vertaling onterecht waar maken, omdat de premissen van de implicaties in de vertaling dan niet worden geactiveerd. Dit illustreert een fundamenteel verschil in expressiviteit tussen $\Pi^0_1$ en $\Sigma^0_1$ in dit specifieke fragment.
Alternatief Bewijs:
Er wordt een tweede, alternatief bewijs voor onbeslisbaarheid gegeven via een reductie vanuit de finite model theory (Trakhtenbrot's theorema), wat de robuustheid van het resultaat onderstreept.

Significantie

De resultaten van dit artikel hebben aanzienlijke theoretische implicaties voor de logica en programma-verificatie:

Grenzen van Beslisbaarheid: Het weerlegt de intuïtie dat het toevoegen van eenvoudige arithmetische elementen ( $0, s$ ) aan een zwak spatial fragment (alleen $\to$ ) noodzakelijkerwijs tot een decidable systeem leidt. Zelfs zonder gescheiden conjunctie ( $*$ ) is het systeem onbeslisbaar.
Expressiviteit van Separation Logic: Het toont aan dat Separation Logic, zelfs in zijn meest beperkte vorm, diep ingebedde rekenkundige redeneringen kan bevatten. Dit heeft gevolgen voor het ontwerp van verificatietools: het toevoegen van zelfs minimale arithmetische ondersteuning kan de beslisbaarheid volledig vernietigen.
Theoretische Inzicht: De paper verrijkt het landschap van de logica door de precieze complexiteit ( $\Pi^0_1$ -compleet) van een fragment te bepalen dat eerder als triviaal of decidable zou kunnen worden beschouwd. Het biedt een nieuwe kijk op hoe geheugenstructuren (heaps) kunnen worden gebruikt om rekenkundige structuren te coderen zonder expliciete rekenoperatoren in de logica zelf.

Kortom, het artikel demonstreert dat de combinatie van een minimale spatial logica met standaard arithmetische interpretaties voldoende kracht heeft om de volledige onbeslisbaarheid van de Peano Arithmetic te simuleren, wat een fundamentele grens markeert in de theorie van programma-verificatie.