Inductive Definitions

  • 0
    いいね
  • 0
    コメント
    この記事は最終更新日から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)}