Как определить эту древовидную структуру с зависимым типом в Coq? - PullRequest
Новая
       4

Как определить эту древовидную структуру с зависимым типом в Coq?

0 голосов
/ 05 октября 2018

Я хотел бы определить довольно простой вид дерева, но я не уверен, как это сделать.

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

Inductive nat_btree : Type :=
| leaf : nat -> nat_btree
| unary : nat_btree -> nat -> nat_btree
| binary : nat_btree -> nat_btree -> nat -> nat_btree.

Теперь я хотел бы определить тип данных, который мы будем называть special_nat_btree, который является nat_btree с условием, что каждый узел является либо:

  1. Узел со значением n и без дочерних элементов (т. Е. Листа)
  2. Узел со значением n + 1 и единственным потомком со значением n
  3. Узел со значением n ^ 2, ировно два ребенка, каждый со значением n

Так, например, мы могли бы иметь следующее: 

1
|
2     2   3
 \   /    |
   4      4
    \    /
      16
       |
      17

Но я действительно не знаю правильный синтаксис или даже лучший подходдля реализации этого в Coq.Сначала я хотел потребовать доказательства того, что «корневые значения» в поддереве (ах) соответствуют тому, что мы пытаемся построить.Так, например, приведенный выше «унарный» конструктор может выглядеть примерно так: 

unary : forall (t : special_nat_btree) (n : nat),
    special_nat_btree -> nat -> (n = S (root_val t)) -> 
    special_nat_btree

Помимо приведенного выше синтаксиса, возможно, уже неправильного, этот подход также требует определения функции «root_val», которая будет находиться во взаимной рекурсии сspecial_nat_btree.Заполнив мои рассуждения, я получаю следующее (это не скомпилируется): 

Inductive special_nat_btree : Type :=
  | leaf : nat -> special_nat_btree
  | unary : forall (t : special_nat_btree) (n : nat),
      special_nat_btree -> nat -> (n = S (root_val t)) -> 
      special_nat_btree
  | binary : forall (t_1 t_2 : special_nat_btree) (n : nat),
      special_nat_btree -> special_nat_btree -> nat ->
      (root_val t_1 = root_val t_2) ->
      (n = (root_val t_1) * (root_val t_1)) -> special_nat_btree
with
root_val (t : special_nat_btree) : nat :=
  match t with
  | leaf n => n
  | unary t' n p => n
  | binary t_1 t_2 n p_1 p_2 => n
  end.

И, э-э, я почти уверен, что схожу с пути.Так как я должен подойти к этому?Или, если мое мышление не совсем не так, каков правильный синтаксис для выполнения того, что я пытаюсь сделать?

1 Ответ

0 голосов
/ 05 октября 2018

Как насчет этого индексированного типа 

(* [btree n]: tree with root value [n]. *)
Inductive btree : nat -> Type :=
| leaf : forall n, btree n
| unary : forall n, btree n -> btree (S n)
| binary : forall n, btree n -> btree n -> btree (n * n)
.

Затем используйте сигму для представления деревьев неопределенного значения: 

Definition tree : Type := { n : nat & btree n }.

Например: 

Example foo : tree := existT _ _
  (unary _ (binary _ (binary _ (unary _ (leaf 1))
                               (leaf 2))
                     (unary _ (leaf 3)))).

_ в дереве на самом деле не значения узлов, которые вы описываете, но вместо этого фактические значения (n в btree n) вычисляются из содержимого этих полей (и поэтомуменее запутанно просто оставить их выше): unary x _ - это узел со значением x+1, а его дочерний элемент имеет значение x.

...