我正在研究“Real World Haskell”,这导致了一个名为“A tutorial on the universality and expressiveness of fold”的免费 PDF 。它表明“折叠”是“通用的”。我正在与他对“普遍”的定义搏斗,并想听听那些已经花时间消化它的人的意见:请用最简单、最通俗易懂的英语解释“折叠的普遍属性”?这个“普遍属性”是什么,为什么它很重要?
谢谢。
我正在研究“Real World Haskell”,这导致了一个名为“A tutorial on the universality and expressiveness of fold”的免费 PDF 。它表明“折叠”是“通用的”。我正在与他对“普遍”的定义搏斗,并想听听那些已经花时间消化它的人的意见:请用最简单、最通俗易懂的英语解释“折叠的普遍属性”?这个“普遍属性”是什么,为什么它很重要?
谢谢。
(行话模式关闭:-)
通用属性只是证明两个表达式相等的一种方式。(这就是行话“证明原理”的意思。)普遍属性说,如果你能够证明这两个方程
g [] = v
g (x:xs) = f x (g xs)
那么你可以得出附加方程
g = fold f v
反之亦然,但这只是通过扩展 的定义来证明是微不足道的fold
。通用属性是一个更深层次的属性(这是一种行话,说为什么它是真的不太明显。)
这样做很有趣的原因是它可以让你避免归纳证明,这几乎总是值得避免的。
该论文定义了两个属性:
g [] = v
g (x : xs) = f x (g xs)
然后声明它fold
不仅是满足这些属性的函数,而且是唯一满足这些属性的函数。它在这方面是独一无二的,这使得它在论文使用的意义上具有“普遍性”。
fold 的特性是它是一个列表递归函数,它等效于所有其他列表递归函数,只要你给它正确的参数。
它具有此属性,因为它接受将应用于列表中项目的函数作为参数。
例如,如果我们编写了一个简单的 sum 函数:
sum [] = 0
sum (head:tail) = head + (sum tail)
那么我们实际上可以将它写成一个折叠函数,通过传入我们想要用来组合项目的 (+) 运算符:
sum list = foldl (+) 0 list
因此,任何简单且递归地作用于列表的函数都可以重写为折叠函数。这种等价性就是它所拥有的属性。我相信他称这个属性是通用的,因为它适用于所有这些线性列表递归算法,无一例外。
正如他解释的那样,这个属性之所以如此有用,是因为我们可以证明所有这些其他算法实际上都等价于折叠,通过证明有关折叠的一些东西,我们也可以为所有其他算法证明它。
我个人觉得 fold 函数很难理解,所以有时我使用自己的函数,如下所示:
-- forall - A kind of for next loop
-- list is list of things to loop through
-- f is function to perform on each thing
-- c is the function which combines the results of f
-- e is the thing to combine to when the end of the list is reached
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b
forall [] f c e = e
forall (x:xs) f c e = c (f x) (forall xs f c e)
(这实际上比 foldl 稍微强大一些,因为它具有将函数 f 应用于列表中的每个项目的额外功能。)
好吧,没有人证明我的功能。但这没关系,因为我可以证明我的函数实际上是一个折叠函数:
forall l f c e = foldl c e (map fn l)
因此,所有关于 fold 的证明,对于我的 forall 函数以及它在整个程序中的所有用途也被证明是正确的。(请注意,我们甚至不需要考虑在对 forall 和 foldl 的每个不同调用中提供了哪种函数 c,这没关系!)
我刚刚在 Wikipedia 中发现了一个新的(对我而言)条目,“Universal Property”。它为这个问题提供了很多启示。这是链接: 从中,我(暂时)得出以下结论:
看来,这两点合在一起就体现了“普遍属性”一词的含义。
虽然如果不阅读该系列中从分类的角度解释通用属性的前几篇文章可能有点难以理解,但这篇文章对折叠的通用属性以及映射和过滤器进行了详细的分类解释。
http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/
虽然我还没有写出来,但后续将把它推广到通用数据结构上的“折叠式”操作(并使其更易于理解,尽管更抽象)。
有关什么是通用属性的更多信息,请参阅这篇文章:http: //jeremykun.com/2013/05/24/universal-properties/
这里是该系列所有帖子的链接:http: //jeremykun.com/main-content/
事实上,目前公认的答案是理解通用属性关于折叠的最简单方法。上面链接的文章只是通过相关论文中没有的类别理论提供了更详细的技术描述。不过,我不同意公认答案中的说法,即普遍属性比无行话的说法更深层次的属性。fold 的普遍性质正是同一个陈述,只是按照范畴论分析事物的性质,被装进了初始对象和最终对象的语言中。这种分析之所以有价值,正是因为它具有自然的概括性。