问题 如何在树和遍历之间建立​​双射？


我在看 inorder + preorder如何构造唯一的二叉树？ 并认为在伊德里斯写一个正式的证据会很有趣。不幸的是，我很早就陷入困境，试图证明在树中找到元素的方法对应于在顺序遍历中找到它的方法（当然，我还需要为前序遍历执行此操作） 。任何想法都会受到欢迎。我对完整的解决方案并不特别感兴趣 - 更多的是帮助我们开始正确的方向。

特定

data Tree a = Tip
            | Node (Tree a) a (Tree a)

我可以通过至少两种方式将其转换为列表：

inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r

要么

foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree c n r) l
inorder = foldrTree (::) []

第二种方法似乎很有用 一切 很难，所以我的大部分努力都集中在第一个方面。我在树中描述这样的位置：

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` Node l x r
  OnLeft : x `InTree` l -> x `InTree` Node l v r
  OnRight : x `InTree` r -> x `InTree` Node l v r

这很容易（使用第一个定义 inorder） 来写

inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t

结果有一个非常简单的结构，似乎相当不错的证明。

写一个版本也不是非常困难

inorderThenInTree : x `Elem` inorder t -> x `InTree` t

不幸的是，到目前为止，我没有想出任何方法来编写一个版本的 inorderThenInTree 我能够证明是与之相反的 inTreeThenInorder。我唯一提出的用途

listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)

我试图回到那里遇到麻烦。

我尝试了一些一般性的想法：

  1. 运用 Vect 代替 List 试图让你更容易找出左边的东西和右边的东西。我陷入了“绿泥”之中。

  2. 绕着树木旋转，尽可能地证明在树根处的旋转导致了一个有充分根据的关系。 （我没有玩下面的旋转，因为我从来没有想过要找到方法 使用 关于这些轮换的任何事情）。

  3. 尝试使用有关如何到达它们的信息来装饰树节点。我没有花很长时间在这上面，因为我想不出通过这种方法表达任何有趣的方法。

  4. 试图构建我们在构建执行此功能的函数时返回的证据。这变得非常混乱，我被卡在某处或其他地方。


10431
2018-06-03 04:25


起源

答案:

你和你一起走在了正确的轨道上 listSplit 引理。您可以使用该函数来了解目标元素是在树的左侧还是右侧。

这是我实施的相关内容

inTreeThenInorder x (branch y l r) e with listSplit x (inOrder l) (y ∷ inOrder r) e

这是完整的实现。我已将它作为外部链接包含在内，以避免不必要的剧透，并利用Agda精彩的HTML超链接，语法突出显示输出。

http://www.galois.com/~emertens/agda-tree-inorder-elem/TreeElem.html


7
2018-06-03 16:32


我终于完成了我的原始目标（证明如果一棵树没有重复的元素，并且具有与另一棵树相同的预订和顺序遍历，那么树是相同的）。看一眼 这个答案。我们非常欢迎有关改进的建议。 - dfeuer

答案:

你和你一起走在了正确的轨道上 listSplit 引理。您可以使用该函数来了解目标元素是在树的左侧还是右侧。

这是我实施的相关内容

inTreeThenInorder x (branch y l r) e with listSplit x (inOrder l) (y ∷ inOrder r) e

这是完整的实现。我已将它作为外部链接包含在内，以避免不必要的剧透，并利用Agda精彩的HTML超链接，语法突出显示输出。

http://www.galois.com/~emertens/agda-tree-inorder-elem/TreeElem.html


7
2018-06-03 16:32


我终于完成了我的原始目标（证明如果一棵树没有重复的元素，并且具有与另一棵树相同的预订和顺序遍历，那么树是相同的）。看一眼 这个答案。我们非常欢迎有关改进的建议。 - dfeuer

我写了 inorderToFro 和 inorderFroTo 以及伊德里斯的相关外表。 这是链接。 

关于您的解决方案我可以提出几点意见（没有详细介绍）：

第一， splitMiddle 没有必要。如果你使用更一般 Right p = listSplit xs ys loc -> elemAppend xs ys p = loc输入 splitRight那么那可以覆盖同样的理由。

其次，你可以使用更多 with 模式而不是显式 _lem 功能;我认为它会更清晰，更简洁。

第三，你做了相当多的工作证明 splitLeft 和合作移动函数的属性通常是有意义的 内 功能。所以，而不是写作 listSplit 并且分别对其结果进行了证明，我们可以修改 listSplit 返回所需的证据。这通常更容易实现。在我的解决方案中，我使用了以下类型：

data SplitRes : (x : a) -> (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> Type where
  SLeft  : (e' : Elem x xs) -> e' ++^ ys = e -> SplitRes x xs ys e
  SRight : (e' : Elem x ys) -> xs ^++ e' = e -> SplitRes x xs ys e

listSplit : (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> SplitRes x xs ys e

我也可以用 Either (e' : Elem x xs ** (e' ++^ ys = e)) (e' : Elem x ys ** (xs ^++ e' = e)) 代替 SplitRes。但是，我遇到了问题 Either。在我看来，伊德里斯的高阶统一太过摇摆不定;我无法理解为什么我的 unsplitLeft 功能不会出现问题 Either。 SplitRes 不包含其类型的函数，所以我猜这就是为什么它工作得更顺利。

一般来说，在这个时候我推荐Agda而不是伊德里斯写这样的样张。它检查得更快，而且更加强大和方便。我很惊讶你在这里写了这么多伊德里斯以及关于树遍历的另一个问题。


4
2018-06-07 11:59


由于我有太多时间，我也写了一篇 原始问题的证明 在Agda，FYI。 - András Kovács
我认为伊德里斯给了我足够的依赖类型的味道，让我真的想学习Agda：P。我写这么多的方式是通过纯粹的坚持。 - dfeuer
一些明确的 lem 需要在其他证明中深入挖掘它们的功能。其他一些人似乎被强加于我的古怪的类型检查行为 with 条款。其他时候，我可能不知道自己在做什么。 - dfeuer
我看到你想出了一个不同的“nodupness”概念。你能否评论一下你认为优点和缺点是什么？ - dfeuer
该 NoDup-s基本上是因为我的直觉觉得最好去寻求更细粒度的递归定义。在我看来，无论如何我都必须证明“根元素不在任何子树中”。但是我不知道这实际上是否比你的定义更好，因为我没有尝试过两者。 - András Kovács

我能够弄清楚如何证明可以从树位置到列表位置，并从阅读中引用的引理类型返回 glguy的回答。最终，我设法走了另一条路，虽然代码（下面）相当可怕。幸运的是，我能够重用可怕的列表引理来证明关于前序遍历的相应定理。

module PreIn
import Data.List
%default total

data Tree : Type -> Type where
  Tip : Tree a
  Node : (l : Tree a) -> (v : a) -> (r : Tree a) -> Tree a
%name Tree t, u

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` (Node l x r)
  OnLeft : x `InTree` l -> x `InTree` (Node l v r)
  OnRight : x `InTree` r -> x `InTree` (Node l v r)

