类型代数和Knuth的向上箭头符号

通过this question和this blog post的阅读让我思考更多关于类型代数，特别是如何滥用它。类型代数和Knuth的向上箭头符号

基本上，

1），我们可以认为Either A B类型添加量：A+B

2），我们可以认为有序对(A,B)的乘法：A*B

3）我们可以认为的函数A -> B指数：B^A

这里有一个明显的模式：Multiplicat离子是重复加法，并且指数是重复乘法。这导致Knuth to define the up arrow↑作为指数，↑↑作为重复指数，↑↑↑作为重复的↑↑，等等。因此，10↑↑↑↑10是一个很大的数字。

我的问题是：如何能在功能↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑代数数据类型来表示？看起来↑应该是一个具有无限多个参数的函数，但这没有多大意义。 A↑B只是[A] -> B，因此A↑↑↑↑B是[[[[A]]]]->B？

奖励积分，如果你可以解释Ackerman function看起来像什么，或者其他hypergrowth functions。

来源

2012-11-01 Mike Izbicki

我不认为这是可以做到以一种真正的规范的方式。用'x-> a'来识别'aˣ'已经有点临时性了，而只有_happens_在'aˣˣʸ'和'aˣ+aʸ'以及'aˣʸ'和'（aˣ）ʸ'之间同构。但是这些同构并不完全是规范的。 – leftaroundabout

在最显着的水平，你能找出一个↑↑b相

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

和↑↑↑b为刚刚

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

所以一切都可以在一些长期来表示函数类型（因此作为一些非常长的元组类型...）。但是我不认为有任何向上箭头符号的表达方式适用于熟悉的Haskell类型（超出上面用...或↑写的那些）的基数，因为我不能想到任何常见的数学那些对基础集合的大小具有大于指数组合依赖性的对象（不需要递归数据类型，这太大了）......组合集合论中可能有一些这样的对象吗？（你的问题似乎[我]更多套的尺寸不是具体什么类型的。）

（该Wikipedia page you linked已经这些对象连接到阿克曼功能。）

来源

2012-11-01 07:51:36 Fixnum

类型代数和Knuth的向上箭头符号

回答

相关问题