💻 computer science

Nonlinear Arithmetic with SMTLIB Division is Undecidable

Het artikel toont aan dat niet-lineaire reële rekenkunde (NRA) zoals gedefinieerd in de SMTLIB-standaard onbeslisbaar is, omdat de behandeling van deling door nul als een ongeïnterpreteerde functie het coderen van onbeslisbare problemen uit de geheeltallige rekenkunde mogelijk maakt.

Oorspronkelijke auteurs: Dejan Jovanovic

Gepubliceerd 2026-05-27

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Dejan Jovanovic

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 detective bent die een mysterie probeert op te lossen met behulp van een zeer strikte set regels. In de wereld van de informatica worden deze regels "theorieën" genoemd, en ze helpen computers te beslissen of een wiskundig raadsel een oplossing heeft of niet.

Dit artikel gaat over een specifieke set regels genaamd Nonlinear Real Arithmetic (NRA). Denk hierbij aan een spel dat wordt gespeeld met reële getallen (zoals 3,14, -5 of 0,001), waarbij je ze kunt optellen, aftrekken, vermenigvuldigen en delen.

De "magische" regel die het spel breekt

Lange tijd geloofden wiskundigen dat dit spel perfect oplosbaar was. Als je een computer een raadsel gaf met deze getallen, kon het uiteindelijk zeggen: "Ja, er is een oplossing," of "Nee, er is geen oplossing."

De auteur, Dejan Jovanović, ontdekte echter een verborgen valstrik in het officiële regelboek (de SMTLIB-standaard). De valstrik zit in hoe de regels omgaan met deling door nul.

In de gewone wiskunde is deling door nul een groot "Nee". Maar in dit specifieke computerregelboek staat: "Als je door nul deelt, maakt het niet uit wat het antwoord is. Het kan alles zijn, zolang het zich maar gedraagt als een normaal getal wanneer je niet door nul deelt."

De auteur noemt dit een "ongedefinieerde functie". Om een analogie te gebruiken: stel je een automaat voor die perfect werkt voor elke snack die je koopt. Maar als je probeert een "Nul-snack" te kopen, crasht de machine niet; in plaats daarvan spitst hij gewoon iets uit – misschien een reepje snoep, misschien een steen, misschien een wolk. De regels vertellen je niet wat het zal zijn; ze zeggen alleen: "Het zal iets zijn."

Hoe dit het spel onoplosbaar maakt

Het artikel betoogt dat deze "alles mag" regel voor deling door nul de sleutel is die een deur naar chaos opent.

Hier is de logica, vereenvoudigd:

