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) $
- For $ \forall a \space nat, \forall b \space nat $, either $ a \geq b $ or $ b \geq a $
Proof:
Some easy to prove Theorem:
- $ \forall b \space nat , b \geq zero $. - Theorem 1
- $ \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)}