请用最简单、最通俗的英语解释一下“折叠的普遍性质”?

发布于 2024-07-19 09:15:33 字数 492 浏览 6 评论 0原文

我正在研究“Real World Haskell”,它生成了一个名为 “关于折叠的通用性和表现力的教程”。 它表明“折叠”是“通用的”。 我正在努力思考他对“通用”的定义,并且想听听那些已经投入时间消化它的人的说法:请用最简单、最通俗易懂的英语解释“折叠的通用属性” ?这个“普遍财产”是什么,为什么它很重要?

谢谢。

I am working through "Real World Haskell", which led to to a free PDF called "A tutorial on the universality and expressiveness of fold". It makes the point that a "fold" is "universal". I am wrestling with his definition of "universal", and would like to hear the from those who have already invested time digesting it: Please explain in the simplest, most jargon-free English possible, the "universal property of fold"? What is this "universal property", and why is it important?

Thanks.

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(5

古镇旧梦 2024-07-26 09:15:33

(行话模式关闭:-)

通用属性只是证明两个表达式相等的一种方法。 (这就是行话“证明原理”的含义。)
通用性质表明,如果您能够证明这两个方程,

g []     = v
g (x:xs) = f x (g xs)

那么您可以得出附加方程。

g = fold f v

反之亦然,但仅通过扩展 fold 的定义来证明这一点是微不足道的。 通用属性是一个更深层次的属性(这是一种行话,表示它为什么不那么明显。)

这样做很有趣的原因是它可以让你避免通过归纳证明,这几乎总是值得避免的。

(Jargon mode off :-)

The universal property is just a way of proving that two expressions are equal. (That's what is meant by the jargon "proof principle".)
The universal property says that if you are able to prove these two equations

g []     = v
g (x:xs) = f x (g xs)

then you may conclude the additional equation

g = fold f v

The converse is also true, but that's trivial to show just by expanding the definition of fold. The universal property is a much deeper property (which is a jargony way of saying it's less obvious why it is true.)

The reason it's interesting to do this at all is that it lets you avoid proof by induction, which is almost always worth avoiding.

无人问我粥可暖 2024-07-26 09:15:33

论文定义了两个属性:

g   []     = v
g (x : xs) = f x (g xs)

然后指出 fold 不仅是满足这些属性的一个函数,而且是满足这些属性的唯一函数特性。 它在这方面的独特性使其在本文所使用的意义上具有“通用性”。

the paper defines two properties:

g   []     = v
g (x : xs) = f x (g xs)

and then states that fold is not only a function that satisfies those properties, but is the only function that satisfies those properties. that it is unique in that regard is what makes it 'universal' in the sense the paper is using.

岁月蹉跎了容颜 2024-07-26 09:15:33

Fold 的属性是它是一个列表递归函数,只要给它正确的参数,它就相当于所有其他列表递归函数。

它具有此属性,因为它接受将应用于列表中的项目的函数作为参数。

例如,如果我们编写一个简单的求和函数:

sum []          = 0
sum (head:tail) = head + (sum tail)

那么我们实际上可以将其编写为折叠函数,通过传入我们想要用来组合项目的 (+) 运算符:

sum list = foldl (+) 0 list

因此,任何简单且递归地作用的函数列表可以重写为折叠函数。 这种等价性就是它所拥有的属性。 我相信他称该属性为通用属性,因为它适用于所有这些线性列表递归算法,无一例外。

正如他所解释的,这个属性如此有用的原因是因为我们可以证明所有其他算法实际上等同于折叠,通过证明有关折叠的一些东西,我们也为所有其他算法证明了这一点。

的函数,如下所示:(

-- 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应用于列表中的每个项目的额外功能。)

我个人觉得fold函数很难理解,所以有时我使用自己 没有人证明我的功能。 但这并不重要,因为我可以证明我的函数实际上是一个折叠函数:

forall l f c e = foldl c e (map fn l)

因此,关于折叠的所有已被证明的事情对于我的 forall 函数以及它在我的程序中的所有用途也被证明是正确的。 (注意,我们甚至不需要考虑在 forall 和 Foldl 的每个不同调用中提供什么样的函数 c,这并不重要!)

The property that fold has is that it is a list-recursing function, which is equivalent to all other list-recursing functions, provided you give it the right parameters.

It has this property, because it accepts as a parameter, the functions which will be applied to the items in the list.

For example, if we wrote a simple sum function:

sum []          = 0
sum (head:tail) = head + (sum tail)

then we could actually write it as a fold function instead, by passing in the (+) operator which we want to use to combine the items:

sum list = foldl (+) 0 list

So any function which acts simply and recursively over a list can be rewritten as a fold function. That equivalence is the property it holds. I believe he calls the property universal, because it works over all these linear-list-recursive algorithms, without exception.

And as he explains, the reason this property is so useful, is that because we can show all these other algorithms are actually equivalent to fold, by proving something about fold, we also prove it for all those other algorithms.

I personally found the fold function hard to understand, so sometimes I used my own which looks like this:

-- 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)

