Chapter III

APPENDIX Normal Form Theorem S-m-n Theorem

This appendix presents the technical details of proving the Kleene Normal Form Theorem, and the S-m-n Theorem via the important technique of “arithmetization”. These lead to basic results in recursive unsolvability and semirecursiveness.

We also include a proof of Kleene’s recursion theorem and an application (Rice’s Theorem).

P has been defined in class as the closure of {λx.0, λx.x + 1} ∪ {λx⃗_{n}.x_{i} : 1 ≤ i ≤ n & n ∈ ℕ} under composition, primitive recursion and unbounded search. We will assign “program codes” to each function, using our usual prime-power coding, namely,

⟨x_{0}, …, x_{n}⟩ = ∏_{i≤n} p_{i}^{x_{i}+1}

We recall the following definition, (1), of the “concatenation function”.

x ∗ y =^{def} x · ∏_{i<lh(y)} p_{i+lh(x)}^{exp(i,y)}  (1)

This yields a primitive recursive function λxy.x ∗ y. It is immediate that “∗” deserves the name, because

⟨a⃗⟩ ∗ ⟨b⃗⟩ = ⟨a⃗, b⃗⟩

for all a⃗ and b⃗. We next “arithmetize” P-functions and their “computations”. We will assign “program codes” to each function. A program code—called a “G“”odelnumber” or a “ϕ-index”, or just an “index” in the literature—is, intuitively, a number in ℕ that codes the “instructions” necessary to compute a P-function.

If i ∈ ℕ is a^{†} code for f ∈ P, then we write

f = {i} Kleene’s notation

or

f = ϕ_{i}^{‡} Rogers’ [Rog67] notation

Thus, either notation, {i} or ϕ_{i}, denotes the function with code i.

The following table assigns inductively Gödel numbers (middle column) to all functions P. In the table, f̂ indicates a code of f.

Function  Code  Comment
λx.0  ⟨0, 1, 0⟩
λx.x + 1  ⟨0, 1, 1⟩
λx⃗_{n}.x_{i} ⟨0, n, i, 2⟩ 1 ≤ i ≤ n
composition: f(g_{1}(y⃗_{m}), …, g_{n}(y⃗_{m})) ⟨1, m, f̂, ĝ_{1}, …, ĝ_{n}⟩  f must be n-ary

all g_{i} must be m-ary

primitive recursion from

“basis” h and “iterated” part g ⟨2, n + 1, ĥ, ĝ⟩ h must be n-ary

g must be (n + 2)-ary

unbounded search: (μy)f(y, x⃗_{n})  ⟨3, n, f̂⟩  f must be (n + 1)-ary

OK, we have been somewhat loose in our description above. “The following table assigns inductively”, we have said, perhaps leading the reader to think that we are defining the codes by recursion on P. Not so. After all, each function has infinitely many codes.

What is really involved here—see also below—is defining the set of all ϕindices, here called Φ, as a subset of {z : Seq(z)}. Φ is the smallest set of “codes” that contains the “initial ϕ-indices”

I = {⟨0, 1, 0⟩, ⟨0, 1, 1⟩} ∪ {⟨0, n, i, 2⟩ : n > 0 & 1 ≤ i ≤ n}

and is closed under the following three operations:

(i) Coding composition: Input a and b_{i} (i = 1, …, n) causes output

⟨1, m, a, b_{1}, …, b_{n}⟩

provided (a)_{1} = n and (b_{i})_{1} = m, for i = 1, …, n.

(ii) Coding primitive recursion: Input a and b causes output

⟨2, n + 1, a, b⟩

provided (a)_{1} = n and (b)_{1} = n + 2.

†The indefinite article is appropriate here. Exactly as in “real life” a “computable” function has infinitely many different programs that compute it, a partial recursive function f has infinitely many different codes (see 0.3 later on).

‡That’s where the name “ϕ-index” comes from.

Supplementary Lecture Notes, C5111/C4111 (Fall 2001)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

(iii) Coding unbounded search: Input a causes output

⟨3, n, a⟩

provided (a)_{1} = n + 1 and n > 0.^{†}

By the uniqueness of prime number decomposition, the following recursive definition that assigns functions to indices is unambiguous.

We define by recursion on Φ a total function λa.{a} (or λa.ϕ_{a}) for each a ∈ Φ, that is, a function that maps codes to functions of P:

