Construcción de números naturales como listas de unidades (posibles objetos infinitos)

Question

Me desconcierta esta pregunta, que se refiere más bien a la relación entre dos enfoques de la teoría de tipos. Sin embargo, se puede acortar a la pregunta :

¿Cuándo es correcto (si es que alguna vez lo es) construir los números naturales como listas de unidades?

Esta es mi línea de pensamiento:

En la teoría de tipos podemos definir el tipo de los números naturales inductivamente:

$\dfrac{\quad}{0 : \mathbb{N}}$ $\dfrac{n : \mathbb{N}}{S(n) : \mathbb{N}}$

Y también existe una regla de inducción matemática:

$$ \frac{C:\mathbb{N} \to \mathrm{Type},b : C(0),i: \forall n \in \mathbb{N}. C(n) \to C(S(n))}{\mathrm{ind}(C,b,i):\forall n \in \mathbb{N} . C(n)} $$

y la recursividad primitiva (que puede demostrarse a partir de la inducción natural): $$ \frac{a: X, f:X \to X}{\mathrm{iter}(f,a):\mathbb{N}\to X,\mathrm{prec}(f,a) : (\mathrm{iter}(f,a)(0) =_X a) (\forall n : \mathbb{N} . \mathrm{iter}(f,a)(S(n))=_X f(\mathrm{iter}(f,a)(n))) } $$ Según he entendido, los miembros de este tipo serán equivalentes a los números naturales de la matemática clásica de la teoría de conjuntos. Sin embargo, también podemos definir el tipo de listas $L(T)$ sobre otro tipo $T$ mediante esta expresión algebraica recursiva: $$L(T) = () | (T \times L(T) )$$ Dónde $()$ indica conjunto vacío. Me pareció natural que pudiéramos reescribir nuestra definición de los números naturales como $\mathbb{N}' = L(()) = 0 | (0 \times\mathbb{N}')$ (Habiendo $0 = ()$ para garantizar $0 \in \mathbb{N} $ ) . Es decir, representarlos como listas de unidades. Sin embargo, en algunos lenguajes de programación como Haskell, las listas infinitas se considerarán objetos propios de tipo $L(T)$ . Esto significa que $\mathbb{N}'$ contendrá una secuencia infinita de unidades o desde el punto de vista de la teoría de conjuntos, $\mathbb{N}' = \mathbb{N} \cup \{ \infty \}$ . Si vemos esto $\infty$ entonces podemos ver que $S(\infty) =\infty$ . Así que $\mathbb{N}'$ no son construcción propia de números naturales. Al principio pensé que esto se debía a la diferencia entre definiciones recursivas e infuctivas. Sin embargo, Wikipedia dice que son lo mismo, así que ahora mismo estoy confundido. Sin embargo, puede darse el caso de que las listas infinitas sean miembros de tales tipos inductivos sólo en Haskell, y no en una teoría de tipos reales (para la que se propuso la primera definición de números naturales). ¿Dónde hay un error en mi razonamiento?

Gracias.

p. s.

Parece que la mejor lectura para este tema es la siguiente ensayo de Veronica Gaspes

actualizar:

Resulta que se puede demostrar para $\mathbb{N}$ por recursión primitiva que $1 \neq 0$ y luego por inducción matemática que $\forall n \in \mathbb{N} . n \neq \infty$ donde $\infty$ se define mediante la relación recursiva $\infty = S(\infty) $ . Así que podemos demostrar con una maquinaria muy básica que $\infty \not \in \mathbb{N}$ . Por otro lado, existe otro monstruo: una secuencia de infinitos tal que $\infty : \mathbb{N} \to \mathbb{N}$ , $\infty(S(n)) = S(\infty(n))$ . Básicamente, una secuencia decreciente infinita de números naturales. Demostrar que no existe equivaldrá a afirmar que todo subconjunto de naturales tiene el menor elemento, lo que a su vez equivaldrá a la ley del medio excluido. Así que ahora puedo ver tres soluciones:

1. Constructivismo estricto: condena a ambos $\infty$ y $\infty(n)$ ser no constructiva. Así que esperamos tener $\mathbb{N} \cong \mathbb{N}'$ . Como precio también prohibiremos la lista infinita y algunas otras construcciones coinductivas o al menos tendremos que redefinirlas de forma más compleja.
2. Enfoque clásico: Aceptar la ley del medio excluido. Entonces podemos demostrar que $\infty(n)$ no es miembro de $\mathbb{N}$ . Sin embargo, todavía tendremos que demostrar propiedades de $\mathbb{N}'$ . Sus propiedades dependerán de cómo definamos las propiedades de $\times$ producto en la definición de $\mathbb{N}'$
3. Números no productivos: Aceptar la existencia de $\infty(n)$ como axioma. Lo que hará que la inducción se comporte de forma extraña.

Answer 1

Creo que el problema en tu razonamiento está en asumir que cuando defines un tipo de listas $L(T)$ por $L(T) = ()|(T \times L(T))$ que esto de alguna manera captura la construcción inductiva de listas finitas, Como te diste cuenta, no lo hace. Esta construcción en Haskell no es la misma que la construcción de un conjunto definido inductivamente en fundamentos matemáticos.

Tenemos una definición inductiva para los naturales: un número natural es 0, o es S seguido de un número natural. Podemos escribir esto en forma Backus-Naur como una gramática:

< N > := 0 | "S" < N >

Pero, cuando esto se lee como una definición inductiva, dice que un objeto coincide en el lado izquierdo si y sólo si existe una secuencia finita de aplicaciones de la gramática -un árbol de análisis sintáctico finito- para verificarlo. La definición de "definición inductiva" incluye este requisito de finitud. Así pues, la definición inductiva no da el tipo completo $L(T)$ de arriba - sólo algunos elementos de ese tipo cumplen la definición inductiva, a saber, los que tienen un árbol de análisis sintáctico finito.

El ensayo de Veronica Gaspes utiliza una terminología (matemáticamente) no estándar. No existen "números naturales infinitos" como su infty en la página 3. Por supuesto, la discusión de la evaluación perezosa en Haskell está bien, y infty es un objeto fino de cierto tipo. Pero no implica seriamente que infty es un número natural. (Del mismo modo, NaN es un valor legal para un número de coma flotante, pero esto no hace que NaN sea un número real).