💻 computer science

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

Questo articolo presenta una dimostrazione costruttiva del teorema di Rice e del problema della fermata basata sull'indeducibilità del decimo problema di Hilbert, evitando l'uso della legge del terzo escluso, della diagonalizzazione e dell'autoriferimento attraverso una costruzione a due testimoni che collega le proprietà semantiche dei programmi alla risolubilità diofantea.

Autori originali: Jonathan Brossard

Pubblicato 2026-04-21

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Jonathan Brossard

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 avere una scatola magica (un computer) che può eseguire qualsiasi programma. La domanda fondamentale è: possiamo creare un "controllore" che, guardando un programma, ci dica sempre se quel programma ha una certa proprietà specifica?

Ad esempio: "Questo programma si fermerà mai?" oppure "Questo programma calcolerà sempre un numero pari?".

1. Il Problema: Il "Controllore Impossibile"

Per decenni, i matematici hanno saputo che la risposta è NO. Esiste un teorema (il Teorema di Rice) che dice: non esiste un algoritmo universale che possa decidere se un programma ha una proprietà "non banale" (cioè una proprietà che non è vera per tutti i programmi e falsa per tutti).

I vecchi modi per dimostrarlo erano come dei trucchi di magia oscura:

Costruivano un programma che si guardava allo specchio (autoriferimento).
Dicevano: "Se il programma si ferma, allora non si ferma; se non si ferma, allora si ferma".
Usavano la logica classica (il "Principio del Terzo Escluso"), che in termini semplici significa dire: "O succede A, o succede B, non c'è una terza opzione". Questo funziona nella logica classica, ma non in quella "costruttiva" (dove devi costruire la prova, non solo dire che esiste).

2. La Nuova Idea: La "Sfida Matematica" (Hilbert)

Jonathan Brossard, l'autore di questo articolo, ha detto: "E se smettessimo di farci i conti con i programmi che si guardano allo specchio e usassimo invece un vecchio problema matematico?"

Il problema scelto è il Decimo Problema di Hilbert.
Immagina di avere un'equazione matematica fatta solo di numeri interi (un polinomio di Diophante).

Domanda: Esiste una combinazione di numeri interi che rende l'equazione uguale a zero?
La scoperta: È stato dimostrato che non esiste un metodo meccanico per rispondere a questa domanda per qualsiasi equazione. È impossibile.

3. Il Trucco: I "Gemelli Specchio"

L'idea geniale di Brossard è costruire due programmi "gemelli" per ogni equazione matematica che vuoi testare. Chiamiamoli Programma Rosso e Programma Blu.

Ecco come funzionano:

Se l'equazione ha una soluzione:
- Il Programma Rosso inizia a comportarsi come un programma che non si ferma mai (diventa un loop infinito).
- Il Programma Blu inizia a comportarsi come un programma che si ferma subito (termina).
- Risultato: Sono diversi! Uno si ferma, l'altro no.
Se l'equazione NON ha una soluzione:
- Entrambi i programmi cercano la soluzione, non la trovano mai e... entrambi si comportano esattamente allo stesso modo: non si fermano mai.
- Risultato: Sono identici. Non c'è modo di distinguerli.

4. La Trappola per il "Controllore"

Ora, immagina di avere un ipotetico "Controllore Magico" (il decider) che dovrebbe dirti se un programma ha una certa proprietà (es. "si ferma?").

Se dai al Controllore il Programma Rosso e il Programma Blu:
- Se l'equazione ha una soluzione, il Controllore dirà: "Uno sì, l'altro no" (perché sono diversi).
- Se l'equazione non ha una soluzione, il Controllore dirà: "Entrambi sono uguali" (perché sono identici).

Il colpo di scena:
Se il Controllore funzionasse davvero, potremmo usarlo per risolvere il Decimo Problema di Hilbert!

Chiediamo al Controllore di analizzare i due programmi.
Se ci dice che sono diversi, sappiamo che l'equazione ha una soluzione.
Se ci dice che sono uguali, sappiamo che non ha soluzione.

Ma sappiamo già che è impossibile risolvere il Decimo Problema di Hilbert con un algoritmo. Quindi, il nostro "Controllore Magico" non può esistere.

