Dopo aver visto che il problema della fermata è indecidibile, viene da chiedersi se sia un caso isolato. Il teorema di Rice risponde che no: è la regola. Qualunque domanda non banale sul comportamento di un programma, cioè sulla funzione che calcola o sul linguaggio che riconosce, è indecidibile. È uno dei risultati più generali e più pratici della teoria della calcolabilità, perché delimita con precisione che cosa possono e non possono fare gli strumenti automatici di verifica.
Proprietà semantiche e proprietà sintattiche
Bisogna distinguere due tipi di domande su una macchina di Turing M.
Proprietà sintattiche: riguardano la descrizione di M, il suo «testo».
- M ha più di 20 stati?
- M contiene una transizione che scrive il simbolo X?
- M entra nello stato q₅ entro i primi 100 passi sull'input vuoto?
Molte di queste sono decidibili: basta leggere la descrizione o simulare un numero limitato di passi.
Proprietà semantiche: riguardano soltanto il linguaggio L(M) riconosciuto da M. Due macchine che riconoscono lo stesso linguaggio hanno la proprietà entrambe o nessuna delle due.
- L(M) è vuoto?
- L(M) contiene la stringa 0101?
- L(M) è finito?
- L(M) è regolare?
- L(M) = Σ*, cioè M accetta tutto?
Il teorema di Rice riguarda queste ultime.
L'enunciato
Sia P una proprietà dei linguaggi Turing-riconoscibili. P è non banale se esiste almeno una macchina il cui linguaggio ha la proprietà e almeno una il cui linguaggio non ce l'ha. Allora:
il linguaggio {⟨M⟩ : L(M) ha la proprietà P} è indecidibile.
Le proprietà banali sono solo due: quella che vale per tutti i linguaggi riconoscibili e quella che non vale per nessuno. Per esse la risposta è sempre sì o sempre no, e la decisione è immediata.
L'idea della dimostrazione
Si riduce A_TM, già noto come indecidibile, al problema di decidere P.
Supponiamo, senza perdita di generalità, che il linguaggio vuoto non abbia la proprietà P (altrimenti si ragiona sul complemento di P). Poiché P è non banale, esiste una macchina T con L(T) dotato della proprietà.
Data una coppia ⟨M, w⟩, costruiamo una macchina M′ che, su input x:
- simula M su w;
- se M accetta w, esegue T su x e risponde come T.
Ora osserviamo:
- se M accetta w, M′ si comporta come T, quindi L(M′) = L(T), che ha la proprietà;
- se M non accetta w, M′ non accetta niente, quindi L(M′) = ∅, che non ha la proprietà.
Un decisore per P, applicato a ⟨M′⟩, deciderebbe se M accetta w. Poiché la costruzione di M′ a partire da ⟨M, w⟩ è meccanica, otterremmo un decisore per A_TM, che non esiste.
Esempi di applicazione
| Domanda | Semantica? | Non banale? | Decidibile? |
|---|---|---|---|
| L(M) è vuoto? | Sì | Sì | No |
| L(M) contiene la stringa vuota? | Sì | Sì | No |
| L(M) è regolare? | Sì | Sì | No |
| M ha almeno 10 stati? | No | — | Sì |
| M, sull'input vuoto, muove mai la testina a sinistra? | No | — | Sì, con un argomento apposito |
| L(M) è riconoscibile? | Sì | No, è banale | Sì (la risposta è sempre sì) |
La riga sul movimento a sinistra è istruttiva: è una proprietà della macchina, non del linguaggio, e Rice non si applica. Si dimostra decidibile osservando che una macchina che va sempre a destra, dopo aver superato l'input, legge solo blank e quindi o si ferma o ripete uno stato entro un numero limitato di passi.
Le conseguenze per il software reale
Tradotto nel linguaggio dei programmi, il teorema di Rice dice che non esiste un analizzatore che, per ogni programma, decida correttamente:
- se il programma restituisce sempre il risultato giusto rispetto a una specifica;
- se due programmi calcolano la stessa funzione;
- se un programma può mai produrre una certa uscita, come la stampa di una password;
- se un programma contiene codice che verrà effettivamente eseguito con qualche input;
- se un file eseguibile, una volta lanciato, si comporterà in modo dannoso.
L'ultimo punto ha un significato concreto nella sicurezza informatica: nessun antivirus può riconoscere con certezza, in ogni caso, tutti e soli i programmi dannosi, se «dannoso» è definito in termini di comportamento.
Come si lavora comunque
Il teorema non condanna l'analisi automatica, ma impone dei compromessi. Le strade che si usano in pratica sono:
- Approssimazione sicura: l'analizzatore può segnalare falsi allarmi ma non perdere problemi reali (o viceversa). È l'approccio di molti strumenti di analisi statica e dei sistemi di tipi.
- Restrizione del linguaggio: su programmi senza cicli illimitati, o su modelli a stati finiti, molte domande diventano decidibili. Il model checking sfrutta questo fatto.
- Proprietà sintattiche: le firme e le regole sulle sequenze di byte guardano il testo del programma, non il comportamento, e per questo sono decidibili; il prezzo è che si aggirano modificando il codice.
- Verifica assistita: un essere umano fornisce invarianti e prove, e la macchina si limita a controllarle.
In sintesi
- Le proprietà semantiche dipendono solo dal linguaggio riconosciuto, non dal testo del programma.
- Il teorema di Rice: ogni proprietà semantica non banale è indecidibile.
- La dimostrazione riduce A_TM costruendo una macchina che si comporta come T oppure non accetta nulla.
- Le proprietà sintattiche, come il numero di stati, restano spesso decidibili.
- Gli strumenti reali convivono con il teorema tramite approssimazioni, restrizioni e verifica assistita.
