Stelling van Rice

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

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[bewerken]

Voor een woord w noteren we de Turingmachine die door w wordt gecodeerd als M_w. Laat R de klasse van Turing-berekenbare partiële functies zijn, en een S een deelverzameling daarvan zodat S\neq\emptyset en S\neq R. De taal \{ w \mid M_w \text{ berekent een functie uit } S \} is niet beslisbaar.

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[bewerken]

Voorbeeld 1[bewerken]

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[bewerken]

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.

Gevolgen in de praktijk[bewerken]

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 practische 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[bewerken]

  • 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.