Đọc qua this question và this blog post giúp tôi suy nghĩ thêm về đại số loại và cụ thể cách lạm dụng nó.Loại đại số và ký hiệu mũi tên lên Knuth
Về cơ bản,
1) Chúng ta có thể nghĩ đến loại Either A B như bổ sung: A+B
2) Chúng ta có thể nghĩ về cặp ra lệnh (A,B) như phép nhân: A*B
3) Chúng ta có thể nghĩ của hàm A -> B là lũy thừa: B^A
Có một mô hình rõ ràng đang diễn ra ở đây: Phép nhân ion được lặp lại, và lũy thừa là phép nhân lặp lại. Điều này dẫn đến Knuth to define the up arrow ↑ là lũy thừa, ↑↑ là lũy thừa lặp lại, ↑↑↑ lặp lại ↑↑, v.v. Do đó, 10 ↑↑↑↑ 10 là số HUGE.
Câu hỏi của tôi là: làm cách nào chức năng ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ được thể hiện trong dữ liệu đại số loại? Dường như ↑ nên là một hàm có số lượng đối số vô hạn, nhưng điều đó không có ý nghĩa gì nhiều. A↑B chỉ đơn giản là [A] -> B và do đó A↑↑↑↑B là [[[[A]]]]->B?
Điểm thưởng nếu bạn có thể giải thích những gì Ackerman function sẽ trông như thế nào hoặc bất kỳ số nào khác trong số hypergrowth functions.
Tôi không nghĩ rằng điều này có thể được thực hiện một cách thực sự kinh điển. Việc xác định 'aˣ' với' x-> a' đã là một chút đặc biệt, chỉ thay vì _happens_ có isomorphy giữa 'a'' và' aˣ + a'' cũng như 'a'' và' (aˣ) ʸ' . Nhưng những đẳng thức này không chính xác về mặt kinh điển. – leftaroundabout