類型代數和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的向上箭頭符號

回答

相關問題