decidibilità

La decidibilità è la proprietà di un problema di decisione: esiste un algoritmo che, per ogni input, fornisce una risposta corretta (sì o no) e termina in un numero finito di passi. In altri termini, un problema è decidibile se esiste una procedura computabile che determina definitivamente l’applicabilità della domanda per ogni possibile input.

Formalmente, si consideri un linguaggio L su un alfabeto. L è decidibile (o ricorsivo) se esiste una macchina di Turing che accetta esattamente le stringhe di L e si ferma per ogni input; in tal caso l’algoritmo decide se una data stringa appartiene o meno a L. Si distingue dai linguaggi ricorsivamente enumerabili (o semi-decidibili), per i quali esiste una macchina che enumerazione le stringhe di L e si ferma solo sui membri; potrebbe invece non fermarsi per gli input non appartenenti a L.

Esempi significativi: la logica proposizionale è decidibile tramite tavole della verità, mentre la logica del primo ordine non è decidibile in generale (l’“Entscheidungsproblem” è stato dimostrato impossibile). Il problema della fermata (Halting Problem) è indecidibile ma è ricorsivamente enumerabile: si può verificare se un programma si ferma, ma non si può decidere in tutti i casi.

Dal punto di vista teorico, una teoria è decidibile se il suo insieme di teoremi è decidibile; molti sistemi formali sono indecidibili, anche se parzialmente trattabili da metodi semi-decidibili. La decidibilità è una nozione fondamentale nella computabilità e nelle sue applicazioni, come la verifica formale e l’analisi dei limiti della formalizzazione matematica.