{⟨0, 1, 0⟩} = λx.0
{⟨0, 1, 1⟩} = λx.x + 1
{⟨0, n, i, 2⟩} = λx⃗_{n}.x_{i}
{⟨1, m, a, b_{1}, …, b_{n}⟩} = λy⃗_{m}.{a}({b_{1}}(y⃗_{m}), …, {b_{n}}(y⃗_{m}))
{⟨2, n + 1, a, b⟩} = λxy⃗_{n}.P rec({a}, {b})
{⟨3, n, a⟩} = λx⃗_{n}.(μy){a}(y, x⃗_{n})

In the above recursive definition we have used the abbreviation P rec({a}, {b}) for the function given (for all x, y⃗_{n}) by the primitive recursive schema with “h-part” {a} and “g-part” {b}.

We can now make the intentions implied in the above table official:

0.1 Theorem. P = {{a} : a ∈ Φ}.

Proof. ⊆-part. Induction on P. The previous table encapsulates the argument diagrammatically.

⊇-part. Induction on Φ. It follows trivially from the recursive definition of {a} and the fact that P contains the initial functions and is closed under composition, primitive recursion and unbounded search. □

0.2 Remark. (Important) Thus, f ∈ P iff for some a ∈ ℕ, f = {a}.

0.3 Example. Every function f ∈ P has infinitely many ϕ-indices. Indeed, let f = {f̂}. Since f = λx⃗_{n}.u_{1}^{1}(f(x⃗_{n})), we obtain f = {⟨1, ⟨0, 1, 1, 2⟩, f̂⟩}. Since ⟨1, ⟨0, 1, 1, 2⟩, f̂⟩ > f̂, the claim follows. □

†By an obvious I.H. the other cases can fend for themselves, but, here, reducing the number of arguments must not result to 0 arguments, as we have decided not to allow 0-ary functions.

Supplementary Lecture Notes, C5111/C4111 (Fall 2001)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

0.4 Theorem. The relation x ∈ Φ is primitive recursive.

Proof. Let χ denote the characteristic function of x ∈ Φ. Then

χ(0) = 1
χ(x + 1)= 0 if  x + 1 = ⟨0, 1, 0⟩ ∨ x + 1 = ⟨0, 1, 1⟩∨

(∃n, i)_{≤x}(n > 0 & 0 ≤ i ≤ n & x + 1 = ⟨0, n, i, 2⟩)∨

(∃a, b, m, n)_{≤x}(χ(a) = 0 & (a)_{1} = n & Seq(b) &
lh(b) = n & (∀i)_{<n}(χ((b)_{i}) = 0 & ((b)_{i})_{1} = m) &
x + 1 = ⟨1, m, a⟩ ∗ b)∨
(∃a, b, n)_{≤x}(χ(a) = 0 & (a)_{1} = n & χ(b) = 0 &
(b)_{1} = n + 2 & x + 1 = ⟨2, n + 1, a, b⟩)∨

(∃a, n)_{≤x}(χ(a) = 0 & (a)_{1} = n + 1 & x + 1 = ⟨3, n, a⟩)

= 1 otherwise

The above can easily be seen to be a course-of-values recursion. For example, if H(x) = ⟨χ(0), …, χ(x)⟩, then an occurrence of “χ(a) = 0” above can be replaced by “(H(x))_{a} = 0”, since a ≤ x. □

We think of^{†} a computation as a sequence of equations like {e}(a⃗) = b. Such an equation is intuitively read as “the program e, when it executes on input a⃗, produces output b”. An equation will be legitimate iff

(i) it states an input-output relation of some initial function (i.e., case where (e)_{0} = 0), or

(ii) it states an input-output relation according to ϕ-indices e such that (e)_{0} ∈ {1, 2, 3}, using results (i.e., equations) that already appeared in the sequence.

For example, in order to state (μy){e}(y, a⃗_{n}) = b one must ensure that all the following equations, where the r_{i}’s are all non-zero,

{e}(b, a⃗_{n}) = 0, {e}(0, a⃗_{n}) = r_{0}, …, {e}(b − 1, a⃗_{n}) = r_{b−1}

have already appeared in the sequence. In our coding, every equation {a}(a⃗_{n}) = b will be denoted by a triple ⟨e, a⃗_{n}, b⟩ that codes, in that order, the ϕ-index, the input and the output. We will collect (code) all these triples into a single code, u = ⟨…, ⟨e, a⃗_{n}, b⟩, …⟩.

