Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Recursive Functions. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Lecture Notes in Theory of Computability. 2001.
[3] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
[4] I. Korec. Úvod do teórie algoritmov. Skriptá MFF UK, 1981.

Chapter. Primitive Recursive Functions.

Section. Backward Recursion.

Exercise. Show that if $g (y)$ , $h (x, z, y)$ and $b (y)$ are all primitive recursive then so is $f (x, y)$ defined by

f (x, y) = g (y) \leftarrow x ≧ b (y)

f (x, y) = h (x, f (x + 1, y), y) \leftarrow x < b (y)

Hint. Define $f (x, y)$ with the help of a binary p.r. function $\tilde{f} (v, y)$ such that

v + x = b (y) \to \tilde{f} (v, y) = f (x, y)

\tilde{f} (v, y) = ?

f (x, y) = ?

[CL] Remark. You can test your solution by interpreting the theory. Choose non-local interpretation and set component identifier suffix to the string _1

Exercise. (1 point) Show that if $g (x, y)$ , $h (x, z, y)$ and $b (y)$ are all primitive recursive then so is $f (x, y)$ defined by

f (x, y) = g (x, y) \leftarrow x ≧ b (y)

f (x, y) = h (x, f (x + 1, y), y) \leftarrow x < b (y)

Hint. Define $f (x, y)$ with the help of a binary p.r. function $\tilde{f} (v, y)$ such that

v + x = b (y) \to \tilde{f} (v, y) = f (x, y)

\tilde{f} (v, y) = ?

f (x, y) = ?

[CL] Remark. You can test your solution by interpreting the theory. Choose non-local interpretation and set component identifier suffix to the string _2

Theorem. Primitive recursive functions are closed under backward recursion.

Query:

Heap used: 331860 free: 133884280

Time used: 0:0:1:45