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.

Chapter. Primitive Recursive Functions.

Section. Primitive Recursive Predicates and Bounded Minimalization.

Exercise. Show that the case discrimination function $D (x, y, z)$ , where

D (x, y, z) = v \leftrightarrow x \neq 0 \land v = y \lor x = 0 \land v = z

is primitive recursive.

D (x, y, z) = ?

[CL] Remark. In the sequel do not use the non-strict version of the function $D$ from the module Standard; it plays the role of if-then-else construct.

Exercise. Show that the characterstic function of the equality predicate $x = y$ is primitive recursive.

(x =_{*} y) = ?

Exercise. Show that the boolean functions are primitive recursive.

(\neg_{*} x) = ?

(x \land_{*} y) = ?

(x \lor_{*} y) = ?

(x \to_{*} y) = ?

(x \leftrightarrow_{*} y) = ?

Exercise. (1 point) Show that primitive recursive functions are closed under the operator of bounded minimalization.

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

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

f (x, y) = μ z ≦ x [g (z, y) = 1]

Proof.

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 _b

Theorem. Primitive recursive functions are closed under the operator of bounded minimalization.

Bounded formulas.

[CL] Syntax. Examples:

Atomic formulas: $x = y$ , $R (x)$ .
Propositional connectives: $⊤$ , $⊥$ , $\neg R$ , $R \land Q$ , $R \lor Q$ , $R \to Q$ , $R \leftrightarrow Q$ .
Bounded quantification: $\exists y y ≦ x : R$ , $\forall y y ≦ x : R$ , $\exists y y < x : R$ , $\forall y y < x : R$ .
Notational conventions: $x \neq y$ .

Explicit definitions of predicates with bounded formulas.

[CL] Syntax. Examples:

R (x) \leftrightarrow \exists y y ≦ x : Q (x, y)

R (x) \leftrightarrow \exists y y < x : Q (x, y)

R (x) \leftrightarrow \forall y y ≦ x : Q (x, y)

R (x) \leftrightarrow \forall y y < x : Q (x, y)

Theorem. Primitive recursive functions are closed under explicit definitions of predicates with bounded formulas.

Theorem. The standard comparision predicates are primitive recursive.

Proof. The claim follows from

x ≦ y \leftrightarrow \exists z z ≦ y : x = z

x < y \leftrightarrow \neg y ≦ x

x ≧ y \leftrightarrow y ≦ x

x > y \leftrightarrow y < x

[CL] Remark. From now on you can use the builtin comparison predicates.

Definitions of functions with bounded minimalization.

[CL] Syntax. Examples:

f (x) = μ y ≦ x [R (x, y)]

f (x) = μ y < x [R (x, y)]

Theorem. Primitive recursive functions are closed under definitions of functions with bounded minimalization.

Exercise. Show that the integer division function $x \div y$ is primitive recursive. Recall that $x \div 0 = 0$ .

x \div y = ?

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

Exercise. Show that the remainder function $x mod y$ is primitive recursive. Recall that $x mod 0 = 0$ .

x \mod y = ?

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

Subsection. Exercises.

Exercise. Show that the predicate of divisibility

x ∣ y \leftrightarrow \exists z y = x \cdot z

is primitive recursive.

x ∣ y \leftrightarrow ?

Exercise. (1 bonus point) Show that the predicate $Prime (x)$ holding of prime numbers is primitive recursive.

Prime (x) \leftrightarrow ?

Exercise. Show that the integer square root function

⌊ \sqrt{x} ⌋ = y \leftrightarrow y^{2} ≦ x \land x < {(y + 1)}^{2}

is primitive recursive

⌊ \sqrt{x} ⌋ = ?