Het doel: De auteur wil bewijzen dat als je deze "magische" delingsregel hebt, je de computer kunt bedriegen om gehele getallen-raadsels op te lossen (raadsels met hele getallen zoals 1, 2, 3).
Het probleem: Het oplossen van gehele getallen-raadsels is berucht onmogelijk voor computers om perfect te doen voor elk geval (dit staat bekend als Hilbert's Tiende Probleem). Het is als proberen een naald te vinden in een hooiberg die eeuwig blijft groeien.
De truc: De auteur toont aan dat je door gebruik te maken van de "magische" deling door nul een wiskundige brug kunt bouwen. Je kunt een moeilijk gehele getallen-raadsel nemen en vertalen naar een reële getallen-raadsel met behulp van deze delingstruc.
- Analogie: Stel je voor dat je een geheime code hebt geschreven in een taal die alleen mensen begrijpen (gehele getallen). Je bouwt een machine (de delingstruc) die deze code vertaalt naar een taal die computers begrijpen (reële getallen). Omdat de taal van de computer deze "magische" deling-door-nul-regel heeft, kan de computer per ongeluk de menselijke code oplossen.
Het resultaat: Aangezien we weten dat computers niet alle gehele getallen-raadsels kunnen oplossen, en deze truc hen in staat stelt om gehele getallen-raadsels op te lossen met behulp van reële getallen, betekent dit dat de computer ook niet alle reële getallen-raadsels kan oplossen. Het spel wordt onbeslisbaar.

De "vloer"-functie analogie

Om dit te bewijzen, gebruikt de auteur een slimme truc. Ze tonen aan dat als je deze "magische" deling hebt, je de computer kunt dwingen te fungeren als een vloer-functie (een functie die een getal naar beneden afrondt naar het dichtstbijzijnde gehele getal, zoals het omzetten van 3,9 in 3).

Zodra de computer getallen naar beneden kan afronden, kan het beginnen met het tellen van gehele getallen. Zodra het gehele getallen kan tellen, kan het proberen die onmogelijke gehele getallen-raadsels op te lossen. Aangezien die raadsels in het algemeen onoplosbaar zijn, wordt het hele systeem van reële getallen-wiskunde met deze delingsregel in het algemeen onoplosbaar.

Wat dit betekent voor de echte wereld (volgens het artikel)

Het artikel spreekt niet over toekomstige AI of medische toepassingen. Het richt zich op de huidige staat van computer benchmarks (testproblemen):

De valstrik: Veel bestaande testproblemen in de SMTLIB-bibliotheek (een enorme collectie wiskundige raadsels die worden gebruikt om computers te testen) gebruiken deling met variabelen (zoals x / y). Als y toevallig nul is, vallen deze raadsels in de "onbeslisbare" valstrik.
De oplossing? De auteur suggereert twee manieren om het regelboek te fixen:
1. Kies een specifiek antwoord: Beslis dat deling door nul altijd gelijk is aan een specifiek getal (zoals 0 of 1), net zoals sommige computersystemen dit hanteren voor binaire getallen.
2. Splits het spel: Creëer een nieuwe, aparte categorie voor problemen waarbij je deelt door variabelen, en houd de "veilige" categorie voor problemen waarbij je alleen deelt door bekende getallen (constanten).

De bottom line

Het artikel beweert dat een specifieke, ogenschijnlijk onschadelijke regel over hoe computers "deling door nul" hanteren, per ongeluk de mogelijkheid van computers om alle wiskundige problemen met reële getallen op te lossen, ondermijnt. Het verandert een oplosbaar spel in een onoplosbaar spel door de computer in staat te stellen om heimelijk problemen op te lossen die het niet zou moeten kunnen oplossen.

Technische Samenvatting: Niet-lineaire rekenkunde met SMTLIB-divisie is onbeslisbaar

Probleemstelling
Het artikel behandelt de beslisbaarheidsstatus van de theorie van niet-lineaire reële rekenkunde (NRA) zoals formeel gedefinieerd in de SMTLIB-standaard. Hoewel de theorie van gesloten reële velden (bestaande uit gelijkheden en ongelijkheden over polynomen) een goed gevestigd beslisbaar fragment van de wiskundige logica is (Tarski [7]), breidt de SMTLIB-definitie van NRA deze signatuur uit om deling op te nemen. Het kritieke probleem ontstaat door de behandeling van deling door nul. In de SMTLIB-standaard wordt deling geïnterpreteerd zoals verwacht voor niet-nul delers, maar blijft een ongeïnterpreteerde functie wanneer de deler nul is. Specifiek staat het axioma $(\forall x, y \in \mathbb{R}) (y \neq 0) \Rightarrow (x = \frac{x}{y} \cdot y)$ elke waarde toe voor $\frac{x}{0}$ , mits het standaardgedrag elders behouden blijft. Het artikel onderzoekt of deze specifieke behandeling van deling door nul de beslisbaarheid van de theorie behoudt.

Methodologie
De auteur hanteert een reductiebewijs om onbeslisbaarheid aan te tonen. De methodologie verloopt in twee logische stappen:

Reductie vanuit geheeltallige rekenkunde: Het artikel stelt eerst vast dat reële rekenkunde uitgebreid met een enkele unary ongeïnterpreteerde functie onbeslisbaar is. Dit wordt bereikt door de ongeïnterpreteerde functie $f$ $f$ te axiomatiseren zodat deze zich gedraagt als de floor-functie $\lfloor \cdot \rfloor$ $⌊ \cdot ⌋$ met behulp van de axioma's:
- $(\forall x \in \mathbb{R}) f(x) + 1 = f(x + 1)$
- $(\forall x \in \mathbb{R}) (0 \le x < 1) \Rightarrow (f(x) = 0)$
  Door deze axioma's af te dwingen, kan elke formule over geheeltallige variabelen equisatisfiable worden gemaakt met een formule over reële variabelen die $f$ bevat. Aangezien geheeltallige rekenkunde onbeslisbaar is (Hilberts 10e probleem [4]), wordt de uitgebreide theorie van reële rekenkunde onbeslisbaar.
Mapping naar deling door nul: Het artikel mapt vervolgens de ongeïnterpreteerde functie $f$ uit de vorige stap direct naar de deling-door-nul-operatie ( $\frac{x}{0}$ ). Door $\frac{x}{0}$ te behandelen als de ongeïnterpreteerde functie, kunnen de axioma's die nodig zijn om de floor-functie te simuleren, worden gecodeerd binnen de NRA-theorie. Bijgevolg kan de satisfiability van willekeurige geheeltallige formules worden gereduceerd tot de satisfiability van NRA-formules die deling door nul bevatten.

Belangrijkste bijdragen en resultaten

Bewijs van onbeslisbaarheid: Het primaire resultaat is de demonstratie dat de SMTLIB-theorie van niet-lineaire reële rekenkunde (NRA) onbeslisbaar is. Dit is een direct gevolg van het opnemen van deling waarbij de deler een ongeïnterpreteerde functie is bij nul.
Coderingsmechanisme: Het artikel biedt een concrete codering (Voorbeeld 1) die laat zien hoe de satisfiability van Diophantische vergelijkingen (bijvoorbeeld $a^3 + b^3 = c^3$ over gehele getallen) kan worden vertaald naar NRA-formules. Dit gebeurt door te stellen dat variabelen als gehele getallen fungeren via de simulatie van de floor-functie met behulp van $\frac{x}{0}$ , en vervolgens de polynoombeperkingen toe te passen.
Impact op bestaande benchmarks: De analyse onthult dat hoewel veel benchmarks in de SMTLIB-NRA-categorie alleen deling gebruiken met constante delers (een beslisbaar fragment), diegenen die gebruikmaken van niet-constante delers vallen onder het nieuw geïdentificeerde onbeslisbare fragment.

Betekenis en claims
Het artikel beweert dat dit resultaat "onverwacht" is, gezien het feit dat het beslisbare fragment van polynoombeperkingen een mijlpaalresultaat is in de wiskundige logica. De betekenis ligt in het verduidelijken van de theoretische grenzen van de SMTLIB-standaard: het opnemen van deling als een ongeïnterpreteerde functie bij nul verandert fundamenteel het landschap van de beslisbaarheid, waardoor de volledige theorie onbeslisbaar wordt.

De auteur merkt op dat deze beperking de uitbreiding van complete kwantoreneliminatietechnieken (zoals die gebruikt worden in CAD of lazy kwantoreneliminatiebenaderingen [3, 5, 6]) naar de volledige NRA-theorie in aanwezigheid van deling door nul uitsluit.

Voorgestelde mitigaties
Het artikel sluit af met een schets van twee mogelijke benaderingen om deze onbeslisbaarheid aan te pakken, zonder te beweren het probleem binnen de huidige standaard te hebben opgelost:

Totale deling: Het toewijzen van een specifieke waarde aan deling door nul (vergelijkbaar met bitvectortheorie [1]), hoewel dit uitdagingen met zich meebrengt bij het selecteren van een geschikte waarde.
Scheiding van theorieën: Het verplaatsen van deling met niet-constante delers naar een aparte theorie (voorgesteld als UFNRA) en het beperken van NRA tot polynoombeperkingen plus deling door niet-nul constanten. De auteur erkent dat dit een herclassificatie van bestaande benchmarks zou vereisen.