Smn-Theorem

Das $s_{n}^m$-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. Ein Resultat daraus ist, dass eine Programmiersprache, die zur Laufzeit generierten Code ausführen kann, Currying unterstützen kann.

Formale Definition

Gegeben sei $i \in \mathbb{N}$ mit $\varphi_{i}\colon \mathbb{N}^{m+n} \to \mathbb{N}$, wobei i die Programmcodenummer des berechenbaren Programms φ_i sei.

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 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 w_x berechnet, welches bei der Eingabe von v das gleiche berechnet, wie w bei der Eingabe von x und v.

Beispiel

Zu zeigen ist: Es existiert eine totale und berechenbare Funktion $g\colon \mathbb{N}^2 \to \mathbb{N}$, so dass für $i, j, x \in \mathbb{N}$ gilt: φ_g(i,j)(x) = φ_i(x) + φ_j(x).

Definiere ψ(i,j,x) = φ_i(x) + φ_j(x). ψ ist berechenbar und es existiert ein $k \in \mathbb{N}$, so dass gilt: ψ = φ_k.

Nach dem $s_{n}^m$-Theorem gilt:

Es existiert eine totale und berechenbare 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 total und 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)$