AVL树的成员资格证明 [英] Membership proofs for AVL trees

问题描述

我很努力地想出Data.AVL树的成员资格证明的概念.我希望能够传递n ∈ m类型的值，以表示n在AVL树中显示为键，因此，给出这样的证明，get n m总是可以成功产生与n相关的值.您可以假设我的AVL树始终包含从集合半格(A，≈)上的连接半格(A，∨，⊥)绘制的值，尽管下面的幂等性是隐式的.

I'm struggling a little to come up with a notion of membership proof for Data.AVL trees. I would like to be able to pass around a value of type n ∈ m, to mean that n appears as a key in in the AVL tree, so that given such a proof, get n m can always successfully yield a value associated with n. You can assume my AVL trees always contain values drawn from a join semilattice (A, ∨, ⊥) over a setoid (A, ≈), although below the idempotence is left implicit.

module Temp where

open import Algebra.FunctionProperties
open import Algebra.Structures renaming (IsCommutativeMonoid to IsCM)
open import Data.AVL
open import Data.List
open import Data.Nat hiding (_⊔_)
import Data.Nat.Properties as ℕ-Prop
open import Data.Product hiding (_-×-_)
open import Function
open import Level
open import Relation.Binary renaming (IsEquivalence to IsEq)
open import Relation.Binary.PropositionalEquality

module ℕ-AVL {v} (V : Set v)
  = Data.AVL (const V) (StrictTotalOrder.isStrictTotalOrder ℕ-Prop.strictTotalOrder)

data ≈-List {a ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) : Rel (List A) (a ⊔ ℓ) where
   [] : ≈-List _≈_ [] []
   _∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys)

