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

Question

我在看如何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. 尝试构建我们在构建执行此功能的函数时返回的证据.这变得非常混乱,我被卡在某处或其他地方.

Answer 1

你的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

Answer 2

我在 Idris 中编写了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 而不是 Idris 来编写这样的证明。它的检查速度要快得多，而且更加健壮和方便。我很惊讶你在这里写了这么多 Idris 以及关于树遍历的另一个问题。