💻 computer science

Nonlinear Arithmetic with SMTLIB Division is Undecidable

Il documento dimostra che l'aritmetica reale non lineare (NRA) così come definita nello standard SMTLIB è indecidibile perché il suo trattamento della divisione per zero come funzione non interpretata consente la codifica di problemi di aritmetica intera indecidibili.

Autori originali: Dejan Jovanovic

Pubblicato 2026-05-27

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Dejan Jovanovic

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di essere un detective che cerca di risolvere un mistero utilizzando un insieme di regole molto rigide. Nel mondo dell'informatica, queste regole sono chiamate "teorie" e aiutano i computer a decidere se un puzzle matematico ha una soluzione o meno.

Questo articolo riguarda un insieme specifico di regole chiamato Aritmetica Reale Non Lineare (NRA). Pensala come un gioco giocato con numeri reali (come 3,14, -5 o 0,001) in cui puoi sommarli, sottrarli, moltiplicarli e dividerli.

La regola "magica" che rompe il gioco

Per molto tempo, i matematici hanno creduto che questo gioco fosse perfettamente risolvibile. Se si forniva a un computer un puzzle utilizzando questi numeri, questo poteva infine dire: "Sì, c'è una soluzione" oppure "No, non c'è".

Tuttavia, l'autore, Dejan Jovanović, ha scoperto una trappola nascosta nel regolamento ufficiale (lo standard SMTLIB). La trappola risiede nel modo in cui le regole gestiscono la divisione per zero.

Nella matematica normale, dividere per zero è un grande "No". Ma in questo specifico regolamento informatico, le regole dicono: "Se dividi per zero, non ci importa quale sia la risposta. Può essere qualsiasi cosa, purché si comporti come un numero normale quando non stai dividendo per zero."

L'autore definisce questo una "funzione non interpretata". Per usare un'analogia: immagina un distributore automatico che funziona perfettamente per ogni snack che acquisti. Ma se provi a comprare uno "Zero Snack", la macchina non si blocca; invece, sputa semplicemente qualcosa – forse una barretta di cioccolato, forse un sasso, forse una nuvola. Le regole non ti dicono cosa sarà; dicono solo: "Sarà qualcosa."

Come questo rende il gioco irrisolvibile

L'articolo sostiene che questa regola "tutto è concesso" per la divisione per zero è la chiave che apre una porta al caos.

Ecco la logica, semplificata:

L'obiettivo: L'autore vuole dimostrare che se hai questa regola "magica" di divisione, puoi ingannare il computer per risolvere puzzle interi (puzzle con numeri interi come 1, 2, 3).
Il problema: Risolvere puzzle interi è notoriamente impossibile per i computer da fare perfettamente per ogni caso (questo è noto come il Decimo Problema di Hilbert). È come cercare un ago in un pagliaio che continua a crescere per sempre.
Il trucco: L'autore mostra che usando la "magica" divisione per zero, puoi costruire un ponte matematico. Puoi prendere un difficile puzzle intero e tradurlo in un puzzle di numeri reali usando questo trucco di divisione.
- Analogia: Immagina di avere un codice segreto scritto in una lingua che solo gli umani capiscono (interi). Costruisci una macchina (il trucco di divisione) che traduce questo codice in una lingua che i computer capiscono (numeri reali). Poiché la lingua del computer ha questa regola "magica" di divisione per zero, il computer può accidentalmente risolvere il codice umano.
Il risultato: Poiché sappiamo che i computer non possono risolvere tutti i puzzle interi, e questo trucco permette loro di provare a risolvere puzzle interi usando numeri reali, significa che il computer non può risolvere tutti i puzzle di numeri reali nemmeno. Il gioco diventa indecidibile.

L'analogia della funzione "Floor"

Per dimostrarlo, l'autore usa un trucco intelligente. Mostra che se hai questa "magica" divisione, puoi costringere il computer ad agire come una funzione floor (una funzione che arrotonda un numero verso il basso al numero intero più vicino, come trasformare 3,9 in 3).

Una volta che il computer può arrotondare i numeri verso il basso, può iniziare a contare gli interi. Una volta che può contare gli interi, può provare a risolvere quei puzzle interi impossibili. Poiché quei puzzle sono impossibili da risolvere in generale, l'intero sistema di matematica dei numeri reali con questa regola di divisione diventa impossibile da risolvere in generale.

