Stone: Section 7

From CSWiki

Theorems

Theorem 7.1: cons(x,y) is primitive recursive

Theorem 7.2:

• car(ls) is primtive recursive

• cdr(ls) is primitive recursive

Theorem 7.3: nth-cdr(ls,x) is primitive recursive

Theorem 7.4: length(ls) is primitive recursive

Theorem 7.5: list-ref(ls,x) is primitive recursive

Theorem 7.6: iteration is primitive recursive

Theorem 7.7: truncate(n,s) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string

Theorem 7.8: string-length(n,s) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string

Theorem 7.9: string-ref(n,s,p) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string
 p is the zero-based position in the string (from the right-hand side)

Theorem 7.10: concatenate(n,s0,s1) is primitive recursive

 n is the size of the alphabet
 s0 is the encoding for the left-hand string
 s1 is the encoding for the right-hand string

Theorem 7.11:

• ss(n,s,p,t) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string
 p is the zero-based position at which the substring begins
 t is the length of the substring to be extracted

• substring(n,s,p,e) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string
 p is the zero-based position at which the substring begins
 e is the zero-based position just before which the substring ends

Theorem 7.12: string-update(n,s,p,a) is primitive recursive

 n is the size of the alphabet
 s is the encoding for the string
 p is the zero-based position of the symbol to be replaced
 a is the encoding for the symbol to replace the symbol at position p

Example

An encoding for a list

3800 = cons(3, 237) = cons(3, cons(0, 118)) = cons(3, cons(0, cons(1, 29))) = cons(3, cons(0, cons(1, cons(0, 14)))) = cons(3, cons(0, cons(1, cons(0, cons(1, 3))))) = (3 0 1 0 1 0 0)

Misunderstandings

Q. The concatenation function appears to take two strings (s₀ and s₁) and concatenate them into the new string s₁s₀. It appears this way to me because the symbols on the right side of a string are encoded with a higher integer according to the section on strings and s₀ is the number that is being multiplied by n^m.

A. Check the section on strings again -- the positional weights of the symbols in a string increase as you go from right to left, as in ordinary base-ten numeration, not from left to right. It is written on page 20 that

For any string x and any symbol a from the alphabet, the encoding of xa is the sum of a's serial number and n times the encoding of x.

So, when you add a symbol at the right end of a string, the contribution of that symbol to the encoding is between 1 and n (the size of the alphabet), and the contribution of every symbol to its left is scaled up by a factor of n. In a string of length k, the leftmost symbol has been scaled up in this way k − 1 times and contributes somewhere between n^{k − 1} and n^k to the encoding.