onLeftInjective : OnLeft p = OnLeft q -> p = q
onLeftInjective Refl = Refl

onRightInjective : OnRight p = OnRight q -> p = q
onRightInjective Refl = Refl

noDups : Tree a -> Type
noDups t = (x : a) -> (here, there : x `InTree` t) -> here = there

noDupsList : List a -> Type
noDupsList xs = (x : a) -> (here, there : x `Elem` xs) -> here = there

inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r

rotateInorder : (ll : Tree a) ->
                (vl : a) ->
                (rl : Tree a) ->
                (v : a) ->
                (r : Tree a) ->
                inorder (Node (Node ll vl rl) v r) = inorder (Node ll vl (Node rl v r))
rotateInorder ll vl rl v r =
   rewrite appendAssociative (vl :: inorder rl) [v] (inorder r)
   in rewrite sym $ appendAssociative (inorder rl) [v] (inorder r)
   in rewrite appendAssociative (inorder ll) (vl :: inorder rl) (v :: inorder r)
   in Refl


instance Uninhabited (Here = There y) where
  uninhabited Refl impossible

instance Uninhabited (x `InTree` Tip) where
  uninhabited AtRoot impossible

elemAppend : {x : a} -> (ys,xs : List a) -> x `Elem` xs -> x `Elem` (ys ++ xs)
elemAppend [] xs xInxs = xInxs
elemAppend (y :: ys) xs xInxs = There (elemAppend ys xs xInxs)

appendElem : {x : a} -> (xs,ys : List a) -> x `Elem` xs -> x `Elem` (xs ++ ys)
appendElem (x :: zs) ys Here = Here
appendElem (y :: zs) ys (There pr) = There (appendElem zs ys pr)

tThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t
tThenInorder (Node l x r) AtRoot = elemAppend _ _ Here
tThenInorder (Node l v r) (OnLeft pr) = appendElem _ _ (tThenInorder _ pr)
tThenInorder (Node l v r) (OnRight pr) = elemAppend _ _ (There (tThenInorder _ pr))

