Smn-Theorem

Das ${\displaystyle s_{n}^{m}}$-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 ${\displaystyle \{\varphi _{i}\}_{i\in \mathbb {N} }}$ eine effektive Nummerierung aller partiell berechenbaren Funktionen (bspw. die Gödel-Nummerierung aller deterministischen Turing-Maschinen).

Angenommen für einen festen Index ${\displaystyle i}$ sei die entsprechende Funktion vom Typ ${\displaystyle \varphi _{i}\colon \mathbb {N} ^{m+n}\to \mathbb {N} }$, dann gibt es eine totale und berechenbare Funktion ${\displaystyle s_{n}^{m}\colon \mathbb {N} ^{m+1}\to \mathbb {N} }$ mit

${\displaystyle \varphi _{s_{n}^{m}(i,y_{1},...,y_{m})}(z_{1},...,z_{n})=\varphi _{i}(y_{1},...,y_{m},z_{1},...,z_{n})}$ für alle ${\displaystyle (y_{1},...,y_{m},z_{1},...,z_{n})\in \mathbb {N} ^{m+n}}$.

Nichtformale Erklärung

Die ${\displaystyle s_{n}^{m}}$Eigenschaft besagt, dass es zu einem Code ${\displaystyle w}$, der mit den Parametern ${\displaystyle x}$ und ${\displaystyle v}$ ausgeführt wird (bzw. ausgeführt werden kann), ein Transformationsprogramm ${\displaystyle U}$ gibt, das aus ${\displaystyle w}$, ${\displaystyle x}$ und ${\displaystyle v}$ ein Programm ${\displaystyle w_{x}}$ berechnet, welches bei der Eingabe von ${\displaystyle v}$ das Gleiche berechnet, wie ${\displaystyle w}$ bei der Eingabe von ${\displaystyle x}$ und ${\displaystyle v}$.

Beispiele

Das ${\displaystyle s_{n}^{m}}$-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 ${\displaystyle g\colon \mathbb {N} ^{2}\to \mathbb {N} }$ existiert, so dass für ${\displaystyle i,j,x\in \mathbb {N} }$ gilt: ${\displaystyle \varphi _{g(i,j)}(x)=\varphi _{i}(x)+\varphi _{j}(x)}$.

Definiere dazu ${\displaystyle \psi (i,j,x)=\varphi _{i}(x)+\varphi _{j}(x)}$. Die Funktion ${\displaystyle \psi }$ ist berechenbar, es existiert also ein Index ${\displaystyle k\in \mathbb {N} }$, so dass gilt: ${\displaystyle \psi =\varphi _{k}}$. Aus dem ${\displaystyle s_{n}^{m}}$-Theorem folgt nun die Existenz einer total berechenbaren Funktion ${\displaystyle s_{1}^{2}\colon \mathbb {N} ^{3}\to \mathbb {N} }$ mit ${\displaystyle \varphi _{s_{1}^{2}(k,i,j)}(x)=\varphi _{k}(i,j,x)=\psi (i,j,x)}$ für alle ${\displaystyle i,j,x\in \mathbb {N} }$. Nun definieren wir ${\displaystyle g(i,j):=s_{1}^{2}(k,i,j)}$, ${\displaystyle g}$ ist dann offenbar ebenfalls total berechenbar und es gilt:

${\displaystyle \varphi _{g(i,j)}(x)=\varphi _{s_{1}^{2}(k,i,j)}(x)=\psi (i,j,x)=\varphi _{i}(x)+\varphi _{j}(x)}$

Insbesondere wird das ${\displaystyle s_{n}^{m}}$-Theorem oft verwendet, um Reduktionsfunktionen zu konstruieren:

Als Beispiel soll das allgemeine Halteproblem ${\displaystyle H=\{(i,x)\in \mathbb {N} ^{2}\mid \varphi _{i}(x){\downarrow }\}}$ auf das Epsilon-Halteproblem ${\displaystyle H_{0}=\{e\in \mathbb {N} \mid \varphi _{e}(0){\downarrow }\}}$ reduziert werden. Genauer ist also die Existenz einer total berechenbaren Funktion ${\displaystyle f\colon \mathbb {N} ^{2}\to \mathbb {N} }$ zu zeigen, so dass für alle ${\displaystyle i,x\in \mathbb {N} }$ gilt ${\displaystyle \varphi _{i}(x){\downarrow }\Leftrightarrow \varphi _{f(i,x)}(0){\downarrow }}$.

Analog zu oben definiert man ${\displaystyle \psi (i,x,y)=\varphi _{i}(x)}$, die Funktion ${\displaystyle \psi }$ ist offensichtlich berechenbar und ihr Wert hängt nicht von ${\displaystyle y}$ ab. Es sei also ${\displaystyle k}$ ein Index, so dass ${\displaystyle \psi =\varphi _{k}}$. Das ${\displaystyle s_{n}^{m}}$-Theorem liefert jetzt die Existenz einer total berechenbaren Funktion ${\displaystyle s_{1}^{2}}$, so dass ${\displaystyle \varphi _{s_{1}^{2}(k,i,x)}(y)=\varphi _{k}(i,x,y)}$. Setzt man ${\displaystyle f(i,x)=s_{1}^{2}(k,i,x)}$ und wählt ${\displaystyle y=0}$, ergibt sich

${\displaystyle \varphi _{f(i,x)}(0)=\varphi _{k}(i,x,0)=\psi (i,x,0)=\varphi _{i}(x).}$