卒研発表合宿0228pptx 最近の更新履歴 神奈川大学 木下佳樹研究室

二分探索木基本操作の実装

とその正当性検証

神奈川大学 理学部情報科学科　木下研究室 201303273 _樊豪

やったこと

①二分探索木のデータ型と基本操作を定

義した

②要請を決めた

③要請される基本的な性質を与えた

④基本的な性質を満足することを証明し

た

二分探索木のデータ型

定義（集合）

二分木

 _ならば

定義（述語）

 _ならば

 _{で，ならば}

  

二分探索木のデータ型

定義（述語）

 _ならば

 _{で，ならば}

定義（述語 BST ）

二分探索木

 _{は成り立つ．}

 _{で , ならば}

  

定義（述語 member ）

① l ∈ Tree,n ∈ N,r ∈ Tree ならば member n [l,n,r]

② m ∈ N,l ∈ Tree,n ∈ N,r∈ Tree で member m l な

らば member m [l,n,r]

③ m ∈ N,l ∈Tree,n ∈N,r ∈Tree で member m r な

らば member m [l,n,r]

基本操作① insert

insert n t は t に n を付け加えたものである．

  

基本操作② delete

が与えられた自然数を与えられた木から削除する関数

  

のように定義される． は定義されない．

.

基本操作への要請

要請（ insert 挿入）

 が与えられた自然数を与えられた二分探索木に挿入すること が要請される．

要請（ insert 保存）

 は与えられた二分探索木に属している自然数を取り除かない ことが要請される．

要請（ delete 削除）

 が与えられた自然数を与えられた木から削除することが要請 される．

要請（ delete 保存）

 は，与えられた自然数以外の自然数は，与えられた木から 取り除かないことが要請される．

  

基本的な補題

①任意の自然数 n と任意の木 t に対して， member n (insert n t) _{が成り立つ．}

②任意の自然数 m ， n と任意の木 t に対して， member m t ならばが成り立つ．

③任意の自然数 m と任意の木 t に対して，であれば , が成り立 つ．

④任意の自然数 m ， n と任意の木 t に対して， m∈t しかも m≠n ならば m∈delete n t が成り立つ．

  

木の構造に関する帰納法の原理

定義（ Tree に関する構造帰納法）

木の構造に関する帰納法の原理とは，を木に関する述語

とする時

が成り立つことを主張する原理である．

この原理によると，の証明との証明から，の証明が得ら

れる．

  

基本操作の正当性検証　例

を証明するには木の構造に関する帰納法の原理による

と

①を証明すれば良い .

  

帰納法に基づく証明の例

1. が証明される .(member の定義により ) 2. (insert _{の定義により )}

3. 1. においてをで置き換えて ,① の証明が得られる .

次に

② を証明する . を仮定する .

…

  

難点について

任意の自然数 m ， n と任意の木 t に対して， m∈t しかも m≠n ならば m∈delete n t _{が成り立つ .}

を証明する . を適用すると

を任意の木とし , を任意の自然数とする．

 _{を証明する}

の二つと仮定する。

  

難点について

を仮定する上で 3. を証明する

の真偽によっていくつの場合に分けます

必須条件が n 個の場合 , 木の構造に関する帰納法による証明は , 最大場合は種になる .

  

問題点

 性質の証明が得られるとはいえ , 必ず基本操作の正当性が妥当とは言えません ^. 例えば delete を以下のように定義すると

の削除という性質の証明が得られますが , 得られません .

 適切な性質を見つかること .

 基本操作の要請された性質をすべて証明するのは難しい .

  

補題に関する話し

補題 2

 任意の自然数と任意の木に対してしかもならばである .

補題 4

 任意の自然数と任意の木に対してならばである .

  

補題に関する話し

補題 6

 任意の自然数と任意の木に対して , 及びであればである .

補題 8

 任意の自然数と任意の木に対して , ならばである .

  

補題に関する話し

補題 9

 任意の自然数と任意の木に対して , はある .

補題 10

 任意の木に対して , ある .

  

まとめ

①データ型と基本操作を定義した

②要請を決めた

③要請される基本的な性質を与えた

④基本的な性質を満足することを証明し

た

参考文献

i. haskell.org, Haskell home page, https://www.haskell.org/

ii. Graham Hutton, 山本和彦 ( 訳 ), プログラミング Haskell, オーム 社 ,ISBN:978-4-274-06781-5,2009.

iii. R. セジウィック ( 著 ), 野下浩平 / 星守 / 佐藤創 / 田口東 ( 共訳 ), アルゴ リズム C(Algorithms in C), 近代科学社 ,ISBN:4-7649-0256-7

ご清聴ありがとうございました。