Agda: Как вывести доказательство _≤_ (или как реализовать двоичное дерево поиска)

Я, вероятно, не буду подходить к этому наилучшим образом, поскольку Agda и, в частности, стандартная библиотека Agda все еще для меня в новинку. Я пытаюсь реализовать понятие двоичных деревьев поиска.

У меня есть простое определение двоичного дерева

data BTree (A : Set) : ℕ → Set where
  Leaf : A → BTree A 1
  Node : ∀ {n m} → A → BTree A n → BTree A m → BTree A (1 + n + m)

а также две функции bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ и bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ, которые извлекают максимальное и минимальное значения из двоичного дерева.

Теперь я пытаюсь определить тип данных, который доказывает, что конкретное дерево является двоичным деревом поиска. Вот что у меня есть на данный момент.

data BST : {n : ℕ} → BTree ℕ n → Set where
  sortL : {x : ℕ} → BST (Leaf x)
  sortN : ∀ {n m} → {a : ℕ} → {l : BTree ℕ n} → {r : BTree ℕ m}
                            → (sl : BST l) → (sr : BST r)
                            → {cl : a ≥ (bt-⊔ l)} → {cr : a < (bt-⊓ r)}
                            → BST (Node a l r)

Моя интуиция для конструктора узла BST состоит в том, чтобы взять значение, хранящееся в узле (a), двух поддеревьях (l и r), доказать, что два поддерева являются BST (sl и sr), и доказать, что текущее значение a больше чем все в левом поддереве и меньше всего в правом (cl и cr).

Кажется, это более или менее работает, и я могу построить следующее простое дерево и доказательство BST.

T₂ : BTree ℕ 3
T₂ = Node 5 (Leaf 3) (Leaf 7)

bst₂ : BST T₂
bst₂ = sortN sortL sortL {s≤s (s≤s (s≤s z≤n))} {s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))}

Однако я хочу, чтобы Агда сделала вывод о доказательствах для cl и cr, поскольку они чрезвычайно утомительны. Если я не укажу их в определении bst₂, тогда Agda, похоже, подумает, что у меня есть дыры в моем коде, давая мне переменные подчеркивания, связанные с cl и cr.

Мне непонятно, как это сделать, и не совсем понятно, правильно ли я использую эту часть стандартной библиотеки. Я открыт для любых предложений или решений, которые упростят эту задачу.


dependent-type agda
person Karl    schedule 13.04.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Отношение «меньше или равно» можно определить как функцию:

open import Data.Empty
open import Data.Unit.Base using (⊤; tt)
open import Data.Nat.Base

_≤⊤_ : ℕ -> ℕ -> Set
0     ≤⊤ m     = ⊤
suc n ≤⊤ 0     = ⊥
suc n ≤⊤ suc m = n ≤⊤ m

test : 10 ≤⊤ 20
test = tt

А также возможно овеществление оригинальных доказательств:

≤⊤→≤ : ∀ n m -> n ≤⊤ m -> n ≤ m
≤⊤→≤  0       m      _  = z≤n
≤⊤→≤ (suc n)  0      ()
≤⊤→≤ (suc n) (suc m) p  = s≤s (≤⊤→≤ n m p)

test-test : 10 ≤ 20
test-test = ≤⊤→≤ _ _ test

test-test оценивается как s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))).

а также две функции bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ и bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ, которые извлекают максимальное и минимальное значения из двоичного дерева.

Их лучше хранить, чем извлекать. Ознакомьтесь с докладом Как держать своих соседей в порядке, который подробные сведения объясняют, как определять упорядоченные типы данных (код в документе не проверяет типы в последних версиях Agda, см. некоторые советы здесь).

Однако я хочу, чтобы Агда сделала вывод о доказательствах для cl и cr, поскольку они чрезвычайно утомительны.

Эти sortN и sortL тоже утомительны. Должна быть возможность определить

open import Relation.Nullary

ordered? : ∀ {n} -> (b : BTree ℕ n) -> Dec (BST b)
ordered? = ...

ordered? решает, упорядочено дерево или нет. Затем вы можете устранить это Dec с помощью Relation.Nullary.Decidable.from-yes. Но сначала прочтите статью и выберите более подходящее представление BST.

person user3237465    schedule 13.04.2016
comment
Спасибо за общий совет и ссылку на эту статью. Это должно, как минимум, дать мне гораздо больше возможностей попробовать. - person Karl; 13.04.2016