haskell - 可以使用foldr 重写任何递归定义吗？

Question

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

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

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

Answer 1

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

一个更有趣的问题是，我们是否可以禁止 Haskell 的一般递归，并且“递归”仅通过与每个用户定义的数据类型关联的消除器/变形，这是自然概括foldr 到归纳定义的数据类型。这本质上是(高阶)原始递归。

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

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

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

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

更有趣的是，一般的定点运算符丢失了。

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

一个更有趣的问题是:我们可以在 Haskell 中表达的总共个函数是多少？我们确实失去了所有非全部功能，但是我们会失去任何全部功能吗？

可计算性理论指出，由于语言变得完整(不再是非终止)，我们甚至在整个片段上也失去了表达性。

证明是标准的对角化论证。修复总片段中程序的任何枚举，以便我们可以谈论“第 i 个程序”。然后，令 eval i x 为在自然 x 上运行第 i 程序作为输入的结果(为简单起见，假设这是很好的)键入，结果是自然的)。请注意，由于语言是完整的，因此结果必须存在。此外，eval 可以用不受限制的 Haskell 语言实现，因为我们可以用 Haskell 编写 Haskell 的解释器(作为练习:-P)，并且这对于片段来说也同样有效。然后，我们只需采取

f n = succ $ eval n n

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

eval i x = f x

对于所有x。但随后，

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

这是不可能的——矛盾。量子ED。