Before proceeding, let us recall that Seq(z) ↔ x > 1 & (∀y)_{≤x}(∀z)_{≤x}(y|x & P r(y) & P r(z) & z < y → z|x) and lh(z) = (μy)_{≤z}¬p_{y}|z. We also define the following two primitive recursive predicates:

†“We think of” indicates our determination to avoid a rigorous definition. The integrity of our exposition will not suffer from this.

Supplementary Lecture Notes, C5111/C4111 (Fall 2001)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

(1) λuv.u ∈ v (“v is a term in the (coded) sequence u”)

(2) λuvw.v < _{u}w (“v occurs before w in the (coded) sequence u”)

Primitive recursiveness follows from the equivalences

v ∈ u ↔ Seq(u) & (∃i)_{≤u}(u)_{i} = v
v < _{u}w ↔ v ∈ u & w ∈ u & (∃i, j)_{≤u}((u)_{i} = v & (u)_{j} = w & i < j)

We are now ready to define the relation “Computation(u)” which holds iff “u codes a computation according to the previous understanding”. This involves a lengthy formula. In the interest of readability, comments enclosed in { }-brackets are included on the left margin, to indicate the case under consideration.

Computation(u)↔Seq(u) & (∀v)_{≤u}[v ∈ u →
{λx.0} (∃x)_{≤u}v = ⟨⟨0, 1, 0⟩, x, 0⟩∨
{λx.x + 1} (∃x)_{≤u}v = ⟨⟨0, 1, 1⟩, x, x + 1⟩∨
{λx⃗_{n}.x_{i}} (∃x, n, i)_{≤u}{Seq(x) & n = lh(x) & i < n &

v = ⟨⟨0, n, i + 1, 2⟩⟩ ∗ x ∗ ⟨(x)_{i}⟩}∨

{composition} (∃x, y, f̂, ĝ, m, n, z)_{≤u}{Seq(x) & Seq(y) & Seq(f̂) &

Seq(ĝ) & n = lh(x) & n = lh(ĝ) & m = lh(y) &

(f̂)_{1} = n & (∀i)_{<n}(Seq((ĝ)_{i}) & ((ĝ)_{i})_{1} = m) &

v = ⟨⟨1, m, f̂⟩ ∗ ĝ⟩ ∗ y ∗ ⟨z⟩ &

⟨f̂⟩ ∗ x ∗ ⟨z⟩ < _{u}v & (∀i)_{<n}⟨(ĝ)_{i}⟩ ∗ y ∗ ⟨(x)_{i}⟩ < _{u}v}∨

{prim. recursion} (∃x, y, ĥ, ĝ, n, c)_{≤u}{Seq(ĥ) & (ĥ)_{1} = n & Seq(ĝ) &

(ĝ)_{1} = n + 2 & Seq(y) & lh(y) = n & Seq(c) &

lh(c) = x + 1 & v = ⟨⟨2, n + 1, ĥ, ĝ⟩, x⟩ ∗ y ∗ ⟨(c)_{x}⟩ &

⟨ĥ⟩ ∗ y ∗ ⟨(c)_{0}⟩ <_{u} v & (∀i)_{<x}⟨ĝ, i⟩ ∗ y ∗ ⟨(c)_{i}, (c)_{i+1}⟩ < _{u}v}∨

{(μy)f(y, x⃗_{n})} (∃f̂, y, x, n, r)_{≤u}{Seq(f̂) & (f̂)_{1} = n + 1 & n > 0 &

Seq(x) & lh(x) = n & Seq(r) & lh(r) = y &

v = ⟨⟨3, n, f̂⟩⟩ ∗ x ∗ ⟨y⟩ &

⟨f̂, y⟩ ∗ x ∗ ⟨0⟩ < _{u}v &

(∀i)_{<y}(⟨f̂, i⟩ ∗ x ∗ ⟨(r)_{i}⟩ < _{u}v & (r)_{i} > 0)}]

By inspection of the formula to the right of “↔” above we see that Computation(u) is primitive recursive.

0.5 Definition (The Kleene T -predicate). For each n ∈ ℕ, T^{(n)}(a, x⃗_{n}, z) stands for Computation((z)_{1}) & ⟨a, x⃗_{n}, (z)_{0}⟩ ∈ (z)_{1}. □

