Help us understand the problem. What is going on with this article?

# Inductive Definitions

More than 3 years have passed since last update.

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


Why not register and get more from Qiita?
1. We will deliver articles that match you
By following users and tags, you can catch up information on technical fields that you are interested in as a whole
2. you can read useful information later efficiently
By "stocking" the articles you like, you can search right away
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
1. We will deliver articles that match you
By following users and tags, you can catch up information on technical fields that you are interested in as a whole
2. you can read useful information later efficiently
By "stocking" the articles you like, you can search right away