Smn-Theorem

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Das -Theorem ist ein zentrales Resultat der Berechenbarkeitstheorie. Es stellt ein Hilfsmittel dar, mit dem man den Code eines Programms in Abhängigkeit von Parametern berechnen kann, und wurde erstmals durch Stephen C. Kleene bewiesen (vgl. Rekursionssatz). Ein Resultat daraus ist, dass eine Programmiersprache, die zur Laufzeit generierten Code ausführen kann, Currying unterstützen kann.

Formale Definition[Bearbeiten | Quelltext bearbeiten]

Sei eine effektive Nummerierung aller partiell berechenbaren Funktionen (bspw. die Gödel-Nummerierung aller deterministischen Turing-Maschinen).

Angenommen für einen festen Index sei die entsprechende Funktion vom Typ , dann gibt es eine totale und berechenbare Funktion mit

für alle .

Nichtformale Erklärung[Bearbeiten | Quelltext bearbeiten]

Die Eigenschaft besagt, dass es zu einem Code , der mit den Parametern und ausgeführt wird (bzw. ausgeführt werden kann), ein Transformationsprogramm gibt, das aus , und ein Programm berechnet, welches bei der Eingabe von das Gleiche berechnet, wie bei der Eingabe von und .

Beispiele[Bearbeiten | Quelltext bearbeiten]

Das -Theorem ist eine Möglichkeit aus Funktionen, deren Berechenbarkeit bereits bekannt ist, neue zu konstruieren.

Es sei beispielsweise zu zeigen, dass eine totale und berechenbare Funktion existiert, so dass für gilt: .

Definiere dazu . Die Funktion ist berechenbar, es existiert also ein Index , so dass gilt: . Aus dem -Theorem folgt nun die Existenz einer total berechenbaren Funktion mit für alle . Nun definieren wir , ist dann offenbar ebenfalls total berechenbar und es gilt:

Insbesondere wird das -Theorem oft verwendet, um Reduktionsfunktionen zu konstruieren:

Als Beispiel soll das allgemeine Halteproblem auf das Epsilon-Halteproblem reduziert werden. Genauer ist also die Existenz einer total berechenbaren Funktion zu zeigen, so dass für alle gilt .

Analog zu oben definiert man , die Funktion ist offensichtlich berechenbar und ihr Wert hängt nicht von ab. Es sei also ein Index, so dass . Das -Theorem liefert jetzt die Existenz einer total berechenbaren Funktion , so dass . Setzt man und wählt , ergibt sich