The above discussion yields immediately:

0.6 Theorem (Kleene Normal Form Theorem).

(1) y = {a}(x⃗_{n}) ≡ (∃z)(T^{(n)}(a, x⃗_{n}, z) & (z)_{0} = y)

(2) {a}(x⃗_{n}) = ((μz)T^{(n)}(a, x⃗_{n}, z))_{0}

(3) {a}(x⃗_{n}) ↓≡ (∃z)T^{(n)}(a, x⃗_{n}, z).

0.7 Remark. (Very important) The right hand side of 0.6(2), above, is mean-

ingful for all a ∈ ℕ, while the left hand side is only meaningful for a ∈ Φ. We now extend the symbols {a} and ϕ_{a} to be meaningful for all a ∈ ℕ. In all cases, the meaning is given by the right hand side of (2). Of course, if a ∉ Φ, then (μz)T^{(n)}(a, x⃗_{n}, z) ↑, for all x⃗_{n}, since T^{(n)}(a, x⃗_{n}, z)

will be false under the circumstances. Hence also {a}(x⃗_{n}) ↑, as it should be intuitively. In computer programmer’s jargon: “If the ‘program’ a is ‘syntactically incorrect’, then it will not ‘run’. Thus, it will ‘define’ the everywhere undefined function.”

We can now define a P-counterpart to R_{∗} and PR_{∗} and consider its closure properties.

0.8 Definition. (Semi-recursive relations or predicates) A relation P (x⃗) is semi-recursive iff for some f ∈ P, the equivalence

P (x⃗) ↔ f(x⃗) ↓  (1)

holds (for all x⃗, of course). Equivalently, we can state that P = dom(f). The set of all semi-recursive relations is denoted by P_{∗}^{†} If f = {a} in (1) above, then we say that “a is a semi-recursive index of P ”. If P has one argument (i.e., P ⊆ ℕ) and a is one of its semi-recursive indices,

then we write P = W_{a} ([Rog67]). □

We have at once

0.9 Corollary. (Normal Form Theorem for semi-recursive relations) P (x⃗_{n}) ∈ P_{∗} iff, for some a ∈ ℕ,

P (x⃗_{n}) ↔ (∃z)T^{(n)}(a, x⃗_{n}, z).

Proof. only if-part. This is 0.6(3). if-part. (∃z)T^{(n)}(a, x⃗_{n}, z) ↔ (μz)T^{(n)}(a, x⃗_{n}, z) ↓. But λx⃗_{n}.(μz)T^{(n)}(a, x⃗_{n}, z) ∈ P. □ Rephrasing the above (hiding the “a”, and remembering that PR_{∗} ⊆ R_{∗})

†We are making this symbol up. It is not standard in the literature.

Supplementary Lecture Notes, C5111/C4111 (Fall 2001)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

we have

0.10 Corollary. (Strong Projection Theorem) P (x⃗_{n}) ∈ P_{∗} iff, for some Q(x⃗_{n}, z) ∈ R_{∗},

P (x⃗_{n}) ↔ (∃z)Q(x⃗_{n}, z).

Here is a characterization of P_{∗} that is identical, in form, to the characterizations of PR_{∗} and R_{∗}.

0.11 Corollary. P (x⃗_{n}) ∈ P_{∗} iff, for some f ∈ P,

P (x⃗_{n}) ↔ f(x⃗_{n}) = 0.

Proof. only if-part. Say P (x⃗_{n}) ↔ g(x⃗_{n}) ↓. Take f = λx⃗_{n}.0 · g(x⃗_{n}).

if-part. Let f = {a}. By 0.6(1), f(x⃗_{n}) = 0 ↔ (∃z)(T^{(n)}(a, x⃗_{n}, z) & (z)_{0} = 0). We are done by strong projection. □

We immediately obtain

0.12 Corollary. R_{∗} ⊆ P_{∗}.

Intuitively, for a predicate R ∈ R_{∗} we have an algorithm (one that computes χ_{R}) that for any input x⃗ will halt and answer “yes” ( = 0) or “no” ( = 1) to the question “x⃗ ∈ R?”

