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.

Chapter. Programs Operating on Trees.

Section. Binary Trees.

Subsection. Arithmetization of Binary Trees.

Constructors of binary trees.

• = 0, 0

\frac{x}{l ∣ r} = 1, x, l, r

[CL] Discrimination on the constructors of binary trees. Example(s):

f (•) = ?

f (\frac{x}{l ∣ r}) = ?

Binary trees.

Bt (•)

Bt (\frac{x}{l ∣ r}) \leftarrow N (x) \land Bt (l) \land Bt (r)

[CL] Formatting the output. Use the format $Bt$ to display numbers as binary trees. Try out the following simple queries

    171386336145149 = t:Bt

    1,10,(1,11,(0,0),0,0),(1,12,(0,0),0,0) = t:Bt

Subsection. Basic Operations and Predicates.

Size and depth of binary trees. Define the functions $∣ t ∣$ and $d (t)$ computing respectively the size and the depth of the binary tree $t$ . Note that we have

Bt (t) \to d (t) ≦ ∣ t ∣ \land ∣ t ∣ < 2^{d (t)}

∣ • ∣ = 0

∣ \frac{x}{l ∣ r} ∣ = ∣ l ∣ + ∣ r ∣ + 1

d (•) = ?

d (\frac{x}{l ∣ r}) = ?

Reflection function. Define the function $Reflect (t)$ which yields the mirror's image of the binary tree $t$ .

Reflect (t) = ?

Membership in binary trees. Define the predicate $x \in t$ such that

\neg x \in •

x \in \frac{y}{l ∣ r} \leftrightarrow x = y \lor x \in l \lor x \in r

x \in \frac{y}{l ∣ r} \leftarrow x = y

x \in \frac{y}{l ∣ r} \leftarrow x \neq y \land x \in l

x \in \frac{y}{l ∣ r} \leftarrow x \neq y \land \neg x \in l \land x \in r

Isomorphic binary trees. Given binary trees $t_{1}$ and $t_{2}$ , the predicate $t_{1} ≃ t_{2}$ holds if the trees $t_{1}$ and $t_{2}$ are isomorphic (of the same shape).

• ≃ •

\frac{x_{1}}{l_{1} ∣ r_{1}} ≃ \frac{x_{2}}{l_{2} ∣ r_{2}} \leftarrow l_{1} ≃ l_{2} \land r_{1} ≃ r_{2}

We have

Bt (t) \to t ≃ t

t_{1} ≃ t_{2} \to t_{2} ≃ t_{1}

t_{1} ≃ t_{2} \land t_{2} ≃ t_{3} \to t_{1} ≃ t_{3}

Bt (t_{1}) \land t_{1} ≃ t_{2} \to Bt (t_{2})

t_{1} ≃ t_{2} \to ∣ t_{1} ∣ = ∣ t_{2} ∣

t_{1} ≃ t_{2} \to d (t_{1}) = d (t_{2})

Subsection. Traversals of Binary Trees.

Basic traversals of binary trees.

Preorder (•) = 0

Preorder (\frac{x}{l ∣ r}) = (x, 0) \oplus Preorder (l) \oplus Preorder (r)

Inorder (•) = 0

Inorder (\frac{x}{l ∣ r}) = Inorder (l) \oplus (x, 0) \oplus Inorder (r)

Postorder (•) = 0

Postorder (\frac{x}{l ∣ r}) = Postorder (l) \oplus Postorder (r) \oplus (x, 0)

Fast programs for tree traversals. Save the concatenation in the definition of each tree traversal function.

Case: preorder traversal.

f (•, as) = as

f (\frac{x}{l ∣ r}, as) = x, f (l, f (r, as))

Invariant:

Bt (t) \to f (t, as) = Preorder (t) \oplus as

Preorder (t) = f (t, 0)

Case: inorder traversal.

f (•, as) = ?

f (\frac{x}{l ∣ r}, as) = ?

Invariant:

Bt (t) \to f (t, as) = Inorder (t) \oplus as

Inorder (t) = ?

Case: postorder traversal. (1 point)

f (t, as) = ?

Invariant:

Bt (t) \to f (t, as) = Postorder (t) \oplus as

Postorder (t) = ?

Subsection. Perfect Binary Trees.

Perfect binary trees. A binary tree $t$ is said to be perfect if

∣ t ∣ + 1 = {Exp}_{2} d (t)

Exercise. Define the function $f (n, x)$ such that

Bt f (n, x)

d f (n, x) = n \land ∣ f (n, x) ∣ + 1 = 2^{n}

y \in f (n, x) \to y = x

f (0, x) = •

f (n + 1, x) = \frac{x}{f (n, x) ∣ f (n, x)}

Exercise. Define the function $f (n)$ such that

Bt f (n)

d f (n) = n \land ∣ f (n) ∣ + 1 = 2^{n}

Preorder f (n) = [0 .. 2^{n} \dot{-} 1)

Hint. Define first an auxiliary function $g (n, m)$ such that

Bt g (n, m)

d g (n, m) = n \land ∣ g (n, m) ∣ + 1 = 2^{n}

Preorder g (n, m) = [m .. m + 2^{n} \dot{-} 1)

g (0, m) = •

g (n + 1, m) = \frac{m}{g (n, m + 1) ∣ g (n, m + 2^{n})}

f (n) = g (n, 0)

Exercise. Define the function $f (n)$ such that

Bt f (n)

d f (n) = n \land ∣ f (n) ∣ + 1 = 2^{n}

Inorder f (n) = [0 .. 2^{n} \dot{-} 1)

g (0, m) = ?

g (n + 1, m) = ?

f (n) = ?

Exercise. (1 point) Define the function $f (n)$ such that

Bt f (n)

d f (n) = n \land ∣ f (n) ∣ + 1 = 2^{n}

Postorder f (n) = [0 .. 2^{n} \dot{-} 1)

g (n, m) = ?

f (n) = ?

Exercise. (1 bonus point) Define the function $f (n)$ which creates perfect binary tree $t$ of depth $n$ with values $0, 1, 2, 3, \dots$ stored in $t$ in breadth-first order. We have

Bt f (n)

d f (n) = n \land ∣ f (n) ∣ + 1 = 2^{n}

x \in f (n) \leftrightarrow x + 1 < 2^{n}

Hint. Define first an auxiliary function $g (n, m)$ such that

Bt g (n, m)

d g (n, m) = n \land ∣ g (n, m) ∣ + 1 = 2^{n}

x \in g (n, m) \leftrightarrow \exists y (x = m ⋆ y \land y + 1 < 2^{n})

Here the $x ⋆ y$ is dyadic concatenation.

g (0, m) = ?

g (n + 1, m) = ?

f (n) = ?

Subsection. Tree Numberings.

Problem. Given a tree, create a new tree of the same shape, but with the values at the nodes replaced by the numbers 0,1,2... in a fixed order.

Exercise. Define the function $f (t)$ such that

Bt (t) \to f (t) ≃ t

Bt (t) \to Preorder f (t) = [0 .. ∣ t ∣)

Remark. Implement the function with the help of the size function $∣ t ∣$ .

Hint. Define first an auxiliary function $g (t, m)$ such that

Bt (t) \to g (t, m) ≃ t

Bt (t) \to Preorder g (t, m) = [m .. m + ∣ t ∣)

g (•, m) = •

g (\frac{x}{l ∣ r}, m) = \frac{m}{g (l, m + 1) ∣ g (r, m + ∣ l ∣ + 1)}

f (t) = g (t, 0)

Exercise. Define the function $f (t)$ such that

Bt (t) \to f (t) ≃ t

Bt (t) \to Inorder f (t) = [0 .. ∣ t ∣)

Remark. Implement the function with the help of the size function $∣ t ∣$ .

g (•, m) = ?

g (\frac{x}{l ∣ r}, m) = ?

f (t) = ?

Exercise. (1 point) Define the function $f (t)$ such that

Bt (t) \to f (t) ≃ t

Bt (t) \to Postorder f (t) = [0 .. ∣ t ∣)

Remark. Implement the function with the help of the size function $∣ t ∣$ .

g (t, m) = ?

f (t) = ?