_-×-_ : {a b c d ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
          REL A C ℓ₁ → REL B D ℓ₂ → A × B → C × D → Set (ℓ₁ ⊔ ℓ₂)
(R -×- S) (a , b) (c , d) = R a c × S b d

-- Two AVL trees are equal iff they have equal toList images.
≈-AVL : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (ℕ-AVL.Tree A) (a ⊔ ℓ)
≈-AVL _≈_ = ≈-List ( _≡_ -×- _≈_ ) on (ℕ-AVL.toList _)

_∈_ : {a ℓ : Level} {A : Set a} {_≈_ : Rel A ℓ} {_∨_ : Op₂ A} {⊥ : A}
      {{_ : IsCM _≈_ _∨_ ⊥}} → ℕ → ℕ-AVL.Tree A → Set (a ⊔ ℓ)
n ∈ m = {!!}

get : {a ℓ : Level} {A : Set a} {_≈_ : Rel A ℓ} {_∨_ : Op₂ A} {⊥ : A} →
      {{_ : IsCM _≈_ _∨_ ⊥}} → (n : ℕ) → (m : ℕ-AVL.Tree A) → n ∈ m → A
get n m n∈m = {!!}

我觉得这应该很容易，但是我发现很难.一种选择是将我的等价概念用于AVL树，即当两棵树具有相同的toList图像时，两棵树是相等的，并利用A上的交换对半定线来定义

I feel like this should be easy, but I'm finding it hard. One option would be to use my notion of equivalence for AVL-trees, which says that two trees are equal iff they have the same toList image, and exploit the commutative monoid over A, defining

n∈m =≈-AVL≈ m(ℕ-AVL.unionWith_ ∨ m(ℕ-AVL.singleton_ n⊥))

n ∈ m = ≈-AVL ≈ m (ℕ-AVL.unionWith _ ∨ m (ℕ-AVL.singleton _ n ⊥))

这实质上表示，当单例映射(n，⊥)在交换可分半模所诱导的部分顺序中位于m下方时，m包含n(从技术上讲，我们需要等幂才能使这种解释有意义).但是，给出这样的定义，我根本不确定如何实现get.

This essentially says that m contains n iff the singleton map (n, ⊥) is "below" m in the partial order induced by the commutative monoid (technically we need the idempotence for this interpretation to make sense). However given such a definition I'm not at all sure how to implement get.

我也尝试定义自己的归纳ε关系，但是发现我似乎很难了解Data.AVL所使用的复杂内部索引.

I have also experimented with defining my own inductive ∈ relation but found that hard as I seemed to end up having to know about the complicated internal indices used by Data.AVL.

最后，我还尝试使用类型为n ∈? m ≡ true的值，其中在Data.AVL中定义了∈?，但在那里也没有太大的成功.任何建议，我将不胜感激.

Finally I also tried using a value of type n ∈? m ≡ true, where ∈? is defined in Data.AVL, but didn't have much success there either. I would appreciate any suggestions.

推荐答案

我认为您最好的选择是将_∈_定义为归纳关系.是的，这需要您了解Data.AVL的内部原理，但是我敢肯定，这将是最令人愉快的表示形式.

I think your best bet is to define _∈_ as an inductive relation. Yes, this requires you to know the internals of Data.AVL, but I'm fairly sure this will be the most pleasant representation to work with.

Data.AVL的内部结构实际上非常简单.我们有一个Indexed.Tree类型，它由三个值索引:下限，上限和高度.给定一棵树t : Indexed.Tree lb ub h，t中的所有值都在(lb, ub)范围内.

The internal structure of Data.AVL is actually quite simple. We have a type Indexed.Tree, which is indexed by three values: the lower bound, the upper bound and the height. Given a tree t : Indexed.Tree lb ub h, all values inside t are within the range (lb, ub).

但是，有一点点曲折:由于我们需要有一棵可以包含任意值的树，因此我们需要用两个新值来人为地扩展isStrictTotalOrder给定的_<_关系-您可以想到那些作为负无穷大和正无穷大在Data.AVL模块中，它们分别称为⊥⁺和⊤⁺.这样，可以包含任意值的树的类型为Tree ⊥⁺ ⊤⁺ h.

There's a slight twist to it, though: since we need to have a tree that can contain arbitrary values, we need to artifically extend the _<_ relation given by isStrictTotalOrder with two new values - you can think of those as a negative and a positive infinity. In the Data.AVL module, these are called ⊥⁺ and ⊤⁺. Trees that can contain arbitrary values are then of type Tree ⊥⁺ ⊤⁺ h.

最后一个是平衡:每个节点要求其子树的高度相距最多一层.我们实际上不需要触摸平衡，但是功能签名可能会提到它.

The last piece is the balancing: each node requires heights of its subtrees to be at most one level apart. We don't actually need to touch balancing, but the function signatures might mention it.

无论如何，我直接使用此原始(索引)变体.不透明，未索引的版本类似于:

Anyways, I'm working directly with this raw (indexed) variant. The opaque, unindexed version is just something like:

data Tree : Set ? where
  tree : ∀ {h} → Indexed.Tree ⊥⁺ ⊤⁺ h

---

先介绍一些样板:

---

Some boilerplate first:

open import Data.Empty
open import Data.Product
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

import Data.AVL

module Membership
  {k v ℓ}
  {Key : Set k} (Value : Key → Set v)
  {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open Data.AVL Value isStrictTotalOrder public
open Extended-key                      public
open Height-invariants                 public

open IsStrictTotalOrder isStrictTotalOrder

这是_∈_的归纳关系:

data _∈_ {lb ub} (K : Key) :
    ∀ {n} → Indexed.Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
  here : ∀ {hˡ hʳ} V
    {l : Indexed.Tree lb [ K ] hˡ}
    {r : Indexed.Tree [ K ] ub hʳ}
    {b : hˡ ∼ hʳ} →
    K ∈ Indexed.node (K , V) l r b
  left : ∀ {hˡ hʳ K′} {V : Value K′}
    {l : Indexed.Tree lb [ K′ ] hˡ}
    {r : Indexed.Tree [ K′ ] ub hʳ}
    {b : hˡ ∼ hʳ} →
    K < K′ →
    K ∈ l →
    K ∈ Indexed.node (K′ , V) l r b
  right : ∀ {hˡ hʳ K′} {V : Value K′}
    {l : Indexed.Tree lb [ K′ ] hˡ}
    {r : Indexed.Tree [ K′ ] ub hʳ}
    {b : hˡ ∼ hʳ} →
    K′ < K →
    K ∈ r →
    K ∈ Indexed.node (K′ , V) l r b

这是您期望的归纳定义:键位于此内部节点中，或者位于子树之一中.我们也可以不使用小于，大于的证明，但这更加方便-当您想要显示树不包含特定元素时，您只需要跟踪路径即可lookup将代替搜索整个树.

This is the sort of inductive definition you'd expect: either the key is in this inner node or it's down in one of the subtrees. We could also do without the less-than, greater-than proofs, but this is more convenient - when you want to show that a tree does not contain a particular element, you only have to track the path lookup would take, instead of searching the whole tree.

如何解释那些l和r隐式参数?请注意，这是完全合理的:我们有一个键K，并且自然地我们要求l中包含的值落在lb和K之间(实际上是[ K ]，因为我们正在使用扩展的)，并且r中的值介于K和ub之间.平衡(b : hˡ ∼ hʳ)在那里，所以我们可以构造一个实际的树节点.

How to interpret those l and r implicit arguments? Notice that is makes perfect sense: we have a key K and naturally we require that the values contained in l fall between lb and K (it's actually [ K ], since we are using the extended _<_) and the values in r fall between K and ub. The balancing (b : hˡ ∼ hʳ) is there just so we can construct an actual tree node.

您的get函数非常简单:

get : ∀ {h lb ub n} {m : Indexed.Tree lb ub h} → n ∈ m → Value n
get (here    V) = V
get (left  _ p) = get p
get (right _ p) = get p

---

好吧，我告诉过您，使用此表示形式相当方便，我将对其进行证明.我们希望_∈_具有的属性之一是可判定性:即，我们可以构造一个程序来告诉我们元素是否在树中:

---

Well, I told you that this representation is fairly convenient to work it and I'm going to prove it. One of the properties we'd like _∈_ to have is decidability: that is, we can construct a program that tells us whether an element is in a tree or not:

find : ∀ {h lb ub} n (m : Indexed.Tree lb ub h) → Dec (n ∈ m)

find将返回yes p，其中p是n在m(n ∈ m)内部的证明，或者是no ¬p，其中¬p是对n ∈ m的引用. ，n ∈ m → ⊥.我们需要一个引理:

find will return either yes p, where p is a proof that n is inside m (n ∈ m), or no ¬p, where ¬p is refutation of n ∈ m, n ∈ m → ⊥. We'll need one lemma:

lem : ∀ {lb ub hˡ hʳ K′ n} {V : Value K′}
  {l : Indexed.Tree lb [ K′ ] hˡ}
  {r : Indexed.Tree [ K′ ] ub hʳ}
  {b : hˡ ∼ hʳ} →
  n ∈ Indexed.node (K′ , V) l r b →
  (n ≯ K′ → n ≢ K′ → n ∈ l) × (n ≮ K′ → n ≢ K′ → n ∈ r)
lem (here    V) =
  (λ _ eq → ⊥-elim (eq P.refl)) , (λ _ eq → ⊥-elim (eq P.refl))
lem (left  x p) = (λ _ _ → p) , (λ ≮ _ → ⊥-elim (≮ x))
lem (right x p) = (λ ≯ _ → ⊥-elim (≯ x)) , (λ _ _ → p)

这告诉我们，如果我们知道n包含在t中，并且我们知道n小于t的根的键，则n必须位于左子树中(并且右子树也是如此).

This tells us that if we know n is contained in t and we know n is less than the key of the root of t, then n must be in the left subtree (and similarly for right subtree).

这是find函数的实现:

find : ∀ {h lb ub} n (m : Indexed.Tree lb ub h) → Dec (n ∈ m)
find n (Indexed.leaf _) = no λ ()
find n (Indexed.node (k , v) l r _) with compare n k
find n (Indexed.node (k , v) l r _) | tri< a ¬b ¬c with find n l
... | yes p = yes (left a p)
... | no ¬p = no λ ¬∈l → ¬p (proj₁ (lem ¬∈l) ¬c ¬b)
find n (Indexed.node (k , v) l r _) | tri≈ ¬a b ¬c
  rewrite (P.sym b) = yes (here v)
find n (Indexed.node (k , v) l r _) | tri> ¬a ¬b c with find n r
... | yes p = yes (right c p)
... | no ¬p = no λ ¬∈r → ¬p (proj₂ (lem ¬∈r) ¬a ¬b)

实现非常简单，但是我建议将其加载到Emacs中，尝试用孔替换一些右侧并查看类型.最后，这是一些测试:

The implementation is fairly straightforward, but I would suggest loading it up in Emacs, trying to replace some of the right-hand-sides with holes and see what the types are. And finally, here are some tests:

open import Data.Nat
open import Data.Nat.Properties

open Membership
  (λ _ → ℕ)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

un-tree : Tree → ∃ λ h → Indexed.Tree ⊥⁺ ⊤⁺ h
un-tree (tree t) = , t

test : Indexed.Tree _ _ _
test = proj₂ (un-tree
  (insert 5 55 (insert 7 77 (insert 4 44 empty))))

Extract : ∀ {p} {P : Set p} → Dec P → Set _
Extract {P = P} (yes _) = P
Extract {P = P} (no  _) = ¬ P

extract : ∀ {p} {P : Set p} (d : Dec P) → Extract d
extract (yes p) = p
extract (no ¬p) = ¬p

∈-test₁ : ¬ (2 ∈ test)
∈-test₁ = extract (find 2 test)

∈-test₂ : 4 ∈ test
∈-test₂ = extract (find 4 test)

这篇关于AVL树的成员资格证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！