プログラミング Haskell 第13章 プログラムの論証 練習問題 その4

最終章「プログラムの論証」の練習問題です。ついに最後です。

• 9.

 以下の型が与えられているとする
data Tree = Leaf Int | Node Tree Tree

この木の葉の個数は、節の個数よりも、常に1多いことを示す

まず葉の個数を数える関数 countLeaf と、節の個数を数える関数 countNode を定義する

countLeaf :: Tree -> Int
countLeaf (Leaf _) = 1
countLeaf (Node l r) = (countLeaf l) + (contLeaf r)

countNode :: Tree -> Int
countNode (Leaf _) = 0
countNode (Node l r) = (countNode l) + (countNode r) + 1

この時任意の Tree t について
countLeaf t = 1 + countNode t
が成り立つことを示せばよい。

t = Leaf n の時
(左辺)
=> countLeaf (Leaf n)
=> 1                    -- countLeaf の定義より

(右辺)
=> 1 + countNode (Leaf n)
=> 1 + 0                -- countNode の定義より
=> 1

t = Node l r の時
countLeaf l = 1 + countNode l
countLeaf r = 1 + countNode r
は成り立つと仮定する

(左辺)
=> countLeaf (Node l r)
=> (countLeaf l) + (countLeaf r)
=> (1 + countNode l) + (countLeaf r)     -- l についての仮定より
=> (1 + countNode l) + (1 + countNode r) -- r についての仮定より
=> 1 + ((countNode l) + (countNode r) + 1) -- 分配則より
=> 1 + countNode (Node l r)              -- countNode の定義を逆に適用
= (右辺)

よって任意の Tree t について葉の数は常に節の数+1になる

• 10. comp' e c = comp e ++ c を満たすような comp' の定義が欲しい

(本文で定義されている comp とそれに関連する型の定義)
  data Expr = Val Int | Add Expr Expr
  data Op = PUSH Int | ADD
  type Code = [Op]

  comp :: Expr -> Code
  comp (Val n) = [PUSH n]
  comp (Add x y) = comp x ++ comp y ++ [ADD]

e = Val n の時
(右辺)
comp (Val n) ++ c
=> [ PUSH n ] ++ c
=> (PUSH n) : c

e = Add l r の時
(右辺)
comp (Add l r) ++ c
=> comp l ++ comp r ++ [ADD] ++ c
=> comp l ++ comp r ++ (ADD:c)
=> comp l ++ (comp' r (ADD:c))
=> comp' l (comp' r (ADD:c))

よって以下の定義を得る
comp' :: Expr -> Code -> Code
comp' (Val n) c = (PUSH n) : c
comp' (Add l r) c = comp' l (comp' r (ADD:c))

ついに「プログラミング Haskell」の本文も終わりました。あとは付録を読んで終了です。
次に読むのは「プログラミングコンテストチャレンジブック」にしようかなと思ってます。