For a predicate Q ∈ P_{∗} we are only guaranteed the existence of a weaker algorithm (for f ∈ P such that dom(f) = Q). It will halt iff the answer to the question “x⃗ ∈ Q?” is “yes” (and halting will amount to “yes”). If the answer is “no” it will never tell, because it will (as we say for non halting) “loop for ever” (or diverge). Hence the name “semi-recursive” for such predicates.

0.13 Theorem. R ∈ R_{∗} iff both R and ¬R are in P_{∗}.

Proof. only if-part. By 0.11 and closure of R_{∗} under ¬.

if-part. Let i and j be semi-recursive indices of R and ¬R respectively, that is

R(x⃗_{n}) ↔ (∃z)T^{(n)}(i, x⃗_{n}, z)
¬R(x⃗_{n}) ↔ (∃z)T^{(n)}(j, x⃗_{n}, z)

Define

g = λx⃗_{n}.(μz)(T^{(n)}(i, x⃗_{n}, z) ∨ T^{(n)}(j, x⃗_{n}, z))

Trivially, g ∈ P. Hence, g ∈ R, since it is total (Why?). We are done by noticing that R(x⃗_{n}) ↔ T^{(n)}(i, x⃗_{n}, g(x⃗_{n})). □

(Unsolvable Problems) A problem is a question “x⃗ ∈ R?” for any predicate R. “The problem x⃗ ∈ R is recursively unsolvable”, or just unsolvable, means that R ∉ R_{∗}, that is, intuitively, there is no algorithmic solution to the problem.

The “halting problem” has central significance in recursion theory. It is the question whether “program x will ever halt if it starts computing on input x”. That is, we set K = {x : {x}(x) ↓}. The halting problem is x ∈ K.^{†} We denote the complement of K by \overline{K}.

0.14 Theorem. (Unsolvability of the halting problem) The halting problem is unsolvable.

Proof. It suffices to show that \overline{K} is not semi-recursive. Suppose instead that i is a semi-recursive index of the set. Thus,

x ∈ \overline{K} ↔ (∃z)T^{(1)}(i, x, z)

or, making the part x ∈ \overline{K}—that is, \{x\}(x) ↑—explicit

¬(∃z)T^{(1)}(x, x, z) ↔ (∃z)T^{(1)}(i, x, z)  (1)

Substituting i into x in (1) we get a contradiction. □

K ∈ P_{∗}, of course, since {x}(x) ↓↔ T^{(1)}(x, x, z). We conclude that the inclusion R_{∗} ⊆ P_{∗} is proper, i.e., R_{∗} ⊂ P_{∗}.

0.15 Theorem. (Closure properties of P_{∗})

P_{∗} is closed under ∨, &, (∃y)_{<z}, (∃y), (∀y)_{<z}. It is not closed under either ¬ or (∀y).

Proof. We will rely on the normal form theorem for semi-recursive relations and the strong projection theorem.

Given semi-recursive relations P (x⃗_{n}), Q(y⃗_{m}) and R(y, u⃗_{k}) of semi-recursive indices p, q, r respectively. (∨:)

P (x⃗_{n}) ∨ Q(y⃗_{m}) ↔ (∃z)T^{(n)}(p, x⃗_{n}, z) ∨ (∃z)T^{(m)}(q, y⃗_{m}, z)
↔ (∃z)(T^{(n)}(p, x⃗_{n}, z) ∨ T^{(m)}(q, y⃗_{m}, z))

(&:)

P (x⃗_{n}) & Q(y⃗_{m}) ↔ (∃z)T^{(n)}(p, x⃗_{n}, z) & (∃z)T^{(m)}(q, y⃗_{m}, z)
↔ (∃w)((∃z)_{<w}T^{(n)}(p, x⃗_{n}, z) & (∃z)_{<w}T^{(m)}(q, y⃗_{m}, z))

†“K” is a reasonably well reserved symbol for the set {x : {x}(x) ↓}. Unfortunately, K is also used for the “first projection” of a “pairing function”, but the context easily decides which is which.

Supplementary Lecture Notes, C5111/C4111 (Fall 2001)\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

Breaking the pattern established by the proof for ∨ we may suggest a simpler proof: P (x⃗_{n}) & Q(y⃗_{m}) ↔ ((μz)T^{(n)}(p, x⃗_{n}, z) + (μz)T^{(m)}(q, y⃗_{m}, z)) ↓. Yet another proof, involving the decoding function λiz.(z)_{i} is

