The s-m-n Theorem#
This section contains one of the most widely-used technical results in computability theory,Lemma 2 below.
Lemma 2
Let \(m\) and \(n\) be natural numbers.
There is a program \(s^m_n\) such that for all words \(p\), \(q_1\), \(\ldots\), \(q_m\), \(r_1\), \(\ldots\), \(r_n\),
Remark 1
The way the notation in \(s^m_n\) works is that we have \(m\) stored variables, and we expect \(n\) more to run \(p\).
Here is the statement in words:
If we start running \(s^m_n\) with \(p\) in R1, \(q_1\) in R2, and \(\ldots\), \(q_m\) in R\((m+1)\) then we get a word \(x\) in R1 (and all other registers empty).
If we then run \(x\) with \(r_1\) in R1,\(\ldots\), \(r_n\) in R\(n\), we would get the same thing as running the original \(p\) with \(q_1\) in R1, \(\ldots\), \(q_m\) in R\(m\), \(r_1\) in R\((m+1)\), \(\ldots\), \(r_m\) in R\((m+n)\).
We are not going to prove Lemma 2 in full, but we do want to give all the details on what is probably the most important special case, when \(m = n = 1\).
Example: \(s^1_1\)
We seek a program \(s^1_1\) so that
We take \(s^1_1\) to be
move_1_3 + move_2_1 + write + move_1_2 + [[write]](move_1_2) + move_2_1 + move_3_1
Before we check that this works, here is a comment on the difference between write and [[write]](move_1_2).
The program write takes whatever word \(x\) is in R1 and, using R2 as a temporary register, returns a program which
would write \(x\) after whatever is in R1. The program [[write]](move_1_2) puts the program move_1_2 after whatever
is in R1.
We verify that our proposal for \(s^1_1\) works by making tables of what happens after each of its sub-programs.
start |
move_1_3 |
move_2_1 |
write |
move_1_2 |
|
|---|---|---|---|---|---|
R1 |
p |
q |
|
||
R2 |
q |
q |
|
||
R3 |
p |
p |
p |
The reason for starting with move_1_3 is that write uses R2, so we need that register to be empty before executing write
Continuing:
|
move_2_1 |
move_3_1 |
|
|---|---|---|---|
R1 |
move_1_2 |
move_1_2 + |
move_1_2 + |
R2 |
|
||
R3 |
p |
p |
So we see that \([\![s^1_1]\!](p, q)\) is the program move_1_2 + [[write]](q) + p.
We run this program on r in R1.
start |
move_1_2 |
|
p |
|
|---|---|---|---|---|
R1 |
r |
q |
|
|
R2 |
r |
r |
As desired, we get \([\![ p]\!](q,r)\).
This concludes the verification.
Lemma 3
For each \(m\) and \(n\), [[s^m_n]] is a primitive recursive function.
Also, there is a primitive recursive function \(f:N\times N\to Words\) such that for all \(m\) and \(n\), \(f(m,n)\) has the property defining \(s^m_n\). That is,