Как определить обход уровня дерева бинарного дерева в Изабель / Хол - PullRequest
Новая
       4

Как определить обход уровня дерева бинарного дерева в Изабель / Хол

0 голосов
/ 08 января 2020

Я написал обход уровня двоичного дерева в определениях других языков, но я не знаю, как представить обход уровня в isabelle / hol. Кто-нибудь определил это или как его определить?

1 Ответ

2 голосов
/ 08 января 2020

В принципе, вы можете сделать это точно так же, как в Haskell. Проблемный бит c состоит в том, что вам нужно доказать завершение рекурсивной вспомогательной функции (то, что называется tbf в коде Haskell, который вы связали). Самый простой способ показать это - найти на входе какой-то показатель (список деревьев), который уменьшается с каждым рекурсивным вызовом.

Я предлагаю следующую меру: суммировать размеры всех деревьев в списке, где размер - это число всех узлов в дереве (включая конечные узлы).

Мы можем использовать двоичные деревья из библиотеки HOL (HOL-Library.Tree). Сначала мы определим некоторые вспомогательные функции на деревьях, в том числе наши размерные функции, и докажем некоторые факты о них: 

primrec tree_values :: "'a tree ⇒ 'a list" where
  "tree_values Leaf = []"
| "tree_values (Node l x r) = [x]"

primrec tree_children :: "'a tree ⇒ 'a tree list" where
  "tree_children Leaf = []"
| "tree_children (Node l x r) = [l, r]"

primrec tree_size :: "'a tree ⇒ nat" where
  "tree_size Leaf = 1" 
| "tree_size (Node l x r) = tree_size l + tree_size r + 1"

definition tree_list_size :: "'a tree list ⇒ nat"
  where "tree_list_size = sum_list ∘ map tree_size"

lemma tree_size_pos: "tree_size t > 0"
  by (induction t) auto

lemma tree_size_nonzero [simp]: "tree_size t ≠ 0"
  by (simp add: tree_size_pos)

lemma tree_list_size_children [simp]:
  "tree_list_size (tree_children t) = tree_size t - 1"
  by (cases t) (auto simp: tree_list_size_def)

Далее нам понадобится еще одна простая лемма о sum_list и concat: 

lemma sum_list_concat: "sum_list (concat xs) =     sum_list (map sum_list xs)"
  by (induction xs) auto

Наконец, мы можем определить BFS и доказать его завершение: 

function bfs_aux :: "'a tree list ⇒ 'a list" where
  "bfs_aux ts =
     (if ts = [] then [] else concat (map tree_values ts) @ bfs_aux (concat (map tree_children ts)))"
  by auto
termination
proof (relation "measure tree_list_size")
  fix ts :: "'a tree list"
  assume ts: "ts ≠ []"
  have "tree_list_size (concat (map tree_children ts)) =
        sum_list (map (tree_list_size ∘ tree_children) ts)"
    by (simp add: map_concat sum_list_concat tree_list_size_def o_assoc)
  also from ‹ts ≠ []› have "… < sum_list (map tree_size ts)"
    by (intro sum_list_strict_mono) (auto simp: tree_size_pos)
  also have "… = tree_list_size ts"
    by (simp add: tree_list_size_def)
  finally show "(concat (map tree_children ts), ts) ∈ measure tree_list_size"
    by simp
qed auto

definition bfs :: "'a tree ⇒ 'a list"
  where "bfs t = bfs_aux [t]‹›

И мы можем проверить это: 

value "bfs (⟨⟨⟨Leaf, ''d'', Leaf⟩, ''b'', ⟨Leaf, ''e'', Leaf⟩⟩, ''a'', 
             ⟨⟨Leaf, ''f'', Leaf⟩, ''c'', ⟨Leaf, ''g'', Leaf⟩⟩⟩)"
> "[''a'', ''b'', ''c'', ''d'', ''e'', ''f'', ''g'']"
    :: "char list list"

Подробнее об определении функций с не- тривиальные шаблоны рекурсии, подобные этой и доказывающие их завершение, см. документацию пакета функций (в частности, раздел 4).

...