P (x⃗_{n}) & Q(y⃗_{m}) ↔ (∃z)T^{(n)}(p, x⃗_{n}, z) & (∃z)T^{(m)}(q, y⃗_{m}, z)
↔ (∃z)(T^{(n)}(p, x⃗_{n}, (z)_{0}) & T^{(m)}(q, y⃗_{m}, (z)_{1}))

There is a technical reason (soon to manifest itself) that we want to avoid “complicated” functions like λiz.(z)_{i} in the proof.

((∃y)_{<z}:)

(∃y)_{<z}R(y, u⃗_{k}) ↔ (∃y)_{<z}(∃w)T^{(k+1)}(r, y, u⃗_{k}, w)
↔ (∃w)(∃y)_{<z}T^{(k+1)}(r, y, u⃗_{k}, w)

((∃y):)

(∃y)R(y, u⃗_{k}) ↔ (∃y)(∃w)T^{(k+1)}(r, y, u⃗_{k}, w)
↔ (∃z)(∃y)_{<z}(∃w)_{<z}T^{(k+1)}(r, y, u⃗_{k}, w)

Both of the ∃-cases can be handled by the decoding function λiz.(z)_{i}. For example,

(∃y)R(y, u⃗_{k}) ↔ (∃y)(∃w)T^{(k+1)}(r, y, u⃗_{k}, w)
↔ (∃z)T^{(k+1)}(r, (z)_{0}, u⃗_{k}, (z)_{1})

((∀y)_{<z}:)

(∀y)_{<z}R(y, u⃗_{k}) ↔ (∀y)_{<z}(∃w)T^{(k+1)}(r, y, u⃗_{k}, w)
↔ (∃v)(∀y)_{<z}(∃w)_{<v}T^{(k+1)}(r, y, u⃗_{k}, w)

Think of v above as the successor (+1) of the maximum of some set of w-values, w_{0}, …, w_{z−1}, that “work” for y = 0, …, z − 1 respectively. The usual overkill proof of the above involves (z)_{i} (or some such decoding scheme) as follows:

(∀y)_{<z}R(y, u⃗_{k}) ↔ (∀y)_{<z}(∃w)T^{(k+1)}(r, y, u⃗_{k}, w)
↔ (∃w)(∀y)_{<z}T^{(k+1)}(r, y, u⃗_{k}, (w)_{y})

Regarding closure under ¬ and ∀y, K provides a counterexample to ¬, and ¬T^{(1)}(x, x, y) provides a counterexample to ∀y. □

(Recursively enumerable predicates) A predicate R(x⃗_{n}) is recursively enumerable, or r.e., iff R = ∅ or, for some f ∈ R of one variable, R = {x⃗_{n} : (∃m)f(m) = ⟨x⃗_{n}⟩}, or, equivalently

R(x⃗_{n}) ↔ (∃m)f(m) = ⟨x⃗_{n}⟩  (1)

By (1), R every r.e. relation is semi-recursive. The converse is also true.

0.16 Theorem. Every semi-recursive R is r.e.

Proof. Let a be a semi-recursive index of R. If R = ∅ then we are done. Suppose then R(a⃗_{n}) for some a⃗_{n}. We define a function f by cases

f(m) = \begin{cases}⟨(m)_{0}, …, (m)_{n−1}⟩ & if T^{(n)}(a, (m)_{0}, …, (m)_{n−1}, (m)_{n}) \\ ⟨a⃗_{n}⟩ & otherwise \end{cases}

It is trivial that f is recursive and satisfies (1) above. Indeed, our f is in PR. □

Suppose that i codes a “program” that acts on input variables x and y to compute a function λxy.f(x, y). It is certainly trivial to modify the program to compute λx.f(x, a) instead. In computer programming terms, we replace a “command” such as “read y” by one that says “y := a” (copy the value of a into y). From the original code, a new code (depending on i and a) ought to be trivially calculated.

This is the essence of Kleene’s iteration or “S-m-n” theorem below.

0.17 Theorem. (Kleene’s S-m-n or iteration theorem) There is a primitive recursive function λxy.σ(x, y) such that for all i, x, y,

{i}(⟨x, y⟩) = {σ(i, y)}(x)

Proof. Let a be a ϕ-index of λx.⟨x, 0⟩ and b a ϕ-index of λx.3x.

