CSC 341: February 23, 2007

From CSWiki

1 Instructor's notes for the class session
- 1.1 "Programming" in the notation for recursive functions
2 Study questions
- 2.1 Proposed Solutions

Instructor's notes for the class session

"Programming" in the notation for recursive functions

The notation that I use to express the construction of primitive recursive functions using composition and recursion is designed to bring out some similarities between proof construction and programming: If a function can be defined in this notation, as developed in the first nine sections of the handout, then the definition itself is a proof by construction that the function is, by definition, primitive recursive.

This doesn't automatically make the proofs really easy, since the notation isn't as flexible, robust, or programmer-friendly as most contemporary high-level programming languages. However, after you read it and write it for a while, certain idioms become natural.

For instance, when you need a ternary function that adds one to its middle argument and returns the result, it's natural to think of the C version

int bump_middle(int x, y, z) {
  return y++;
}

or the Scheme version

(lambda (x y z)
  (+ y 1))

and try to write something like $\texttt{[successor\ }y\texttt{]}$ or (recognizing that the middle value has to be selected from the three inputs) $\texttt{[successor\ }\texttt{pr}^1_3\texttt{]}$ . But this is wrong: In the notation, a left bracket has to be followed by a higher-order constructor, something that combines or connects numeric functions to form other numeric functions, rather than by a numeric function like successor. So the correct expression is $\texttt{[}\texttt{o}^1_3\texttt{\ successor\ }\texttt{pr}^1_3\texttt{]}$ .

Sometimes students look at expressions like these and wonder: But where do the inputs come from? How does the notation refer to them? The answer is that the inputs to the function as a whole don't come from anywhere until a computation is actually started (by applying the function to actual arguments). The expression is a blueprint for the machine that carries out the computation of the function; the inputs don't arrive until the machine is actually started. And the notation itself doesn't have any way to refer to any of the inputs, although it does have projection functions, which can be used to pick out any of the inputs that are needed, in the order in which they are needed.

If you're translating the body of a Scheme procedure into this notation, then, you replace every occurrence of a parameter with the projection function that would pick out that parameter, and then add function-composition operators as necessary to make sure that the selected values are transmitted to the functions that need them.

[edit]

Study questions

Describe the values of the function $\texttt{[}\bar{\mu}_1\texttt{\ divides?]}$ .
Describe the values of the function $\texttt{[}\bar{\mu}_1\texttt{\ [}\texttt{o}^2_2\texttt{\ divides?\ }\texttt{pr}^0_2\texttt{\ [}\texttt{o}^1_2\texttt{\ successor\ }\texttt{pr}^1_2\texttt{]]]}$ .
Extend the notation for primitive recursive functions to include the bounded existential quantification $\texttt{[}\bar{\exists}_n\texttt{\ }p\texttt{]}$ of any primitive recursive predicate $p$ of valence $n + 1$ , defined by $\texttt{[}\bar{\exists}_n\texttt{\ }p\texttt{]}(x_0, \ldots, x_{n - 1}, x_n) = 1 \Longleftrightarrow p(x_0, \ldots, x_{n - 1}, x)\textrm{\ is\ truish\ for\ some\ } x \le x_n.$
Prove that the binary function lcm, which computes the least common multiple of its arguments, is primitive recursive.

[edit]

Proposed Solutions

Given inputs $x 0, x 1$ , the function yields the least natural number $i$ such that $i \le x_1$ and $x 0$ evenly divides $i$ . Won't $i$ always be 0?
Given inputs $x 0, x 1$ , the function yields the least natural number $i$ such that $i \le x_1$ and $x 0$ evenly divides $i + 1$ .