Cosa significa questo per il mondo reale (secondo l'articolo)

L'articolo non parla di intelligenza artificiale futura o usi medici. Si concentra sullo stato attuale dei benchmark informatici (problemi di test):

La trappola: Molti problemi di test esistenti nella libreria SMTLIB (un'enorme raccolta di puzzle matematici usati per testare i computer) usano la divisione con variabili (come x / y). Se y risulta essere zero, questi puzzle cadono nella trappola "indecidibile".
La soluzione? L'autore suggerisce due modi per correggere il regolamento:
1. Scegli una risposta specifica: Decidi che dividere per zero sempre uguale a un numero specifico (come 0 o 1), proprio come alcuni sistemi informatici lo gestiscono per i numeri binari.
2. Dividi il gioco: Crea una nuova categoria separata per i problemi in cui si divide per variabili, e mantieni la categoria "sicura" per i problemi in cui si divide solo per numeri noti (costanti).

La conclusione

L'articolo afferma che una regola specifica, apparentemente innocua su come i computer gestiscono la "divisione per zero", rompe accidentalmente la capacità dei computer di risolvere tutti i problemi matematici che coinvolgono numeri reali. Trasforma un gioco risolvibile in uno irrisolvibile permettendo al computer di risolvere furtivamente problemi che non avrebbe dovuto essere in grado di risolvere.

Riepilogo Tecnico: L'aritmetica non lineare con la divisione SMTLIB è indecidibile

Enunciato del Problema
Il lavoro affronta lo stato di decidibilità della teoria dell'Aritmetica Reale Non Lineare (NRA) così come definita formalmente nello standard SMTLIB. Mentre la teoria dei campi reali chiusi (comprendente uguaglianze e disuguaglianze su polinomi) è un frammento ben consolidato della logica matematica decidibile (Tarski [7]), la definizione SMTLIB della NRA estende questa firma includendo la divisione. La questione critica deriva dal trattamento della divisione per zero. Nello standard SMTLIB, la divisione è interpretata come previsto per divisori non nulli, ma rimane una funzione non interpretata quando il divisore è zero. Nello specifico, l'assioma $(\forall x, y \in \mathbb{R}) (y \neq 0) \Rightarrow (x = \frac{x}{y} \cdot y)$ consente qualsiasi valore per $\frac{x}{0}$ , purché il comportamento standard sia mantenuto altrove. Il lavoro indaga se questo specifico trattamento della divisione per zero preservi la decidibilità della teoria.

Metodologia
L'autore impiega una prova per riduzione per dimostrare l'indecidibilità. La metodologia procede in due passaggi logici:

Riduzione dall'Aritmetica Intera: Il lavoro stabilisce inizialmente che l'aritmetica reale arricchita con una singola funzione unaria non interpretata è indecidibile. Ciò è ottenuto assiomaticizzando la funzione non interpretata $f$ $f$ affinché si comporti come la funzione parte intera $\lfloor \cdot \rfloor$ $⌊ \cdot ⌋$ utilizzando gli assiomi:
- $(\forall x \in \mathbb{R}) f(x) + 1 = f(x + 1)$
- $(\forall x \in \mathbb{R}) (0 \le x < 1) \Rightarrow (f(x) = 0)$
  Imponendo questi assiomi, qualsiasi formula su variabili intere può essere equisoddisfacibile con una formula su variabili reali che coinvolge $f$ . Poiché l'aritmetica intera è indecidibile (decimo problema di Hilbert [4]), la teoria dell'aritmetica reale estesa diventa indecidibile.
Mappatura sulla Divisione per Zero: Il lavoro mappa quindi la funzione non interpretata $f$ dal passaggio precedente direttamente sull'operazione di divisione per zero ( $\frac{x}{0}$ ). Trattando $\frac{x}{0}$ come funzione non interpretata, gli assiomi necessari per simulare la funzione parte intera possono essere codificati all'interno della teoria NRA. Di conseguenza, la soddisfacibilità di formule intere arbitrarie può essere ridotta alla soddisfacibilità di formule NRA che coinvolgono la divisione per zero.

Contributi e Risultati Chiave

Prova di Indecidibilità: Il risultato principale è la dimostrazione che la teoria SMTLIB dell'Aritmetica Reale Non Lineare (NRA) è indecidibile. Questo è una diretta conseguenza dell'inclusione della divisione dove il divisore è una funzione non interpretata allo zero.
Meccanismo di Codifica: Il lavoro fornisce una codifica concreta (Esempio 1) che mostra come tradurre la soddisfacibilità di equazioni diofantee (ad esempio, $a^3 + b^3 = c^3$ sugli interi) in formule NRA. Ciò è fatto asserendo che le variabili agiscano come interi attraverso la simulazione della funzione parte intera utilizzando $\frac{x}{0}$ , e applicando quindi i vincoli polinomiali.
Impatto sui Benchmark Esistenti: L'analisi rivela che, mentre molti benchmark nella categoria NRA di SMTLIB utilizzano la divisione solo con divisori costanti (un frammento decidibile), quelli che utilizzano divisori non costanti rientrano nel nuovo frammento indecidibile identificato.

Significato e Affermazioni
Il lavoro afferma che questo risultato è "inaspettato" dato che il frammento decidibile dei vincoli polinomiali è un risultato fondamentale nella logica matematica. Il significato risiede nel chiarire i confini teorici dello standard SMTLIB: l'inclusione della divisione come funzione non interpretata allo zero altera fondamentalmente il panorama della decidibilità, rendendo indecidibile l'intera teoria.

L'autore nota che questa limitazione preclude l'estensione delle tecniche complete di eliminazione dei quantificatori (come quelle utilizzate nel CAD o negli approcci di eliminazione dei quantificatori lazy [3, 5, 6]) all'intera teoria NRA in presenza di divisione per zero.

Mitigazioni Proposte
Il lavoro conclude delineando due approcci potenziali per affrontare questa indecidibilità, senza affermare di aver risolto il problema all'interno dello standard corrente:

Divisione Totale: Assegnare un valore specifico alla divisione per zero (simile alla teoria dei bitvettori [1]), sebbene ciò presenti sfide nella selezione di un valore appropriato.
Separazione della Teoria: Spostare la divisione con divisori non costanti in una teoria separata (proposta come UFNRA) e limitare la NRA ai vincoli polinomiali più la divisione per costanti non nulle. L'autore riconosce che ciò richiederebbe la riclassificazione dei benchmark esistenti.