listSplit_lem : (x,z : a) -> (xs,ys:List a) -> Either (x `Elem` xs) (x `Elem` ys)
  -> Either (x `Elem` (z :: xs)) (x `Elem` ys)
listSplit_lem x z xs ys (Left prf) = Left (There prf)
listSplit_lem x z xs ys (Right prf) = Right prf


listSplit : {x : a} -> (xs,ys : List a) -> x `Elem` (xs ++ ys) -> Either (x `Elem` xs) (x `Elem` ys)
listSplit [] ys xelem = Right xelem
listSplit (z :: xs) ys Here = Left Here
listSplit {x} (z :: xs) ys (There pr) = listSplit_lem x z xs ys (listSplit xs ys pr)

mutual
  inorderThenT : {x : a} -> (t : Tree a) -> x `Elem` inorder t -> InTree x t
  inorderThenT Tip xInL = absurd xInL
  inorderThenT {x} (Node l v r) xInL = inorderThenT_lem x l v r xInL (listSplit (inorder l) (v :: inorder r) xInL)

  inorderThenT_lem : (x : a) ->
                     (l : Tree a) -> (v : a) -> (r : Tree a) ->
                     x `Elem` inorder (Node l v r) ->
                     Either (x `Elem` inorder l) (x `Elem` (v :: inorder r)) ->
                     InTree x (Node l v r)
  inorderThenT_lem x l v r xInL (Left locl) = OnLeft (inorderThenT l locl)
  inorderThenT_lem x l x r xInL (Right Here) = AtRoot
  inorderThenT_lem x l v r xInL (Right (There locr)) = OnRight (inorderThenT r locr)

unsplitRight : {x : a} -> (e : x `Elem` ys) -> listSplit xs ys (elemAppend xs ys e) = Right e
unsplitRight {xs = []} e = Refl
unsplitRight {xs = (x :: xs)} e = rewrite unsplitRight {xs} e in Refl

unsplitLeft : {x : a} -> (e : x `Elem` xs) -> listSplit xs ys (appendElem xs ys e) = Left e
unsplitLeft {xs = []} Here impossible
unsplitLeft {xs = (x :: xs)} Here = Refl
unsplitLeft {xs = (x :: xs)} {ys} (There pr) =
  rewrite unsplitLeft {xs} {ys} pr in Refl

splitLeft_lem1 : (Left (There w) = listSplit_lem x y xs ys (listSplit xs ys z)) ->
                 (Left w = listSplit xs ys z) 

splitLeft_lem1 {w} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem1 {w}  Refl | (Left w) = Refl
  splitLeft_lem1 {w}  Refl | (Right s) impossible

splitLeft_lem2 : Left Here = listSplit_lem x x xs ys (listSplit xs ys z) -> Void
splitLeft_lem2 {x} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left y) impossible
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Right y) impossible

splitLeft : {x : a} -> (xs,ys : List a) ->
            (loc : x `Elem` (xs ++ ys)) ->
            Left e = listSplit {x} xs ys loc ->
            appendElem {x} xs ys e = loc
splitLeft {e} [] ys loc prf = absurd e
splitLeft (x :: xs) ys Here prf = rewrite leftInjective prf in Refl
splitLeft {e = Here} (x :: xs) ys (There z) prf = absurd (splitLeft_lem2 prf)
splitLeft {e = (There w)} (y :: xs) ys (There z) prf =
  cong $ splitLeft xs ys z (splitLeft_lem1 prf)

splitMiddle_lem3 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) z) ->
                   Right Here = listSplit xs (y :: ys) z

splitMiddle_lem3 {y} {x} {xs} {ys} {z} prf with (listSplit xs (y :: ys) z)
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left w) impossible
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} prf | (Right w) =
    cong $ rightInjective prf  -- This funny dance strips the Rights off and then puts them
                               -- back on so as to change type.


splitMiddle_lem2 : Right Here = listSplit xs (y :: ys) pl ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem2 {xs} {y} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem2 {xs = xs} {y = y} {ys = ys} {pl = pl} Refl | (Left loc) impossible
  splitMiddle_lem2 {xs = []} {y = y} {ys = ys} {pl = pl} Refl | (Right Here) = rightInjective prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = x} {ys = ys} {pl = Here} prf | (Right Here) = (\Refl impossible) prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = y} {ys = ys} {pl = (There z)} prf | (Right Here) =
    cong $ splitMiddle_lem2 {xs} {y} {ys} {pl = z} (splitMiddle_lem3 prpr)

