推广折叠使得它变得足够表达以定义任何有限递归？

Question

因此,有一种被称为"折叠的普遍属性"的东西,完全如下:

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

但是,正如您现在可能的那样,有一些罕见的情况dropWhile,fold f i 除非您将其概括,否则无法重新定义.

最简单但最明显的推广方法是重新定义通用属性:

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.让我们尝试用普遍属性帮助解决给定的方程式,一开始就提到:

• 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从左边自由发生,因此平等不能成立.

---

现在让我试着解释我提出的结果并提出问题.我看到这个问题xs 正在成为一个未绑定的变量 ; 对于各种情况都是如此,包括上面提到的情况dropWhile.是否意味着解决方程式的唯一方法是"扩展" rs到一对(rs, xs)？换句话说,fold累积成元组而不是单一类型(忽略元组本身是单一类型的事实)？有没有其他方法可以概括绕过配对？

Answer 1

正如你所说。通用属性说g [] = i; g (x:xs) = f x (g xs)iff g = fold f i。这不适用于 的直接定义dropWhile，因为可能f :: a -> [a] -> [a]不仅取决于当前折叠步骤中的元素和累积值，还取决于要处理的整个列表后缀（用您的话来说，“ xsemerg[es ] 作为未绑定变量”）。可以做的是扭转dropWhile，以便对列表后缀的这种依赖性在累积值中变得明显，无论是通过元组 - 参见。dropWhilePair从这个问题来看，用f :: a -> ([a], [a]) -> ([a], [a])——或者一个函数——就像chi 的实现一样......

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。事实上，您的问题带来的元组解决方法直接反映了同态的概念（有关它们的解释，请参阅什么是同态？及其 Conor McBride 的精美答案）。从表面上看，拟态现象是变态现象的概括（即简单的折叠）。然而，只需要稍微改变一下就可以实现变态的拟态。（对此的更多技术评论可以在Varmo Vene 的博士论文《归纳和共归纳类型的分类编程》的第 3 章中找到。）