連結リストでの例

ウィキペディア小見出し辞書

連結リストでの例

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/16 02:01 UTC 版)

「構造的帰納法」の記事における「連結リストでの例」の解説

より形式的な例を挙げる。次のようなリストの性質を考える。 length (L ++ M) = length L + length M [EQ] ここで L と M はリストであり、演算子 ++ はリストの連結を表している。 これを証明するには、length と ++ の定義が必要である。 length [] = 0 [LEN1] length (h:t) = 1 + length t [LEN2] [] ++ list = list [APP1] (h:t) ++ list = h : (t ++ list) [APP2] ここで (h:t) は、最初の要素が h で、残りの要素がリスト t で表されるようなリストを表す。[] は空のリストを表す。 いま示そうとしているリストの性質 P(L) は、「すべてのリスト M に対して、上述の等式 EQ が成り立つ」ことである。リストに関する構造的帰納法によって、∀L. P(L) を証明する。 まず P([]) が真であることを示そう。つまり、L = [] であるときに、すべてのリスト M に関して EQ が成り立つことだ。これは次の等式で証明される。 length (L ++ M) = length ([] ++ M) (仮定 L = [] より) = length M (APP1 より) = 0 + length M = length [] + length M (LEN1 より) = length L + length M 次に、すべての 空でない リスト I を考える。I は空でないから、先頭の要素を持つ。それを x とし、残りの要素からなるリストを xs とする。(これは I = x:xs と表せる。) ここでの帰納法の仮定は、すべてのリスト M に対して次の等式 (EQ の L = xs の場合) が成り立つことである。 length (xs ++ M) = length xs + length M (帰納法の仮定) このとき、P(I)、すなわちすべてのリスト M に対して EQ (の L = I の場合) が成り立つことを示したい。先ほどと同様に計算する。 length L + length M = length (x:xs) + length M = 1 + length xs + length M (LEN2 より) = 1 + length (xs ++ M) (帰納法の仮定より) = length (x: (xs ++ M)) (LEN2 より) = length ((x:xs) ++ M) (APP2 より) = length (L ++ M) したがって、構造的帰納法により、すべてのリスト L に対して P(L) が真であることが示された。すなわち、すべてのリスト L と M に対して EQ が真である。