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

Literature.

[1] 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. See [1].

Section. Course of Values Recursion.

Course of values recursive definitions.

Course of values functions. In the following examples use the method of course values sequences to show that the functions in question are primitive recursive.

Exercise. The Fibonacci function ${fib}_{n}$ has the following course of values recursive definition:

{fib}_{0} = 0

{fib}_{1} = 1

{fib}_{n + 2} = {fib}_{n + 1} + {fib}_{n}

Show that the function is primitive recursive.

Hint. First, rewrite the definiton to the standard course of values recursion with monadic discrimination.

{fib}_{0} = ?

{fib}_{n + 1} = ?

Proof.

\overline{f} (n) = ?

Note that we require

L \overline{f} (n) = n + 1

k ≦ n \to {fib}_{k} = {(\overline{f} (n))}_{n ∸ k}

{fib}_{n} = ?

Exercise. (bonus 1 point) The binary size function ${∣ x ∣}_{b}$ has the following course of values recursive definition (with binary discrimination):

{∣ 2 \cdot x + 0 ∣}_{b} = 0 \leftarrow x = 0

{∣ 2 \cdot x + 0 ∣}_{b} = {∣ x ∣}_{b} + 1 \leftarrow x \neq 0

{∣ 2 \cdot x + 1 ∣}_{b} = {∣ x ∣}_{b} + 1

Show that the function is primitive recursive.

Hint. First, rewrite the definiton to the standard course of values recursion with monadic discrimination.

{∣ 0 ∣}_{b} = ?

{∣ x + 1 ∣}_{b} = ?

Proof.

\overline{f} (x) = ?

Note that we require

L \overline{f} (x) = x + 1

z ≦ x \to {∣ z ∣}_{b} = {(\overline{f} (x))}_{x ∸ z}

{∣ x ∣}_{b} = ?

Exercise. (bonus 1 point) The pair size function $| x |_{p}$ has the following course of values recursive definition (with pair discrimination):

{∣ 0 ∣}_{p} = 0

{∣ v, w ∣}_{p} = {∣ v ∣}_{p} + {∣ w ∣}_{p} + 1

Show that the function is primitive recursive.

Hint. First, rewrite the definiton to the standard course of values recursion with monadic discrimination.

{∣ 0 ∣}_{p} = ?

{∣ x + 1 ∣}_{p} = ?

Proof.

\overline{f} (x) = ?

Note that we require

L \overline{f} (x) = x + 1

z ≦ x \to {∣ z ∣}_{p} = {(\overline{f} (x))}_{x ∸ z}

{∣ x ∣}_{p} = ?

Theorem. Primitive recursive functions are closed under course of values recursive definitions.

******************************************************************************
********************************* DEBUGGING **********************************
******************************************************************************

Course of values functions.

\overline{f} (0) = {fib}_{0}, 0

\overline{f} (n + 1) = {fib}_{n + 1}, \overline{f} (n)

\overline{f} (0) = {fib}_{0}, 0

\overline{f} (n + 1) = {fib}_{n + 1}, \overline{f} (n)

\overline{f} (0) = {∣ 0 ∣}_{b}, 0

\overline{f} (x + 1) = {∣ x + 1 ∣}_{b}, \overline{f} (x)

\overline{f} (0) = {∣ 0 ∣}_{b}, 0

\overline{f} (x + 1) = {∣ x + 1 ∣}_{b}, \overline{f} (x)

\overline{f} (0) = {∣ 0 ∣}_{p}, 0

\overline{f} (x + 1) = {∣ x + 1 ∣}_{p}, \overline{f} (x)

\overline{f} (0) = {∣ 0 ∣}_{p}, 0

\overline{f} (x + 1) = {∣ x + 1 ∣}_{p}, \overline{f} (x)

Debugging.

Test_fun (x) = ?

Itfa (0, a) = a

Itfa (n + 1, a) = Itfa (n, (n, Test_fun (n)), a)

Itf (n) = Itfa (n, 0)

Test_pred (x) \leftrightarrow ?

Itpa (0, a) = a

Itpa (n + 1, a) = Itpa (n, n, a) \leftarrow Test_pred (n)

Itpa (n + 1, a) = Itpa (n, a) \leftarrow \neg Test_pred (n)

Itp (n) = Itpa (n, 0)