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  noteren we de turingmachine die door  wordt gecodeerd als . Laat  de klasse van turingberekenbare partiële functies zijn, en een  een deelverzameling daarvan zodat  en . De stelling van Rice zegt dat de taal  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  is (voor een constante ) dus beslisbaar. Ook worden twee deelverzamelingen van berekenbare functies uitgesloten. Aangezien alle turingmachines een functie berekenen, bestaat  uit alle turingmachines, en de verzameling van alle turingmachines is beslisbaar. Aan de andere kant geldt ook dat  een beslisbare verzameling is.

Voorbeelden

Voorbeeld 1 
Laat  de functie zijn die gedefinieerd is door  ( is dus de constante 0-functie) en . Dan geldt dat ,  en . 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  uit alle totale functies bestaan. Dan is  een niet-lege, echte deelverzameling van  en dus volgt uit de stelling van Rice dat  (dit is gelijk aan ) 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.

Theoretische informatica