是否存在折叠scott编码列表的非递归术语？

Question

假设我有一个scott编码的列表,例如:

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是不同的通用变量，并且它们是唯一出现在右侧的变量，因此该方程位于米勒模式片段中，因此c ~ (\x xs -> x : toList xs)是其最通用的解。

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