将fold泛化，使其变得足以定义任何有限递归? [英] Generalizing fold such that it becomes expressive enough to define any finite recursion?

问题描述

因此，有一种被称为折叠的通用属性"的东西，具体说明如下:

So, there is something known as a "universal property of fold", stating exactly following:

g [] = i; g (x:xs) = f x (g xs)< => g = fold f i

但是，就像您现在所看到的那样，有一些罕见的情况，例如dropWhile，除非您将其概括化，否则无法将其重新定义为fold f i .

However, as you probably now, there are rare cases like dropWhile, which can not be redefined as fold f i unless you generalize it.

最简单但显而易见的概括方法是重新定义通用属性:

The simplest yet obvious way to generalize is to redefine universal property:

g' y [] = j y; g' y (x:xs) = h y x xs (g' y xs)< => g' y = fold (?) l

在这一点上，我可以做一个假设:我假设存在某种函数p :: a -> b -> b，该函数可以满足方程g' y = fold p l.让我们尝试在通用属性的帮助下求解给定的方程，一开始就提到:

At this point I can make my assumption: I assume existence of somewhat function p :: a -> b -> b, which would satisfy the equation g' y = fold p l. Let's try to solve given equation with help of universal property, mention at the very beginning:

• g' y [] = j y = fold p l [] = l => j y = l
• g' y (x:xs) = h y x xs (g' y xs) = fold p l (x:xs) = p x (fold p l xs) = p x (g' y xs) =>让rs = (g' y xs)， h y x xs rs = p x rs，这是错误的:xs从左边自由出现，因此相等性不能成立.

• g' y [] = j y = fold p l [] = l => j y = l
• g' y (x:xs) = h y x xs (g' y xs) = fold p l (x:xs) = p x (fold p l xs) = p x (g' y xs) => letting rs = (g' y xs), h y x xs rs = p x rs, which is wrong: xs occurs freely from the left and thus equality can't hold.

现在让我尝试解释我想出的结果并提出问题. 我发现问题是xs 正在作为未绑定变量；在包括上述dropWhile在内的各种情况下都是如此.这是否意味着方程求解的唯一方法是将rs扩展"为一对(rs, xs)?换句话说，fold会累积到元组而不是单一类型(忽略元组本身是单一类型的事实)吗?还有其他方法可以概括旁路配对吗?

Now let me try to interpret result I've came up with and ask question. I see that the problem is xs emerging as unbound variable; it's true for various situations, including above mentioned dropWhile. Does it mean that the only way that equation can be solved is by "extending" rs to a pair of (rs, xs)? In other words, fold accumulates into tuple rather than a single type (ignoring the fact that tuple itself is a single type)? Is there any other way to generalize bypassing pairing?

推荐答案

就是您所说的.通用属性表示g [] = i; g (x:xs) = f x (g xs)和g = fold f i.这不适用于dropWhile的简单定义，因为可能的f :: a -> [a] -> [a]不仅取决于当前折叠步骤的元素和累加值，还取决于要处理的整个列表后缀(在您的单词，"xs emerg [es]作为未绑定变量").可以做的是扭转dropWhile，以便对列表后缀的这种依赖关系可以通过元组(参见cf)在累加值中体现出来. dropWhilePair来自此问题，带有f :: a -> ([a], [a]) -> ([a], [a])-或函数-如

It is as you say. The universal property says that g [] = i; g (x:xs) = f x (g xs) iff g = fold f i. This can't apply for a straightforward definition of dropWhile, as the would-be f :: a -> [a] -> [a] depends not just on the element and accumulated value at the current fold step, but also on the whole list suffix left to process (in your words, "xs emerg[es] as an unbound variable"). What can be done is twisting dropWhileso that this dependency on the list suffix becomes manifest in the accumulated value, be it through a tuple -- cf. dropWhilePair from this question, with f :: a -> ([a], [a]) -> ([a], [a]) -- or a function -- as in chi's implementation...

dropWhileFun = foldr (\x k -> \p -> if p x then k p else x : k (const False)) (const [])

...和f :: a -> ((a -> Bool) -> [a]) -> ((a -> Bool) -> [a]).

归根结底，通用属性就是它的本质-关于foldr的基本事实.并非所有递归函数都可以立即通过foldr表示，这并非偶然.实际上，您的问题在表格中提出的解决方法直接反映了同态的概念(有关它们的解释，请参见 What是同形的?及其Conor McBride的精妙答案).从表面上看，同态是对同态的概括(即简单的折叠).但是，仅需稍稍扭曲即可实现同形异形. (有关此问题的其他技术评论，例如，可以在 归纳和共归类型的分类编程，Varmo Vene的博士学位论文.)

At the end of the day, the universal property is what it is -- a fundamental fact about foldr. It is no accident that not all recursive functions are immediately expressible through foldr. In fact, the tupling workaround your question brings to the table directly reflects the notion of paramorphism (for an explanation of them, see What are paramorphisms? and its exquisite answer by Conor McBride). At face value, paramorphisms are generalisations of catamorphisms (i.e. a straightforward fold); however, it only takes a slight contortion to implement paramorphisms in terms of catamorphisms. (Additional technical commentary on that might be found, for instance, in Chapter 3 of Categorical Programming With Inductive and Coinductive Types, Varmo Vene's PhD thesis.)

这篇关于将fold泛化，使其变得足以定义任何有限递归?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！