haskell - numero - Tipo de álgebra y notación de flecha arriba de Knuth

numero de graham

Question

Al leer esta pregunta y esta publicación del blog, me puse a pensar más en el tipo de álgebra y específicamente en cómo abusar de ella.

Básicamente,

1) Podemos pensar en el tipo Either AB como una adición: A+B

2) Podemos pensar en el par ordenado (A,B) como una multiplicación: A*B

3) Podemos pensar en la función A -> B como exponenciación: B^A

Hay un patrón obvio que está sucediendo aquí: la multiplicación es la suma repetida, y la exponenciación es la multiplicación repetida. Esto llevó a Knuth a definir la flecha hacia arriba ↑ como exponenciación, ↑↑ como exponenciación repetida, ↑↑↑ como repetición ↑↑, y así sucesivamente. Por lo tanto, 10 ↑↑↑↑ 10 es un número ENORME.

Mi pregunta es: ¿cómo se puede representar la función ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ en tipos de datos algebraicos? Parece que ↑ debería ser una función con un número infinito de argumentos, pero eso no tiene mucho sentido. ¿Sería A↑B simplemente [A] -> B y, por lo tanto, A↑↑↑↑B sería [[[[A]]]]->B ?

Puntos de bonificación si puede explicar cómo se vería la función Ackerman , o cualquiera de las otras funciones de hipercrecimiento .

Answer 1

En el nivel más obvio, podrías identificar un ↑↑ b con

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

y un ↑↑↑ b es justo

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

por lo que todo se puede expresar en términos de algún tipo de función larga (por lo tanto, como un tipo de tupla inmensamente larga ...). Pero no creo que haya una expresión conveniente para un símbolo de flecha ascendente arbitrario en términos de (la cardinalidad de) los tipos de Haskell familiares (más allá de los escritos anteriormente con ... o ↑ ), ya que no puedo pensar en ningún objetos matemáticos comunes que tienen dependencias combinatorias mayores que las exponenciales en el tamaño de los conjuntos subyacentes (sin recurrir a tipos de datos recursivos, que son demasiado grandes) ... tal vez haya algunos de estos objetos en la teoría de conjuntos combinatoria. (Su pregunta me parece más sobre el tamaño de los conjuntos que cualquier cosa específica de los tipos).

(La página de Wikipedia que vinculó ya conecta estos objetos a la función Ackermann).