(This is actually slightly more powerful than foldl because it has the extra feature of applying the function f to each item in the list.)

Well nobody proved anything about my function. But that doesn't matter, because I can show that my function is in fact a fold function:

forall l f c e = foldl c e (map fn l)

And hence all the things that have been proved about fold, are also proven true for my forall function, and all its uses throughout my program. (Note we need not even consider what kind of function c is supplied in each of the different calls to forall and foldl, it doesn't matter!)

时间海 2024-07-26 09:15:33

我刚刚在维基百科上发现了一个新的(对我来说)条目,“通用财产”。 它为这个问题提供了很多线索。 这是链接:
由此,我(暂时)得出以下结论:

  1. 尽管您可能会想到 100 种不同的方法来遍历列表、沿途计算并从列表中生成一个最终值,但所有 100 种方法都是同构的 /em> (意味着最终它们是相同的)。 实际上只有一种方法可以将列表减少到一个值,那就是 FOLD。
  2. Fold 也是如何将列表缩减为单个值的“最有效的解决方案”。 或者您可能会说,最“分解”或最“简化”的解决方案。

这两点似乎共同体现了“普遍财产”一词的含义。

I just found a new (to me) entry in Wikipedia, "Universal Property". It sheds a TON of light on this question. Here's the link:
From it, I (tenatively) conclude the following:

  1. Though you may think of 100 different ways to walk through a list, computing along the way, and producing one final value from the list, all 100 of those ways are isomorphic (meaning that ultimately, they're the same). There really is only one way to reduce a list to one value, and that is FOLD.
  2. Fold is also the "most efficient solution" to how to reduce a list to a single value. Or you might say, the most "factored" or most "simplified" solution.

Together, it seems, those 2 points capture the meaning of the term "universal property".

无法言说的痛 2024-07-26 09:15:33

尽管如果不阅读该系列中从分类角度解释通用属性的前几篇文章,可能会有点难以理解,但这篇文章对折叠、映射和过滤器的通用属性进行了详细的分类解释。

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/

事实上,当前接受的答案是理解通用属性关于折叠的含义的最简单方法。 上面链接的文章只是通过范畴论给出了更详细的技术描述,而相关论文中没有提到这一点。 不过,我不同意已接受的答案中的陈述,即普遍财产是比无行话陈述更深层次的财产。 折叠的普遍性质正是同样的陈述,只是根据范畴论分析事物的本质,被包装成初始和最终对象的语言。 这种分析之所以有价值,正是因为它具有自然的概括性。

Though it may be a bit difficult to follow without reading the previous posts in the series explaining universal properties from a categorical standpoint, this post gives a detailed categorical explanation of the universal property of fold, as well as map and filter.

http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/

Though I have yet to write it, the followup will generalize this (and make it much simpler to understand, albeit more abstract) to "fold-like" operations on general data structures.

See this post for more on what a universal property is: http://jeremykun.com/2013/05/24/universal-properties/

And here for links to all posts in the series: http://jeremykun.com/main-content/

In truth, the currently accepted answer is the easiest way to understand what the universal property is saying about fold. The articles linked to above simply give a more detailed technical description via category theory that is absent from the paper in question. I disagree the statement in the accepted answer, though, that the universal property is a much deeper property than the jargon-free statement. The universal property of fold is precisely the same statement, just boxed up into the language of initial and final objects as per the nature of analyzing things with category theory. This analysis is valuable precisely because of its natural generalizations.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文