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.

[CL] Remark. Clausal form of function definitions is allowed.

Chapter. Primitive Recursive Functions.

Section. Recursion with Measure.

Exercise. Consider the following recursive definition of the greatest common divisor function:

\gcd (x, y) = \max (x, y) \leftarrow x = 0

\gcd (x, y) = \max (x, y) \leftarrow x \neq 0 \land y = 0

\gcd (x, y) = \gcd (x, y ∸ x) \leftarrow x \neq 0 \land y \neq 0 \land x < y

\gcd (x, y) = x \leftarrow x \neq 0 \land y \neq 0 \land x = y

\gcd (x, y) = \gcd (x ∸ y, y) \leftarrow x \neq 0 \land y \neq 0 \land x > y

This is a recursion with a suitable measure $μ [x, y]$ such that

x \neq 0 \land y \neq 0 \land x < y \to μ [x, y ∸ x] < μ [x, y]

x \neq 0 \land y \neq 0 \land x > y \to μ [x ∸ y, y] < μ [x, y]

Derive the function $\gcd (x, y)$ as primitive recursive with the help of its approximation function $f^{+} (z, x, y)$ such that

z > μ [x, y] \to f^{+} (z, x, y) = \gcd (x, y)

μ [x, y] = ?

f^{+} (z, x, y) = ?

\gcd (x, y) = ?

Exercise. (2 points) Consider the following recursive definition:

Flatten (0) = 0

Flatten (u, 0) = Flatten (u), 0

Flatten (u, v, w) = Flatten ((u, v), w)

This is a recursion with a suitable measure $μ [x]$ such that

μ [u] < μ [u, 0]

μ [(u, v), w] < μ [u, v, w]

Derive the function $Flatten (x)$ as primitive recursive with the help of its approximation function $f^{+} (z, x)$ such that

z > μ [x] \to f^{+} (z, x) = Flatten (x)

μ [x] = ?

f^{+} (z, x) = ?

Flatten (x) = ?

Exercise. Consider the recursive definition of McCarthy 91 function:

f_{91} (x) = f_{91} f_{91} (x + 11) \leftarrow x < 101

f_{91} (x) = x ∸ 10 \leftarrow x ≧ 101

This is a recursion with a suitable measure $μ [x]$ such that

x < 101 \to μ [x + 11] < μ [x]

x < 101 \to μ [f_{91} (x + 11)] < μ [x]

Derive the function $f_{91} (x)$ as primitive recursive with the help of its approximation function $f^{+} (z, x)$ such that

z > μ [x] \to f^{+} (z, x) = f_{91} (x)

μ [x] = ?

f^{+} (z, x) = ?

f_{91} (x) = ?

Exercise. (2 points) Consider the following recursive definition:

f_{19} (x) = x ∸ 2 \leftarrow x > 20

f_{19} (x) = f_{19} f_{19} (x + 3) \leftarrow x ≦ 20

This is a recursion with a suitable measure $μ [x]$ such that

x ≦ 20 \to μ [x + 3] < μ [x]

x ≦ 20 \to μ [f_{19} (x + 3)] < μ [x]

Derive the function $f_{19} (x)$ as primitive recursive with the help of its approximation function $f^{+} (z, x)$ such that

z > μ [x] \to f^{+} (z, x) = f_{19} (x)

μ [x] = ?

f^{+} (z, x) = ?

f_{19} (x) = ?

Theorem. Primitive recursive functions are closed under recursion with measure.