类型代数和高德纳向上箭头表示法



阅读这个问题和这篇博客文章让我更多地思考类型代数,特别是如何滥用它。

基本上,

1) 我们可以将Either A B类型视为加法:A+B

2) 我们可以把有序对(A,B)看作乘法:A*B

3) 我们可以把函数A -> B看作幂:B^A

这里有一个明显的模式:乘法是重复加法,求幂是重复乘法。这使得Knuth定义了向上箭头↑作为幂运算,↑↑作为重复的幂运算,↑↑↑重复↑↑,等等。因此,10↑↑↑↑10是一个巨大的数字。

我的问题是:函数↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑用代数数据表示类型?看起来↑应该是一个参数数量不定的函数,但这没有多大意义。A↑B会简单地是[A] -> B,从而A↑↑↑↑B会是[[[[A]]]]->B吗?

如果你能解释Ackerman函数或任何其他超增长函数的样子,那就有加分了。

在最明显的级别上,您可以识别↑↑b带

((...(a -> a) -> ...) -> a)  -- iterated b times

和↑↑↑b只是

(a↑↑(a↑↑(...(a↑↑(a↑↑a))...))) -- iterated b times

所以所有的东西都可以用一些长函数类型来表示(因此是一些超长元组类型…)。但我认为没有一个方便的表达式可以用熟悉的Haskell类型(除了上面用...写的)的基数来表示任意的向上箭头符号,因为我想不出任何常见的数学对象对底层集的大小有大于指数的组合依赖性(如果不考虑递归数据类型,它们太大了)。。。组合集合论中可能存在这样的对象?(在我看来,你的问题更多的是关于集合的大小,而不是任何特定于类型的问题。)

(你链接的维基百科页面已经将这些对象连接到阿克曼函数。)

最新更新