Smn-Theorem

Das $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 $\{\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 $i$ sei die entsprechende Funktion vom Typ $\varphi _{i}\colon \mathbb {N} ^{m+n}\to \mathbb {N}$, dann gibt es eine totale und berechenbare Funktion $s_{n}^{m}\colon \mathbb {N} ^{m+1}\to \mathbb {N}$ mit

$\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 $(y_{1},...,y_{m},z_{1},...,z_{n})\in \mathbb {N} ^{m+n}$.

Nichtformale Erklärung

Die $s_{n}^{m}$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 $w_{x}$ berechnet, welches bei der Eingabe von $v$ das Gleiche berechnet, wie $w$ bei der Eingabe von $x$ und $v$.

Beispiele

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

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

$\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 $s_{n}^{m}$-Theorem oft verwendet, um Reduktionsfunktionen zu konstruieren:

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

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

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