CSC 341: April 13, 2007

From CSWiki

1 Instructor's notes for the class session
2 Study questions
- 2.1 Proposed Solutions

Instructor's notes for the class session

What the parameter theorem says

The parameter theorem says that there is a class of primitive recursive functions -- in the handout, they are called sections and denoted by the identifier section, with appropriate subscripts and superscripts -- each taking as its first input the encoding for a partial recursive function, and taking as additional inputs numerical parameters that are to be, in effect, hard-coded into that partial recursive function. A section outputs the encoding for a partial recursive function of reduced valence, similar to the one encoded by the section's first input, but with the missing inputs simply set to constants that are supplied as the section's remaining inputs.

The key equation to remember is this one: If $e$ is the number that encodes the partial recursive function $f$ , then, for any natural numbers $u_0, \ldots, u_{n - 1}$ , $\texttt{section}^m_n (e, u_0, \ldots, u_{n - 1})$ is the encoding for a partial recursive function $g$ such that

$g(x_0, \ldots, x_{m - 1}) = f(x_0, \ldots, x_{m - 1}, u_0, \ldots, u_{n - 1}).$

The subscript $n$ in ` $\texttt{section}^m_n$ ' indicates the number of parameters and the superscript $m$ the valence of $g$ . This only works if the valence of $f$ is $m + n$ , of course.

[edit]

Proving the parameter theorem

The proof is by construction. It is easy to write a definition for $g$ in our notation, taking $f$ and $u_0, \ldots, u_{n - 1}$ as given:

$g \equiv \texttt{[}\circ^{m + n}_m\texttt{\ }f \texttt{\ pr}^0_m\texttt{\ }\ldots \texttt{pr}^{m - 1}_m \texttt{\ [}\circ^0_m \texttt{\ } u_0\texttt{-constant]\ } \ldots \texttt{\ [}\circ^0_m \texttt{\ } u_{n - 1}\texttt{-constant]]}$

Here each $u_i\texttt{-constant}$ is a nullary function that outputs $u i$ .

The construction in the parameter theorem simply translates this recipe for constructing $g$ into the notation itself, using the reflection methods introduced in section 11 of the handout. The details of the construction depend on $m$ and $n$ , but in ways that are quite regular and can be accommodated in a general construction template.

[edit]

Consequences of the parameter theorem

Many common functions operating on natural numbers, lists, strings, and other data structures can be thought of as sections of functions that we have already proven to be primitive recursive (e.g., halve is a section of quotient, square of raise-to-power, one? of equal?, etc.). It follows immediately from the parameter theorem that all such functions are themselves also primitive recursive.

However, some of the consequences of the parameter theorem are subtler. The handout develops the example of the converse function, which takes as input the encoding for any binary partial recursive function and outputs the encoding for its converse. It would be fairly straightforward to develop a proof that converse is primitive recursive, using the same strategy that we used to show that sections are primitive recursive: Given the encoding $e$ for any binary partial recursive function $f$ , we want converse to output the encoding for a binary partial recursive function $g$ such that $g (x 0, x 1) = f (x 1, x 0)$ . It is straightforward, in our notation, to write the definition that relates $g$ to $f$ , which is $g \equiv \texttt{[}\circ^2_2 \texttt{\ } f \texttt{\ pr}^1_2 \texttt{\ pr}^0_2 \texttt{]}$ , and we can then use reflection to abstract this pattern:

$\texttt{converse\ } \equiv \texttt{\ [} \circ^3_1 \texttt{\ encode-composition\ two}_1 \texttt{\ two}_1 \texttt{\ [} \circ^2_1 \texttt{\ cons\ pr}^0_1 \texttt{\ [} \circ^2_1 \texttt{\ cons\ [} \circ^2_1 \texttt{\ encode-projection-function\ one}_1 \texttt{\ two}_1 \texttt{]\ [} \circ^2_1 \texttt{\ cons\ [} \circ^2_1 \texttt{\ encode-projection-function\ zero}_1 \texttt{\ two}_1 \texttt{]\ nil}_1 \texttt{]]]]}$

But a different and more readily generalized approach is possible now that we have the parameter theorem. The idea is to express the dependence of $g$ on $f$ in a way that makes the encoding of $f$ visible, so that it can be treated as a parameter. The universality theorem can generally be used to do this; in the converse example, this use takes the form of the apply-binary function. We work up a partial recursive function that relates $g$ to $f$ and has the encoding for $f$ as an input, infer that this function has an encoding $t$ , and use an appropriate section and a constant function that outputs that encoding to help us define that high-level transformation we want (in this case, converse).

[edit]

Study questions

Use the parameter theorem to show that there is a primitive recursive function split-input that takes the encoding for any binary partial recursive function $f$ as input and outputs the encoding for a singulary partial recursive function $g$ such that $g (x) = f (x, x)$ for every natural number $x$ .
Use the parameter theorem to show that there is a primitive recursive function function-sum that takes as inputs the encodings for any singulary partial recursive functions $f$ and $g$ and outputs the encoding for a singular partial recursive function $h$ such that $h (x) = f (x) + g (x)$ for every natural number $x$ .