CSC 341: February 26, 2007
From CSWiki
Contents |
Instructor's notes for the class session
Defining new functions vs. defining new higher-order constructors
Section 4 introduces conditionals and the conditional-forming constructor
, which we can use to define primitive recursive functions by cases. The proof of Theorem 4.7, which justifies this mechanism, is slightly different in nature from the proofs of the theorems in section 3, which concerned single functions like add and divides?. It is more general, since it shows that the construction builds a primitive recursive function
, for any primitive recursive functions p, f, and g of valence n.
From a programming point of view, showing how to define a new primitive recursive function, like equal?, is like defining a new procedure in Scheme, while introducing a new constructor, like
, is more like defining a syntactic keyword in Scheme -- it expands the repertoire of expression types. The point of Theorem 4.7 is to show that this expansion is "conservative" and does not really affect the class of expressible (and hence primitive recursive) functions, since any function that can be defined with
can also be defined without it (and the proof of Theorem 4.7 shows how).
Accumulators
If we think of the notation for primitive recursive functions as analogous to a programming language, we have so far seen expressions for primitives (which are kind of analogous to literal constants), composition (which is kind of analogous to statement or expression sequencing in conventional programming language), recursion, and conditionals. The other kind of control structure that a programmer is likely to miss is a loop -- a mechanism for running through a series of possibilities and somehow accumulating or keeping track of an overall result.
The accumulator constructions described in section 6 abstract out three common kinds of loops in which the loop control variable is a natural number. Bounded quantification determines whether some Boolean condition is satisfied for every value of the loop control variable up to (and including) a specified limit. Bounded summation adds up the values of a specified function for every value of the loop control variable up to (and including) a specified limit. Bounded minimization searches for a value of the loop control variable (not exceeding a specified limit) that satisfies some Boolean condition. All of these can be valence-generalized to accommodate inputs other than the loop control variable.
The adjective "bounded" reflects the fact that these loops are forced to terminate once the limit is reached. Every function defined from primitive recursive functions by bounded quantification, bounded summation, or bounded minimization is primitive recursive (and Theorems 6.1, 6.2, and 6.3 show how).
Encodings for lists
The goal: To get a one-to-one correspondence between natural numbers and lists of natural numbers.
Pairing numbers: cons, car, and cdr. Leaving space for the null list. Nil and null?.
Iterates. The
operator.
Encodings for strings
The goal: Given any alphabet, to get a one-to-one correspondence between natural numbers and strings on that alphabet.
Lexicographic ordering doesn't work, because there is no upper bound on the length of a string. Instead, we need to ensure that any shorter string precedes any longer one, and then use lexicographic ordering to arrange strings of the same length.
Study questions
- What list is encoded by the natural number 3600?
- What natural number encodes the list (2, 4, 0)?
- Define a primitive recursive function cadr that extracts the second element of a list of two or more elements from its encoding.
- Describe the relationship between the inputs to the function
and its output.
- Using the alphabet
, what natural number encodes the string 1207? What string is encoded by the natural number 1310?
- Define a primitive recursive function index that takes three arguments -- the size of an alphabet, the encoding for a string in that alphabet, and the encoding for a symbol in that alphabet -- and returns the leftmost position in the string at which that symbol occurs, or 0 if there is no such position.
Proposed Solutions
- 3600 = cons(4, 225) = cons(4, cons(0, 112) = cons(4, cons(0, cons(4, 7) = (4 0 4 0 0 0)
- (2, 4, 0) = cons(2, cons(4, cons(0, nil))) = cons(2, cons(4, 1)) = cons(2, 48) = 388
-
-
- The encoding for 1207 is 2318 = 10*(10*(10*(10*0+2)+3)+1)+8, and 1310 = 10*(10*(10*(10*0+1)+2)+10)+10 encodes the string 0199.
-

