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

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

[CL] CL-TeX.

Chapter. Beginning of Arithmetization.

Section. Pairing Functions.

Subsection. Catalan Pairing Function. See also in [2] the section Suitable Pairing Function in the chapter Recursive Bootstrapping of PA.

[CL] Pairing function. The following properties of the Catalan pairing function are built in into the CL theorem prover:

x_{1}, x_{2} = y_{1}, y_{2} \leftrightarrow x_{1} = y_{1} \land x_{2} = y_{2}

x, y = 0 \leftrightarrow ⊥

Moreover, we have

x = τ [x] \leftrightarrow ⊥

(occur_check)

for terms $τ [x]$ of the form

τ [x] \equiv x, y

τ [x] \equiv y, x

τ [x] \equiv (x, y_{1}), y_{2}

τ [x] \equiv (y_{1}, x), y_{2}

τ [x] \equiv y_{1}, x, y_{2}

τ [x] \equiv y_{1}, y_{2}, x

\dots

[CL] Pair case analysis. Syntax:

case P ; <term>

Example(s):

$case P; t$
$\frac{}{t = 0 ∣ t = v, w}$
where $v$ and $w$ are new variables (eigen-variables).

The predicate $P$ is defined in the module Standard.

[CL] Pair induction. Syntax:

ind P ; <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$ind P; x$
$\frac{φ [x] *}{φ [0] * ∣ φ [v] \land φ [w] \to φ [v, w] *}$
$ind P; x; a$
$\frac{φ [x] *}{φ [0] * ∣ \forall a φ [v] \land \forall a φ [w] \to φ [v, w] *}$

The predicate $P$ is defined in the module Standard.

[CL] Pair size. The pair size function $| x |_{p}$ is defined in the module Standard. The following its properties are built in into the CL theorem prover:

| 0 |_{p} = 0

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

| x |_{p} = 0 \leftrightarrow x = 0

| x |_{p} = 1 \leftrightarrow x = 0, 0

| x \oplus y |_{p} = | x |_{p} + | y |_{p}

Subsubsection. Projections.

Projection functions.

π_{1} (0) = 0

π_{1} (v, w) = v

π_{2} (0) = 0

π_{2} (v, w) = w

Iteration of the second projection.

π_{2}^{0} (x) = x

π_{2}^{n + 1} (x) = π_{2} π_{2}^{n} (x)

Exercise. Prove

π_{2}^{n} (0) = 0

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

π_{2}^{m + n} (x) = π_{2}^{m} π_{2}^{n} (x)

π_{2}^{n} (0) = 0

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

π_{2}^{m + n} (x) = π_{2}^{m} π_{2}^{n} (x)

Subsubsection. Tupling.

Exercise. 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}$ . Prove that the function satisfies the above property. Do not use auxiliary functions!

Twofib (n) = ?

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

Subsubsection. Pair Representation of Numbers.

Reflection function.

Reflect (0) = 0

Reflect (v, w) = Reflect (w), Reflect (v)

Exercise. Prove

Reflect (x) = 0 \leftrightarrow x = 0

| Reflect (x) |_{p} = | x |_{p}

Reflect Reflect (x) = x

Reflect (x) = Reflect (y) \to x = y

\exists y Reflect (y) = x

Reflect (x) = 0 \leftrightarrow x = 0

| Reflect (x) |_{p} = | x |_{p}

Reflect Reflect (x) = x

Reflect (x) = Reflect (y) \to x = y

\exists y Reflect (y) = x

Flattened trees.

Flattened (0)

Flattened (x, 0) \leftarrow Flattened (x)

Exercise. Define the function $Flatten (x)$ such that

| Flatten (x) |_{p} = | x |_{p}

Flattened Flatten (x)

Do not use auxiliary functions!

Flatten (0) = 0

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

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

| Flatten (x) |_{p} = | x |_{p}

Flattened Flatten (x)