Clausal Language (ver. 5.81.21, 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.

[CL] CL-TeX.

Chapter. Primitive Recursive Functions.

Section. Nested Simple Recursion.

Subsection. Nested Simple Recursion: Case $k = 2$ and One Parameter.

Exercise. (bonus 5 points) Show that if $g (y)$ , $h (x, z_{1}, z_{2}, y)$ , $s_{1} (x, y)$ and $s_{2} (x, y, z_{1})$ are all primitive recursive then so is $f (x, y)$ defined by

f (0, y) = g (y)

f (x + 1, y) = h (x, f (x, s_{1} (x, y)), f (x, s_{2} (x, y, f (x, s_{1} (x, y)))), y)

Hint. Derive the function as primitive recursive with the help of its course of values function:

\overline{f} (0, y) = f (0, y), 0, 0

\overline{f} (x + 1, y) = f (x + 1, y), \overline{f} (x, s_{1} (x, y)), \overline{f} (x, s_{2} (x, y, f (x, s_{1} (x, y))))

Proof.

Local update. The 4-ary function $U (x, y, t, i)$ updates the partial computation tree $t$ for $f (x, y)$ at position $i$ by a correct value. Show that the function is primitive recursive.

[CL] Remark. Clausal language allowed in the definition of this function.

U (x, y, t, i) = ?

Global update. The 4-ary function $M_{i} (x, y, t)$ updates the partial computation tree $t$ for $f (x, y)$ at each position $j < i$ by a correct value. Show that the function is primitive recursive.

M_{i} (x, y, t) = ?

Perfect binary trees. The function $Mkpbt (n)$ creates a perfect binary tree of the depth $n$ . Show that the function is primitive recursive.

Mkpbt (n) = ?

Course of values function. Show that the function $\overline{f} (x, y)$ is primitive recursive.

\overline{f} (x, y) = ?

Final step. Show that the function $f (x, y)$ is primitive recursive.

f (x, y) = ?

[CL] Remark. You can test your solution by interpreting the theory. Choose non-local interpretation.

Subsection. Nested Simple Recursion: General Case.

Theorem. Primitive recursive functions are closed under nested simple recursion.

Query:

Heap used: 359428 free: 133856280

Time used: 0:0:0:51