5. Perché è importante? (La parte "Costruttiva")

La differenza fondamentale con i vecchi metodi è che questo nuovo approccio:

Non usa il "Terzo Escluso": Non dice "o l'equazione ha soluzione o non ne ha". Costruisce una macchina che se ha soluzione fa una cosa, se non ne ha ne fa un'altra, senza mai dover decidere a priori quale dei due casi sia vero.
Non usa l'autoriferimento: Non crea programmi che si guardano allo specchio. Usa solo due programmi che "aspettano" una soluzione matematica.
È più "pulito": È come se invece di costruire un labirinto che si chiude su se stesso, avessimo costruito un ponte che collega due isole. Se il ponte crolla, sappiamo che l'isola di partenza non esiste.

In Sintesi

L'autore ha dimostrato che è impossibile creare un programma che decida le proprietà degli altri programmi, non usando i soliti trucchi logici complessi, ma collegando direttamente il problema alla matematica pura (le equazioni di Diophante).

È come dire: "Non puoi costruire un oracolo che ti dica se un programma si ferma, perché se potessi farlo, potresti anche risolvere un problema matematico che sappiamo essere irrisolvibile. Quindi, l'oracolo non può esistere."

E il bello è che questa dimostrazione è valida anche per chi crede che la logica debba essere costruita pezzo per pezzo (logica intuizionista), senza salti di fede logici. È una prova solida, costruita con i mattoni della matematica, non con la magia della logica classica.

1. Il Problema

Il teorema di Rice afferma che nessuna proprietà semantica non banale dei programmi è decidibile. La dimostrazione classica di questo teorema (e del Problema della Fermata) si basa su due passaggi che richiedono l'uso della Legge del Terzo Escluso (LEM) e della diagonalizzazione:

Diagonalizzazione: Costruzione di un programma che si comporta in modo opposto a un ipotetico deciditore.
Split su $\bot$ : Una distinzione di casi basata sul fatto che un programma che diverge sempre ( $\bot$ ) soddisfi o meno la proprietà $P$ in questione ( $P(\bot) \lor \neg P(\bot)$ ).

Questi approcci sono intrinsecamente classici e non validi nella logica intuizionista, rendendo difficile l'integrazione di tali risultati in sistemi di verifica formale come Coq o Rocq senza assumere assiomi classici. L'obiettivo del paper è fornire una dimostrazione costruttiva di questi teoremi, valida nella logica intuizionista, che elimini la necessità di LEM, diagonalizzazione e auto-riferimento.

2. Metodologia

L'autore propone una riduzione diretta dal Decidibilità del Decimo Problema di Hilbert (MRDP) al Teorema di Rice, evitando di passare attraverso il Problema della Fermata come intermedio classico.

L'idea chiave: Costruzione a Due Testimoni

Invece di costruire un singolo programma che si auto-riferisce, l'autore associa a ogni polinomio diofanteo $D$ una coppia di programmi $(S^0_D, S^1_D)$ :

Se $D$ è risolvibile: I programmi $S^0_D$ e $S^1_D$ si comportano rispettivamente come due testimoni fissi $e_0$ (che non soddisfa $P$ ) e $e_1$ (che soddisfa $P$ ).
Se $D$ non è risolvibile: Entrambi i programmi divergono identicamente (si comportano come $\bot$ ).

La proprietà semantica $P$ è "non banale" per definizione se esistono testimoni espliciti $e_0$ e $e_1$ tali che $\neg P(e_0)$ e $P(e_1)$ .

Il Meccanismo di Contraddizione

Si ipotizza l'esistenza di un deciditore $Decide_P$ per la proprietà $P$ . Si definisce una funzione $\delta_D$ basata sulla differenza dei risultati del deciditore sui due programmi:
$\delta_D = Decide_P(S^1_D) - Decide_P(S^0_D)$

Caso Risolvibile: Poiché $S^1_D \simeq e_1$ e $S^0_D \simeq e_0$ , allora $P(S^1_D)$ è vero e $P(S^0_D)$ è falso. Di conseguenza, $\delta_D = 1 - 0 = 1$ .
Caso Non Risolvibile: Poiché $S^1_D \simeq S^0_D \simeq \bot$ , per estensionalità $P(S^1_D) \iff P(S^0_D)$ . Il deciditore restituirà lo stesso valore per entrambi, quindi $\delta_D = 0$ .

