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

Literature.

Literature.

[1] J. Komara. Declarative Programming. Downloadable lecture notes available through the web page of the course.
[2] J. Kľuka. Lecture Notes from Introduction to Declarative Programming.
[3] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Beginning of Arithmetization.

Section. Pairing Functions.

Subsection. Catalan Pairing Function.

[CL] Syntax. The Catalan pairing function $x, y$ , written as $x,y$ , is pre-defined in CL.

Basic properties of Catalan 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 Catalan pairing function. We have

x_{1}, x_{2} < y_{1}, y_{2} \leftrightarrow | x_{1}, x_{2} |_{p} < | y_{1}, y_{2} |_{p} \lor | x_{1}, x_{2} |_{p} = | y_{1}, y_{2} |_{p} \land (x_{1} < y_{1} \lor x_{1} = y_{1} \land x_{2} < y_{2})

where $| x |_{p}$ is the pair size function defined in the module Standard.

[CL] Discrimination on pair patterns. Example(s):

f (0) = ?

f (v, w) = ?

f (0) = ?

f (u, 0) = ?

f (u, v, w) = ?

Subsubsection. Pair Representation of Numbers.

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 (x) = ?