Rice's Theorem

Wenn du eine IDE baust (IntelliJ). Der Benutzer fragt: "Wird diese Variable jemals null sein?" Deine IDE antwortet: "Vielleicht." (Warnung). Sie kann nicht "Ja" oder "Nein" beweisen (wegen Rice). Triviale Eigenschaften sind entscheidbar ("Enthält der Code 5 Zeilen?"). Semantische Eigenschaften ("Was tut der Code?") sind unentscheidbar.

1. Nicht-Trivial

Was heißt "nicht-trival"? Eine Eigenschaft $P$ ist nicht-trivial, wenn es mindestens ein Programm gibt, das sie hat, und mindestens eines, das sie nicht hat. "Ist das Programm ein Programm?" -> Trivial (Ja für alle). "Berechnet es die Quadratwurzel?" -> Nicht-trival (Manche ja, manche nein). Rice sagt: Man kann die Turing-Maschinen nicht in "Wurzel-Rechner" und "Nicht-Wurzel-Rechner" sortieren.

2. Extensional vs. Intensional

Rice gilt für extensionale Eigenschaften (Input/Output Verhalten). Es gilt nicht für intensionale Eigenschaften (Wie der Code aussieht). "Hat der Code 100 Schritte?" -> Entscheidbar. "Nutzt der Code Rekursion?" -> Entscheidbar. Deshalb funktionieren Linter.

1. Beweis durch Reduktion vom Halteproblem

Wie beweist man Rice? Durch Widerspruch. Angenommen, es gäbe einen Code-Prüfer WillPrintHello(Code). Wir bauen ein neues Programm P':

1. Simuliere Programm X auf Input Y. (Das Halteproblem).
2. Wenn X hält, drucke "Hello". Hätte unser Prüfer WillPrintHello(P') eine Antwort, wüssten wir sofort, ob X auf Y hält. Da das Halteproblem unlösbar ist, muss auch die Frage nach "Hello" unlösbar sein. Dieser Trick funktioniert für jede semantische Eigenschaft.

2. Index-Mengen & Kleenes Rekursionstheorem

Mathematisch betrachtet Rice die Index-Menge $S$ einer Funktionsklasse. Wenn $S$ die Menge aller "Indizes" (Programme) ist, die die Funktion $f$ berechnen, dann ist $S$ entweder leer, die Menge aller Programme, oder nicht-rekursiv (unentscheidbar). Ein tieferer Grund liegt im Rekursionstheorem von Kleene: Jedes Programm kann seinen eigenen Quellcode "kennen" und manipulieren. Ein Programm könnte also einen Rice-Prüfer fragen: "Werde ich X tun?", und dann genau das Gegenteil tun. Deshalb kann kein Prüfer jemals für alle Programme korrekt sein.

3. Approximation in der Produktion

Da wir laut Rice nichts beweisen können, nutzt die Industrie (z. B. bei der Verifikation von Flugzeug-Software) Sound Approximations.

• Over-Approximation: "Ich finde alle möglichen Fehler, melde aber auch viele Fehlalarme (False Positives)." (Statische Analyse).
• Under-Approximation: "Ich melde nur echte Fehler, finde aber nicht alle." (Testing/Fuzzing). Rice's Theorem zwingt uns dazu, uns zwischen diesen beiden Welten zu entscheiden – Fehlerfreiheit und Vollständigkeit sind gleichzeitig technisch unmöglich.