haskell - 是否有任何非递归术语可以折叠在斯科特编码列表上？

Question

假设我有一个 scott-encoded列表如:

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

我想要一个接收此类列表并将其转换为实际列表([1,2,3])的函数，但此类函数不能递归。也就是说，它必须是 eta-beta 范式。这个功能存在吗？

Answer 1

好吧，我试一试。请随时纠正我，因为我不是这方面的专家。

对于任意x和xs ，情况一定是 toList (\c n -> c x xs)简化为可转换为 x : toList xs 的项。

只有当我们将左侧减少到 c x xs 时，这才有可能通过申请(\c n -> c x xs)给一些c和n 。所以toList ~ (\f -> f ? ?) 。 (顺便说一句，这是我想不出一个很好的严格论证的部分；我有一些想法，但没有一个很好。我很高兴听到提示)。

现在情况一定是c x xs ~ (x : toList xs) 。但自从 x和xs是不同的通用变量，并且它们是唯一出现在右侧的变量，方程在 Miller's pattern fragment 中，因此 c ~ (\x xs -> x : toList xs)是其最通用的解决方案。

所以，toList必须减少到 (\f -> f (\x xs -> x : toList xs) n)对于一些n 。显然，toList不能有正规形式，因为我们总是可以展开递归发生。