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

Literature.

[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.

[CL] CL-TeX.

Chapter. Beginning of Arithmetization.

Section. Pairing Functions.

Subsection. Cantor Pairing Function.

Triangular numbers.

T_{n} = 1 + 2 + 3 + \dots + (n ∸ 1) + n

T_{n} = n \cdot (n + 1) \div 2

The 'inverse' of the triangular function. Define the unary function $T_{m}^{- 1}$ such that

T_{m}^{- 1} = n \leftrightarrow T_{n} ≦ m \land m < T_{n + 1}

Hint. Derivation is based on the following property of triangular numbers

8 \cdot T_{n} + 1 = {(2 \cdot n + 1)}^{2}

T_{m}^{- 1} = ?

Pairing function. Define the modified Cantor pairing function $⟨ x, y ⟩$ .

⟨ x, y ⟩ = ?

Basic properties of the pairing function. We have

⟨ x_{1}, x_{2} ⟩ = ⟨ y_{1}, y_{2} ⟩ \to x_{1} = y_{1} \land x_{2} = y_{2}

x < ⟨ x, y ⟩ \land y < ⟨ x, y ⟩

x = 0 \lor \exists y \exists z x = ⟨ y, z ⟩

Ordering properties of the pairing function. We have

⟨ x_{1}, x_{2} ⟩ ≦ ⟨ y_{1}, y_{2} ⟩ \leftrightarrow x_{1} + x_{2} < y_{1} + y_{2} \lor x_{1} + x_{2} = y_{1} + y_{2} \land x_{1} ≦ y_{1}

⟨ x_{1}, x_{2} ⟩ < ⟨ y_{1}, y_{2} ⟩ \leftrightarrow x_{1} + x_{2} < y_{1} + y_{2} \lor x_{1} + x_{2} = y_{1} + y_{2} \land x_{1} < y_{1}

Diagonal function. Define the unary function $d (x)$ such that

d ⟨ x, y ⟩ = x + y

d (x) = ?

Projections. Define the projection functions of the pairing function which are unary functions $π_{1} (x)$ and $π_{2} (x)$ such that

π_{1} (x) = y \leftrightarrow x = 0 \land y = 0 \lor \exists z x = ⟨ y, z ⟩

π_{2} (x) = z \leftrightarrow x = 0 \land z = 0 \lor \exists y x = ⟨ y, z ⟩

π_{1} (x) = ?

π_{2} (x) = ?

Exercise. Define the unary iteration $π_{2}^{n} (x)$ of the second projection function.

π_{2}^{n} (x) = ?

Exercise. (2 points) Find a primitive recursive definition of the following function

Twofib (n) = ⟨ {fib}_{n}, {fib}_{n + 1} ⟩

which does not contain any application of ${fib}_{n}$ .

Twofib (n) = ?

Section. Tuples.

Arithmetization of tuples. Define the binary predicate $Tuple (n, x)$ holding if the number $x$ is the code of an $n$ -tuple. Note that this includes the case when $n = 0$ or $n = 1$ . Find an explicit definition of the predicate!

Tuple (n, x) \leftrightarrow ?

Projection function for tuples. (1 point) Define the ternary function ${[x]}_{i}^{n}$ which generalizes the projection functions $π_{1} (x)$ and $π_{2} (x)$ to accept tuples, i.e. the application ${[x]}_{i}^{n}$ yields the $i$ -th element of the $n$ -tuple $x$ provided $1 ≦ i \land i ≦ n$ .

{[x]}_{i}^{n} = ?