Next we find a primitive recursive λy.h(y) such that for all x and y

{h(y)}(x) = ⟨x, y⟩  (∗)

To achieve this observe that

⟨x, 0⟩ = {a}(x)

and

⟨x, y + 1⟩ = 3⟨x, y⟩ = {b}(⟨x, y⟩)

Thus, it suffices to take

h(0) = a
h(y + 1) = ⟨1, 1, b, h(y)⟩

Now that we have an h satisfying (∗), we note that

σ(i, y) =^{def} ⟨1, 1, i, h(y)⟩

will do. □

0.18 Corollary. There is a primitive recursive function λiy.k(i, y) such that, for all i, x, y,

{i}(x, y) = {k(i, y)}(x).

Proof. Let a_{0} and a_{1} be ϕ-indices of λz.(z)_{0} and λz.(z)_{1} respectively. Then {i}((z)_{0}, (z)_{1}) = {⟨1, 1, i, a_{0}, a_{1}⟩}(z) for all z, i. Take k(i, y) = σ(⟨1, 1, i, a_{0}, a_{1}⟩, y).

□

0.19 Corollary. There is for each m > 0 and n > 0 a primitive recursive function λiy⃗_{n}.S_{n}^{m}(i, y⃗_{n}) such that, for all i, x⃗_{m}, y⃗_{n},

{i}(x⃗_{m}, y⃗_{n}) = {S_{n}^{m}(i, y⃗_{n})}(x⃗_{m}).

Proof. Let a_{r} (r = 0, …, m − 1) and b_{r} (r = 0, …, n − 1) be ϕ-indices so that {a_{r}} = λxy.(x)_{r} (r = 0, …, m − 1) and {b_{r}} = λxy.(y)_{r} (r = 0, …, n − 1).

Set c(i) = ⟨1, 2, i, a_{0}, …, a_{m−1}, b_{0}, …, b_{n−1}⟩, for all i ∈ ℕ, and let d be a ϕ-index of λx⃗_{m}.⟨x⃗_{m}⟩.

Then,

{i}(x⃗_{m}, y⃗_{n}) = {c(i)}(⟨x⃗_{m}⟩, ⟨y⃗_{n}⟩)
= {k(c(i), ⟨y⃗_{n}⟩)}(⟨x⃗_{m}⟩)  by 0.18
= {⟨1, m, k(c(i), ⟨y⃗_{n}⟩), d⟩}(x⃗_{m})

Take λiy⃗_{n}.S_{n}^{m} = ⟨1, m, k(c(i), ⟨y⃗_{n}⟩), d⟩. □

0.20 Corollary. (Kleene’s recursion theorem) If λzx⃗.f(z, x⃗_{n}) ∈ P, then for some e,

{e}(x⃗_{n}) = f(e, x⃗_{n}) for all x⃗_{n}.

Proof. Let {a} = λzx⃗_{n}.f(S_{1}^{n}(z, z), x⃗_{n}). Then

f(S_{1}^{n}(a, a), x⃗_{n}) = {a}(a, x⃗_{n})
= {S_{1}^{n}(a, a)}(x⃗_{n})  by 0.19

Take e = S_{1}^{n}(a, a). □

0.21 Definition. A complete index set is a set A = {x : {x} ∈ Q} for some Q ⊆ P.

A is trivial iff A = ∅ or A = ℕ (correspondingly, Q = ∅ or Q = P). Otherwise it is non trivial. □

0.22 Theorem. (Rice) A complete index set is recursive iff it is trivial.

Thus, “algorithmically” we can only “decide” trivial properties of “programs”.

Proof. (The idea of this proof is attributed in [Rog67] to G.C. Wolpin.) if-part. Immediate, since χ_{∅} = λx.1. only if-part. By contradiction, suppose that A = {x : {x} ∈ Q} is non

trivial, yet A ∈ R_{∗}. So, let a ∈ A and b ∉ A. Define f by

f(x) = \begin{cases}b & if x ∈ A \\ a & if x ∉ A \end{cases}

Clearly,

x ∈ A iff f(x) ∉ A, for all x  (1)

By the recursion theorem, there is an e such that {f(e)} = {e} (apply 0.20 to λxy.{f(x)}(y)).

Thus, e ∈ A iff f(e) ∈ A, contradicting (1). □

Bibliography

[Rog67] H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, New York, 1967.