haskell - 玫瑰树如何展开工作(来自折纸编程)

Question

我一直在读这篇文章Origami Programming by Jeremy Gibbons我无法弄清楚 unfoldR 和 unfoldF 函数如何用于 Rose Trees。

在论文中，Rose Tree 类型定义为:

data Rose α = Node α (Forest α)
type Forest α = List (Rose α)

unfoldR 和 unfoldF 函数是相互递归的，定义为:

unfoldR :: (β → α) → (β → List β) → β → Rose α
unfoldR f g x = Node (f x) (unfoldF f g x)

unfoldF :: (β → α) → (β → List β) → β → Forest α
unfoldF f g x = mapL (unfoldR f g) (g x)

看起来，除了一些小的边缘情况外，这些函数将无限递归。这两个相互递归的函数如何终止？

Answer 1

它们不一定终止!

unfoldR 和 unfoldF 的定义形成 co-inductive分别作用于类型 Rose 和 Forest 。共感应是结构感应的对偶。共归纳函数旨在创建无限的数据结构，稍后将通过递归函数使用这些数据结构。

由于 Haskell 的惰性求值，我们可以通过应用函数 f::(β → α) 和 g::(β → List β) 以及 x::β 的初始“种子值”x::β 到 unfoldR 和 unfoldF。

然后，我们将使用另一个递归函数 h::Rose -> γ 来使用无限数据结构

整理一个未定义的示例:

f :: (β → α)
f = undefined
g :: (β → List β) 
g = undefined
x :: β
x = undefined
h :: Rose -> γ
h = undefined

result :: γ
result = h $ unfoldR f g x

这里结果将是对无限结构的计算的评估。但如果它是一个无限数据结构，h 如何终止？ 如何 结果 如何评估？

虽然 unfoldR f g x 将产生无限结构，但 h 只会搜索搜索空间的有限子集，因此 结果可以被评估。

注意: 我们还可以定义 f、g 和 x 来创建有限结构，它不必是无限的