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. General Recursive Functions.

Section. $μ$ -recursive Functions.

Definition of $μ$ -recursive functions.

Theorem. The class of $μ$ -recursive functions is primitively recursively closed.

Corollary.

Every primitive recursive function is $μ$ -recursive.
Every primitive recursive predicate is $μ$ -recursive.
$μ$ -recursive functions are closed under explicit definitions.
$μ$ -recursive predicates are closed under explicit definitions of predicates with bounded formulas.
$μ$ -recursive functions are closed under nested simple recursion.

Theorem. $μ$ -recursive functions are closed under regular minimalization.

Exercise. (2 points) Consider the following definition of the Ackermann-Péter function by nested double recursion:

A (0, y) = y + 1

A (x + 1, 0) = A (x, 1)

A (x + 1, y + 1) = A (x, A (x + 1, y))

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

\forall x \forall y \exists z f^{+} (z, x + 1, y + 1) = A (x, y) + 1

z_{1} ≦ z_{2} \land f^{+} (z_{1}, x + 1, y + 1) = v + 1 \to f^{+} (z_{2}, x + 1, y + 1) = v + 1

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

d (x, y) = ?

A (x, y) = ?

Theorem. The class of $μ$ -recursive functions is closed under regular recursion.

Theorem. The class of general recursive functions coincides with the class of $μ$ -recursive functions.