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.

[CL] CL-TeX.

Chapter. Primitive Recursive Functions.

Section. Basic Development.

Exercise. Find a p.r. derivation of the following unary constant functions

C_{1} (x) = 1

C_{2} (x) = 2

C_{1} (x) = ?

C_{2} (x) = ?

Exercise. Find a p.r. derivation of the ternary constant function $C_{2}^{3} (x_{1}, x_{2}, x_{3}) = 2$ .

C_{2}^{3} (x_{1}, x_{2}, x_{3}) = ?

Constant functions are primitive recursive.

Explicit definitions of functions.

Exercise. (1 point) Show that primitive recursive functions are closed under explicit definitions.

Remark. Prove the claim for the special case in the following theory.

Show that if $G_{1}$ , $G_{2}$ and $G_{3}$ are p.r. functions then so is the ternary function $f$ defined by

f (x, y, z) = G_{3} (x, G_{2} (z, G_{1} (x)), 2)

Proof.

f (x, y, z) = ?

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

Theorem. Primitive recursive functions are closed under explicit definitions.

Primitive recursive definitions.

Remark. Two special cases are listed below.

Exercise. Show that primitive recursive functions are closed under iteration of unary functions.

Remark. Prove the claim in the following theory.

Show that if $f (x)$ is a unary p.r. function then so is its unary iteration $f^{n} (x)$ defined by

f^{0} (x) = x

f^{n + 1} (x) = f f^{n} (x)

Proof.

f^{n} (x) = ?

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

Exercise. (1 point) Show that primitive recursive functions are closed under parameterless primitive recursive definitions.

Remark. Prove the claim for the special case in the following theory.

Show that if $h (x, z)$ is a binary p.r. function then so is the unary function $f (x)$ defined by

f (0) = m

f (x + 1) = h (x, f (x))

Proof.

f (x) = ?

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

Theorem. Primitive recursive functions are closed under primitive recursive definitions.

Exercise. Show that the multiplication function $x \cdot y$ is primitive recursive.

x \cdot y = ?

[CL] Remark. From now on you can use the builtin function $x \cdot y$ .

Exercise. Show that the exponentiation function $x^{y}$ is primitive recursive.

x^{y} = ?

Exercise. Show that the summation function $\sum_{i = 0}^{n} i$ is primitive recursive.

\sum_{i = 0}^{n} i = ?

Exercise. Show that the predecessor function $x \dot{-} 1$ is primitive recursive.

x ∸ 1 = ?

Exercise. Show that the modified subtraction function $x \dot{-} y$ is primitive recursive.

x ∸ y = ?

[CL] Remark. From now on you can use the builtin function $x \dot{-} y$ .