Clausal Language (ver. 5.81.21, 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. 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

[CL] Structural case analysis on binary trees. Syntax:

case Bt ; <term>

Example(s):

$case Bt; t$
$\frac{Bt (t)}{t = • ∣ t = \frac{x}{l ∣ r} \land Bt (l) \land Bt (r)}$
where $x$ , $l$ and $r$ are new variables (eigen-variables).

Structural induction on binary trees. (1 point) Show that the principle of structural induction over binary trees is admissible in Peano arithmetic.

Remark. Prove the claim for the special case in the following theory.

[CL] Hint. Reduce structural induction on $t$ to course of values induction with measure $| t |_{p}$ . Recall that the pair size function $| x |_{p}$ , written as |x|, is defined in the module Standard.

φ [•]

φ [l] \land φ [r] \to φ [\frac{x}{l ∣ r}]

Bt (t) \to φ [t]

[CL] Structural induction on binary trees. Syntax:

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

where the induction formula is formed from the current sequent.

Example(s):

$ind Bt; t$
$\frac{Bt (t) \to φ [t] *}{φ [•] * ∣ φ [l] \land φ [r] \to φ [\frac{x}{l ∣ r}] *}$
where $x$ , $l$ and $r$ are new variables (eigen-variables).
$ind Bt; t; a$
$\frac{Bt (t) \to φ [t] *}{φ [•] * ∣ \forall a φ [l] \land \forall a φ [r] \to φ [\frac{x}{l ∣ r}] *}$
where $x$ , $l$ and $r$ are new variables (eigen-variables).

[CL] Structural induction on binary trees (2nd form). Syntax:

ind* Bt ; <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$ind* Bt; t$
$\frac{Bt (t) \to φ [t] *}{φ [•] * ∣ Bt (l) \land φ [l] \land Bt (r) \land φ [r] \to φ [\frac{x}{l ∣ r}] *}$
where $x$ , $l$ and $r$ are new variables (eigen-variables).
$ind* Bt; t; a$
$\frac{Bt (t) \to φ [t] *}{φ [•] * ∣ Bt (l) \land \forall a φ [l] \land Bt (r) \land \forall a φ [r] \to φ [\frac{x}{l ∣ r}] *}$
where $x$ , $l$ and $r$ are new variables (eigen-variables).

Subsection. Basic Operations and Predicates.

Size and depth of binary trees.

∣ • ∣ = 0

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

d (•) = 0

d (\frac{x}{l ∣ r}) = \max (d (l), d (r)) + 1

Exercise. Prove

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

[CL] Hint. In the proof you will need the following simple properties of the maximum function:

\max (x, y) ≦ z \leftrightarrow x ≦ z \land y ≦ z

Max_le

\max (x, y) ≧ x \land \max (x, y) ≧ y

Spec_max_ge

2^{\max (x, y)} = \max (2^{x}, 2^{y})

Exp2_max

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

Membership in binary trees.

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

Exercise. Prove

\neg x \in •

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

\neg x \in •

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

Counting the labels in binary trees.

#_{x} (•) = 0

#_{x} (\frac{y}{l ∣ r}) = #_{x} (l) + #_{x} (r) + (x =_{*} y)

Reflection function.

Reflect (•) = •

Reflect (\frac{x}{l ∣ r}) = \frac{x}{Reflect (r) ∣ Reflect (l)}

Exercise. Prove

Bt (t) \to Bt Reflect (t)

Bt (t) \to ∣ Reflect (t) ∣ = ∣ t ∣

Bt (t) \to d Reflect (t) = d (t)

Bt (t) \to x \in Reflect (t) \leftrightarrow x \in t

Bt (t) \to #_{x} Reflect (t) = #_{x} (t)

Bt (t) \to Reflect Reflect (t) = t

Bt (t_{1}) \land Bt (t_{2}) \land Reflect (t_{1}) = Reflect (t_{2}) \to t_{1} = t_{2}

Bt (t_{1}) \to \exists t_{2} Reflect (t_{2}) = t_{1}

Bt (t) \to Bt Reflect (t)

Bt (t) \to ∣ Reflect (t) ∣ = ∣ t ∣

Bt (t) \to d Reflect (t) = d (t)

Bt (t) \to x \in Reflect (t) \leftrightarrow x \in t

Bt (t) \to #_{x} Reflect (t) = #_{x} (t)

Bt (t) \to Reflect Reflect (t) = t

Bt (t_{1}) \land Bt (t_{2}) \land Reflect (t_{1}) = Reflect (t_{2}) \to t_{1} = t_{2}

Bt (t_{1}) \to \exists t_{2} Reflect (t_{2}) = t_{1}

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)

Exercise. Prove

Bt (t) \to Preorder (t) = Rev Postorder Reflect (t)

Bt (t) \to Postorder (t) = Rev Preorder Reflect (t)

Bt (t) \to Preorder (t) = Rev Postorder Reflect (t)

Bt (t) \to Postorder (t) = Rev Preorder Reflect (t)

Fast programs for tree traversals.

Case: preorder traversal.

f (•, a) = a

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

Exercise. (1 point) Prove

Bt (t) \to Preorder (t) = f (t, 0)

Bt (t) \to Preorder (t) = f (t, 0)

Case: inorder traversal.

Exercise. Save the concatenation in the definition of the function $Inorder (t)$ with help of an accumulator function and verify your implementation.

Case: postorder traversal.

Exercise. Save the concatenation in the definition of the function $Postorder (t)$ with help of an accumulator function and verify your implementation.

Subsection. Perfect Binary Trees.

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

∣ t ∣ + 1 = 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 (n, x) = ?

Bt f (n, x)

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

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

Exercise. (3 points) 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)

[CL] Hint. In the proof you will need the following property of exponentiation

2^{x} \neq 0

Exp2_is_not_zero

from the module Maux*.

g (n, m) = ?

f (n) = ?

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)

Bt f (n)

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

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

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)

f (n) = ?

Bt f (n)

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

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

Exercise. 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)

f (n) = ?

Bt f (n)

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

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

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.

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}

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

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

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

Verify your implementation!

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 ∣)

Implementation.

g (t, m) = ?

f (t) = ?

Verification.

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

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

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

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

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

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

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

Verify your implementation!

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

Implementation.

f (t) = ?

Verification.

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

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

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

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

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

Verify your implementation!

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

Implementation.

f (t) = ?

Verification.

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

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

Subsection. Flattened Trees.

Flattened (•)

Flattened (\frac{x}{l ∣ •}) \leftarrow Flattened (l)

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

Bt (t) \to Flattened Flatten (t)

Bt (t) \to #_{x} Flatten (t) = #_{x} (t)

Do not use auxiliary functions!

Flatten (t) = ?

Remark. Prove the conditions of regularity for a suitable measure $μ [t]$ .

μ [t] = ?

Exercise. (bonus 2 points) Prove that the function satisfies the required properties.

Bt (t) \to Flattened Flatten (t)

Bt (t) \to #_{x} Flatten (t) = #_{x} (t)