agda - 如何在树及其遍历之间建立​​双射？

Question

我正在查看How does inorder+preorder construct unique binary tree?并认为用 Idris 写一个正式的证明会很有趣。不幸的是，我很早就陷入困境，试图证明在树中查找元素的方法与在中序遍历中查找它的方法相对应(当然，我还需要为前序遍历执行此操作) 。任何想法都会受到欢迎。我对完整的解决方案并不是特别感兴趣——更多的只是帮助朝着正确的方向开始。

给定

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 引理是在正确的轨道上。您可以使用该函数来了解目标元素是位于树的左侧还是右侧。在Agda标准库中listSplit被称为++⁻

这是我的实现中的相关行

with ++⁻ (inorder l) x∈t

这是完整的实现。我将其作为外部链接包含在内，以避免不必要的剧透，并利用 Agda 精彩的 HTML 超链接、语法突出显示的输出。您可以单击查看任何支持引理的类型和定义。

https://glguy.net/agda-tree-inorder-elem/Tree.html