Smn-Theorem

Das -Theorem ist ein zentrales Resultat der Berechenbarkeitstheorie. Es stellt ein Hilfsmittel in der Informatik 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

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

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

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

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.