La funzione $D \mapsto \delta_D$ diventerebbe così un algoritmo decidibile per la risolvibilità diofantea. Tuttavia, il Teorema MRDP (insieme alla sua versione costruttiva) afferma che la risolvibilità diofantea è indecidibile. Questo genera una contraddizione costruttiva senza mai dover determinare il valore di verità di $P(\bot)$ o assumere $P(\bot) \lor \neg P(\bot)$ .

3. Contributi Chiave

Dimostrazione Costruttiva: Il primo teorema di Rice dimostrato interamente nella logica intuizionista, senza LEM, diagonalizzazione o auto-riferimento.
Riduzione Diretta a MRDP: Sposta il fondamento dell'indecidibilità dalla diagonalizzazione di Turing alla complessità aritmetica dei polinomi diofantei.
Eliminazione della Condizione di Totalità: A differenza di prove precedenti (es. Forster et al.), questa costruzione non richiede che i programmi testimoni $e_0$ e $e_1$ siano totali. I programmi $S^b_D$ passano l'intero "budget di fuel" (step-indexing) ai programmi testimoni senza modifiche, garantendo l'equivalenza osservazionale anche per programmi parziali.
Formalizzazione in Rocq (Coq): L'intero sviluppo è stato formalizzato nel proof assistant Rocq (Coq).
- Il modello di calcolo utilizzato è basato su step-indexing (funzioni $N \to (N \to \text{option } N)$ ).
- L'unica assunzione esterna è l'indecidibilità del Decimo Problema di Hilbert (MRDP), già dimostrata costruttivamente in coq-library-undecidability.
- Il comando Print Assumptions conferma che il Teorema di Rice e il Problema della Fermata sono "chiusi sotto il contesto globale" (nessun assioma classico aggiunto).

4. Risultati

Teorema di Rice Costruttivo: È stato dimostrato che non esiste alcun programma che decide una proprietà semantica non banale, validando il risultato in logica intuizionista.
Problema della Fermata come Corollario: L'indecidibilità del Problema della Fermata è derivata come conseguenza immediata (in una riga di codice Rocq) applicando il Teorema di Rice alla proprietà "Terminates". Questo inverte la direzione classica: invece di derivare Rice dalla Fermata, la Fermata deriva da Rice (che deriva da MRDP).
Gerarchia di Grado: Il paper introduce un concetto di "Rice degree", suggerendo che l'indecidibilità può essere testimoniata da polinomi diofantei di grado fino a 4 (grazie alla codifica MRDP), sollevando questioni aperte sulla complessità minima necessaria.

5. Significato e Impatto

Verifica Formale e Estrazione di Programmi: Poiché la prova è costruttiva, il ragionamento sull'indecidibilità può essere internalizzato in sistemi come Coq e Agda senza violare la logica intuizionista. Questo permette di ragionare su proprietà di programmi all'interno di ambienti di verifica formale senza assumere assiomi classici.
Reverse Mathematics Costruttiva: Il lavoro contribuisce a identificare con precisione quali principi non costruttivi sono necessari per i teoremi di indecidibilità, dimostrando che l'LEM non è essenziale se si parte dall'indecidibilità diofantea.
Nuova Prospettiva sulla Riduzione: La tecnica della "riduzione non ramificata" (non-branching reduction), dove l'informazione è codificata nella differenza relazionale tra due programmi ( $\delta_D$ ) piuttosto che in una distinzione di casi su un singolo programma, offre una struttura matematica di interesse indipendente per la teoria della computazione.
Indipendenza dal Modello: La prova è valida in qualsiasi modello di calcolo che soddisfi l'interfaccia di equivalenza osservazionale definita, rendendola robusta e generalizzabile.

In sintesi, il paper risolve un problema aperto nella logica costruttiva fornendo una prova elegante e formalmente verificabile dell'indecidibilità, spostando il baricentro dalla logica dei programmi alla teoria dei numeri (problemi diofantei).