是否可以使用 foldr 重写任何递归定义？

Question

假设我在 haskell 中有一个通用的递归定义，如下所示：

foo a0 a1 ... = base_case
foo b0 b1 ...          
    | cond1 = recursive_case_1
    | cond2 = recursive_case_2
    ...

总能用foldr重写吗？可以证明吗？

Answer 1

在类型理论中，确实可以 详细说明 通过相关的 模式匹配 所有定义只使用 eliminators（folds 的强类型版本，列表的 foldr 的泛化）。

参见例如Eliminating Dependent Pattern Matching (pdf)

Answer 2

如果我们从字面上解释你的问题，我们可以写 const value foldr 来实现任何 value，正如@DanielWagner 在评论中指出的那样。

一个更有趣的问题是我们是否可以禁止从 Haskell 和 "recurse" 仅到 eliminators/catamorphisms 的一般递归每个用户定义的数据类型，它们是 foldr 对归纳定义数据类型的自然概括。这本质上是（高阶）原始递归。

执行此限制后，我们只能将终止函数（消除器）组合在一起。这意味着我们不能再定义非终止函数。

作为第一个例子，我们失去了平凡的递归

f x = f x
-- or even
a = a

因为，如前所述，语言变得完整。

更有趣的是，通用不动点运算符丢失了。

fix :: (a -> a) -> a
fix f = f (fix f)

一个更有趣的问题是：total 个函数我们可以用 Haskell 表达什么呢？我们确实失去了所有非全功能，但我们失去了任何全功能吗？

可计算性理论指出，由于语言变得完整（不再有非终止），即使在整个片段上我们也失去了表达能力。

证明是标准的对角化论证。修复整个片段中的所有程序枚举，以便我们可以说 "the i-th program"。然后，让 eval i x 成为运行的结果，第 i 个程序以自然 x 作为输入（为简单起见，假设这是正确输入的，并且结果是自然的）。请注意，由于语言是整体的，因此结果必须存在。此外，eval 可以在不受限制的 Haskell 语言中实现，因为我们可以在 Haskell 中编写 Haskell 的解释器（留作练习 :-P），并且对于该片段来说效果很好。然后，我们只需取

f n = succ $ eval n n

以上是一个总函数（总函数的组合），在Haskell中可以表示，但不能在片段中表示。事实上，否则会有一个程序来计算它，比如第 i 个程序。在这种情况下，我们会有

eval i x = f x

所有 x。但是，

eval i i = f i = succ $ eval i i

这是不可能的 -- 自相矛盾。 QED.

是否可以使用 foldr 重写任何递归定义？

Can any recursive definition be rewritten using foldr?

haskell

functional-programming

fold