splitMiddle_lem1 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) pl) ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem1 {y} {x} {xs} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Left z) impossible
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Right Here) = splitMiddle_lem2 prpr

splitMiddle : Right Here = listSplit xs (y::ys) loc ->
              elemAppend xs (y::ys) Here = loc

splitMiddle {xs = []} prf = rightInjective prf
splitMiddle {xs = (x :: xs)} {loc = Here} Refl impossible
splitMiddle {xs = (x :: xs)} {loc = (There y)} prf = cong $ splitMiddle_lem1 prf

splitRight_lem1 : Right (There pl) = listSplit (q :: xs) (y :: ys) (There z) ->
                  Right (There pl) = listSplit xs (y :: ys) z

splitRight_lem1 {xs} {ys} {y} {z} prf with (listSplit xs (y :: ys) z)
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} Refl | (Left x) impossible
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} prf | (Right x) =
    cong $ rightInjective prf  -- Type dance: take the Right off and put it back on.

splitRight : Right (There pl) = listSplit xs (y :: ys) loc ->
             elemAppend xs (y :: ys) (There pl) = loc
splitRight {pl = pl} {xs = []} {y = y} {ys = ys} {loc = loc} prf = rightInjective prf
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = Here} Refl impossible
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = (There z)} prf =
  let rec = splitRight {pl} {xs} {y} {ys} {loc = z} in cong $ rec (splitRight_lem1 prf)


---------------------------
-- tThenInorder is a bijection from ways to find a particular element in a tree
-- and ways to find that element in its inorder traversal. `inorderToFro`
-- and `inorderFroTo` together demonstrate this by showing that `inorderThenT` is
-- its inverse.

||| `tThenInorder t` is a retraction of `inorderThenT t`
inorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` inorder t) -> tThenInorder t (inorderThenT t loc) = loc
inorderFroTo Tip loc = absurd loc
inorderFroTo (Node l v r) loc with (listSplit (inorder l) (v :: inorder r) loc) proof prf
  inorderFroTo (Node l v r) loc | (Left here) =
    rewrite inorderFroTo l here in splitLeft _ _ loc prf
  inorderFroTo (Node l v r) loc | (Right Here) = splitMiddle prf
  inorderFroTo (Node l v r) loc | (Right (There x)) =
    rewrite inorderFroTo r x in splitRight prf

||| `inorderThenT t` is a retraction of `tThenInorder t`
inorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> inorderThenT t (tThenInorder t loc) = loc
inorderToFro (Node l v r) (OnLeft xInL) =
  rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL)
  in cong $ inorderToFro _ xInL
inorderToFro (Node l x r) AtRoot =
  rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot)
  in Refl
inorderToFro {x} (Node l v r) (OnRight xInR) =
  rewrite unsplitRight {x} {xs = inorder l} {ys = v :: inorder r} (tThenInorder (Node Tip v r) (OnRight xInR))
  in cong $ inorderToFro _ xInR

3
2018-06-04 17:43



热门问题

不使用eval / new函数的JavaScript模板库 当涉及内部类时，Java继承如何工作 .NET Windows服务的奇怪问题 在.ipa或.app下查找App ID 快速入门XSLT参考[关闭] 如何找出Android应用程序中未使用的资源 Ruby中并发的同步方法[重复] 将std :: chrono :: system_clock :: time_point转换为struct timeval并返回 Google Drive API V3（javascript）更新文件内容 Bootstrap 3.0 - 将元素推到底部 受密码保护的.NET ClickOnce部署？ 如何用postgresql安装wordpress coq Set或Type如何成为命题 硒滚动元素进入（中心）视图 在Spring Transaction JUnit测试中自动装配Hibernate会话的正确方法 Git的Dockerfile策略 如何在FOS_PICKFOLDER中使用IFileDialog，同时仍在对话框中显示文件名 在Firefox扩展中复制Google Chrome浏览器操作弹出效果 CakePHP找到MAX 芹菜 - 完成任务的召唤功能 从使用fmemopen创建的流中读取宽字符 .NET是否为每个程序集创建一个字符串实习池？ DefaultModelBinder不绑定嵌套模型 Navigator.MediaDevices.getUserMedia（）使用了哪些相机通信标准？ 选择命名空间名称时应该知道什么？ cout Swagger Codegen CLI Java客户端 - 如何正确使用它 一个很好的哈希函数用于采访整数，字符串？ Maven 3 ciManagement配置的目的是什么？ 如何通过语言文化获取代码页？
licensed under cc by-sa 3.0 with attribution.
隐私政策 往来