# Inductive Definitions

• 0
いいね
• 0
コメント
に更新
3
この記事は最終更新日から1年以上が経過しています。

Exercises of PFPL, 2nd Edition

# 2.1

Definition of judgment $max(m;n;p)$


\frac {a = b nat} { a \geq b nat } . Rule 1\\
\frac { a \geq b nat } { succ(a) \geq b nat } . Rule 2\\
\frac { a \geq b nat } { max(a;b;a) } . Rule 3\\
\frac { b \geq a nat } { max(a;b;b) } . Rule 4



Proof of mode $(\forall, \forall, \exists)$

1. For $\forall a \space nat, \forall b \space nat$, either $a \geq b$ or $b \geq a$

Proof:

Some easy to prove Theorem:

1. $\forall b \space nat , b \geq zero$. - Theorem 1
2. $\forall a \space nat, b \space nat, if a \geq b, then succ(a) \geq b$. -Theorem 2

If a nat and b nat, then there exists c nat such that max(a;b;c)
Define P1(a nat) as for $\forall b \space nat$ , either $a \geq b$ or $b \geq a$

• P1(zero nat) since easy to prove that $\forall b, b \geq zero$.
• Suppose P(a nat). We need to prove P1(succ(a) nat).
• If $a \geq b$ , then $succ(a) \geq b$ according to Rule 2
• If $b \geq a$
• If $b = a$, then $succ(a) \geq b$ according to Rule 2
• Otherwise, according to necessity, we have $b' \geq a, succ(b') = b$. Easy to prove that, $if a \geq b, then succ(a) \geq b$. So we have $succ(b') \geq succ(a)$. Or $b \geq succ(a)$.

According to P1(a nat), we have
- If $a \geq b$, then max(a;b;c) with c = a, exist and unique
- If $b \geq a$, then max(a;b;c) with c = b, exist and unique

# 2.2

## Existence

• hgt(empty; zero) by Rule (2.11 a). So exist height zero for empty tree
• Suppose hgt(t1; n1), hgt(t2; n2). Then for tree node(t1; t2), exist succ(n) with max(n1;n2;n) according to Rule (2.11 b)

## Uniqueness

• hgt(empty; zero). So for empty tree, height is unique (always zero)
• Suppose tree t3 being node(t1; t2), hgt(t1; n1), hgt(t2; n2) and n1, n2 is unique. max(n1;n2;n). According to necessity of Rule 2.11b, if hgt(t3; n3), with succ(n') = n3, then max(n1;n2;n'). max is unique, so n = n' nat. Therefore, n3 = succ(n) nat. And the height is unique.

# 2.3

\frac {}{Empty \space Tree} \\
\frac {b \space Forest} { node(b) \space Tree} \\
\frac {}{Empty \space Forest} \\
\frac {a \space Tree, b \space Forest}{ cons(a; b) \space Forest}


# 2.4

$hgt_t$ is the height of tree. $hgt_f$ is the height of forest


\frac {} {hgt_t(Empty \space Tree; zero) } \\
\frac {hgt_f(f \space Forest; n) } {succ(hgt_t(node(f) \space Tree))} \\

\frac {} {hgt_f(Empty \space Forest; zero)} \\
\frac {hgt_t(t \space Tree; n1), hgt_f(f \space Forest; n2), max(n1,n2,n)} {hgt_f(cons(t;f) \space Forest) ; succ(n)}



The proof of existence and uniqueness is simple and almost the same as previous questions.

# 2.5

bnat : binary natural number



\frac {} {zero \space bnat} \\
\frac {a \space bnat } {twice(a) \space bnat } \\
\frac {a \space bnat } {twicePlusOne(a) \space bnat }



What does "the size of the representation is logarithmic, rather than linear, in the natural number it represents"

# 2.6


\frac {} {succ(zero; twicePlusOne(zero)} \\
\frac {twice(a;b)} {succ(b; twicePlusOne(a)} \\
\frac {twicePlusOne(a;b)} {succ(b; twice(succ(a))} \\

\frac {} {sum(zero; b; b) } \\
\frac {sum(a;b;c)} {sum(a;succ(b); succ(c)}