Stelling van Rice

De stelling van Rice is een belangrijke stelling in de theoretische informatica, meer in het bijzonder in de berekenbaarheidstheorie. Informeel zegt de stelling dat het onmogelijk is een algoritme te schrijven dat als invoer een ander algoritme en een bepaalde niet-triviale eigenschap krijgt en in alle gevallen correct beslist of het algoritme die eigenschap bezit. Uit de stelling volgt dat automatische verificatie van software in het algemeen niet mogelijk is.

De stelling is genoemd naar de Amerikaanse logicus en wiskundige Henry Gordon Rice, die hem in 1954 in zijn proefschrift voor het eerst bewees.

Formele bewering

Voor een woord $w$ noteren we de turingmachine die door $w$ wordt gecodeerd als $M_{w}$. Laat $R$ de klasse van turingberekenbare partiële functies zijn, en een $S$ een deelverzameling daarvan zodat $S\neq \emptyset$ en $S\neq R$. De stelling van Rice zegt dat de taal $\{w\mid M_{w}{\text{ berekent een functie uit }}S\}$ niet beslisbaar is.

Behalve voor turingmachines geldt de stelling ook voor andere turingvolledige berekenmodellen.

De eigenschappen van turingmachines waarover de stelling van Rice gaat, doen uitspraken over de soort functie die de turingmachine berekent. De stelling van Rice doet geen uitspraak over andere eigenschappen van turingmachines. Het aantal toestanden van een turingmachine kan men bijvoorbeeld gewoon tellen, de taal $\{w\mid M_{w}{\text{ heeft }}k{\text{ toestanden}}\}$ is (voor een constante $k$) dus beslisbaar. Ook worden twee deelverzamelingen van berekenbare functies uitgesloten. Aangezien alle turingmachines een functie berekenen, bestaat $\{w\mid M_{w}{\text{ berekent een functie uit }}R\}$ uit alle turingmachines, en de verzameling van alle turingmachines is beslisbaar. Aan de andere kant geldt ook dat $\{w\mid M_{w}{\text{ berekent een functie uit }}\emptyset \}=\emptyset$ een beslisbare verzameling is.

Voorbeelden

Voorbeeld 1

Laat $f_{0}$ de functie zijn die gedefinieerd is door $f_{0}(x)=0$ ($f_{0}$ is dus de constante 0-functie) en $S=\{f_{0}\}$. Dan geldt dat $S\subseteq R$, $S\neq \emptyset$ en $S\neq R$. Uit de stelling van Rice volgt dus dat het onmogelijk is algoritmisch in alle gevallen te bepalen of een gegeven turingmachine de constante 0-functie berekent.

Voorbeeld 2

Laat $S$ uit alle totale functies bestaan. Dan is $S$ een niet-lege, echte deelverzameling van $R$ en dus volgt uit de stelling van Rice dat $\{w\mid M_{w}{\text{ berekent een totale functie}}\}$ (dit is gelijk aan $\{w\mid M_{w}{\text{ termineert voor elke invoer}}\}$) niet beslisbaar is. Uit dit voorbeeld blijkt dat het feit dat het stopprobleem onbeslisbaar is direct uit de stelling van Rice volgt.

Gevolgen in de praktijk

De stelling van Rice heeft verstrekkende gevolgen in de praktijk. Het volgt namelijk uit de stelling dat het onmogelijk is een computerprogramma te schrijven dat in alle gevallen correct beslist of een programma aan een functionele specificatie voldoet. Dat betekent dat automatische softwareverificatie in het algemeen niet mogelijk is.

Dit betekent echter niet dat automatische softwareverificatie geen interessant gebied is. Ten eerste geldt de stelling van Rice niet voor minder krachtige berekeningsmodellen. Die minder krachtige berekeningsmodellen kunnen in de praktijk toch krachtig genoeg zijn voor praktische toepassingen. Ten tweede is het wel mogelijk een programma te schrijven dat weliswaar niet in alle gevallen een correct antwoord levert, maar wel in een groot deel van de gevallen.

Literatuur

• John E. Hopcroft, Rajeev Motwani en Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd ed.). Addison-Wesley, 2006.
• Uwe Schöning. Theoretische Informatik - Kurz gefasst (5. Auflage). Spektrum, 2008.