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]

Gegeben sei mit , wobei die Gödelnummer des berechenbaren Programms sei.

Dann gibt es eine totale und berechenbare Funktion mit

für alle .

Nichtformale Erklärung[Bearbeiten | Quelltext bearbeiten]

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

Beispiel[Bearbeiten | Quelltext bearbeiten]

Zu zeigen ist: Es existiert eine totale und berechenbare Funktion , so dass für gilt: .

Definiere . ist berechenbar und es existiert ein , so dass gilt: .

Nach dem -Theorem gilt:

Es existiert eine totale und berechenbare Funktion mit für alle .

Nun definieren wir . ist total und berechenbar und es gilt: