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

Question

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

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

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

Answer 1

如果我们从字面上解释你的问题，我们可以编写const value foldr来实现任何value，正如 @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运行第一个程序作为输入的结果（为简单起见，假设这是正确类型的，并且结果是自然数）。请注意，由于语言是完整的，因此结果必须存在。此外，可以用不受限制的 Haskell 语言来实现，因为我们可以用 Haskell 编写 Haskell 的解释器（作为练习留下：-P），并且这对于片段来说也可以很好地工作。然后，我们只需取ixeval

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。