haskell - 泛化 fold 使其变得足以定义任何有限递归?

标签 haskell functional-programming generic-programming fold proof

因此,有一种称为“折叠的通用属性”的东西,确切地说如下:
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 作为未绑定(bind)变量出现 ;对于各种情况都是如此,包括上面提到的dropWhile .这是否意味着求解方程的唯一方法是“扩展”rs一对(rs, xs) ?换句话说,fold累积到 元组而不是单个类型 (忽略元组本身是单一类型的事实)?有没有其他方法可以概括绕过配对?

    最佳答案

    正如你所说。通用属性说 g [] = i; g (x:xs) = f x (g xs)如果g = fold f i .这不适用于 dropWhile 的直接定义。 , 作为可能的 f :: a -> [a] -> [a]不仅取决于当前折叠步骤的元素和累积值,还取决于要处理的整个列表后缀(用您的话来说,“xs emerg[es] 作为未绑定(bind)变量”)。能做的就是扭dropWhile这样对列表后缀的这种依赖就会在累加值中体现出来,无论是通过一个元组——参见。 dropWhilePair from this question , 与 f :: a -> ([a], [a]) -> ([a], [a]) -- 或函数 -- 如 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 立即表达,这并非偶然。 .实际上,您的问题提出的元组解决方法直接反射(reflect)了超态的概念(有关它们的解释,请参阅 What are paramorphisms? and its exquisite answer by Conor McBride )。从表面上看,超态是变态的概括(即直接折叠);然而,就变态而言,实现超态只需要轻微的扭曲。 (例如,可以在 Categorical Programming With Inductive and Coinductive Types, Varmo Vene's PhD thesis 的第 3 章中找到关于此的其他技术评论。)

    关于haskell - 泛化 fold 使其变得足以定义任何有限递归?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/49138464/

    相关文章:

    list - 有人可以用我的 Haskell 代码诊断问题吗?

    haskell - 如何确定Haskell函数的类型?

    c - Valgrind 错误和每个元素一个分配的通用列表

    Java 7 传递方法作为通用 SQL 死锁检查的参数

    haskell - 是否可以? : Behavior t [Behavior t a] -> Behavior t [a]

    haskell - 非单射封闭型族

    functional-programming - 如何在 OCaml 中以功能方式使用支持就地修改的字段更新记录?

    kernel - 通用 OpenCL 模板内核和主机

    haskell - Haskell 中逻辑表达式的数据结构

    functional-programming - SICP 练习 4.6 : Implementing let in the evaluator as a derived expression based on lambda