3

假设我们定义了一个玫瑰树，以及数据类型上的相应折叠。

data RTree a = Node a [RTree a]

foldRTree :: (a -> [b] -> b) -> RTree a -> b
foldRTree f (Node x xs) = f x (map (foldRTree f) xs)

这种结构的深度优先遍历的递归定义将是：

dft :: RTree a -> [a]
dft (Node x xs) = x : concat (map dft xs)

我们可以将 dft 表示为 Rose Trees 上的折叠，特别是我们可以通过代数推导出这样的折叠。

// Suppose dft = foldRTree f
// Then foldRTree f (Node x xs) = f x (map (foldRTree f) xs) (definition of foldRTree)
// But also foldRTree f (Node x xs) = dft (Node x xs) (by assumption)
//                                 = x : concat (map dft xs) (definition of dft)

// So we deduce that f x (map (foldRTree f) xs) = x : concat (map dft xs)
// Hence f x (map dft xs) = x : concat (map dft xs) (by assumption)
// So we now see that f x y = x : concat y

我想我们可以这样做的原因是因为 foldRTree 捕获了 RTrees 上的一般递归结构，这让我想到了关于展开的查询。

我们将展开定义如下：

unfold :: (a -> Bool) -> (a -> b) -> (a -> a) -> a -> [b]
unfold n h t x | n x = []
               | otherwise = h x : unfold n h t (t x)


// Or Equivalently
unfold' n h t = map h . takeWhile (not.n) . iterate t

我们可以将深度优先遍历表示为展开如下：

dft (Node x xs) = x : unfold null h t xs
                         where h ((Node a xs) : ys) = a
                               t ((Node a xs) : ys) = xs ++ ys

我正在努力寻找一种方法来开发一种以与 cons 相同的方式代数计算函数 nht 的方法。特别是在开发展开过程中有一个巧妙的步骤，即意识到展开的最终参数需要是 [RTree a] 类型，而不仅仅是 RTree a。因此，对 dft 提出的论点并没有直接传递给展开，因此我们在推理这两个函数时遇到了障碍。

我将非常感谢任何能够提供一种数学方法来推理展开的人，这种方式可以计算所需的函数 nh 和 t 在将递归函数（自然是折叠）表示为展开（可能使用一些定律）时连接折叠和展开？）。一个自然的问题是我们必须用什么方法来证明这种关系是正确的。

4

0 回答 0