En efecto, existe una conexión muy estrecha entre el teorema del punto fijo de Lawvere y el teorema de la recursión, pero hay que verlo de la manera correcta. En concreto, todo se aclara una vez que lo hacemos en el topos efectivo.
Empecemos recordando el teorema de Lawvere. (Utilizo $X \to Y$ y $Y^X$ como sinónimos del conjunto de todas las funciones de $X$ a $Y$ .)
Teorema (Lawvere): Si $e : A \to B^A$ es onto entonces cada $f : B \to B$ tiene un punto fijo.
Prueba. Hay $x \in A$ tal que $e(x)(y) = f(e(y)(y))$ para todos $y \in A$ porque $e$ es sobre y $x \mapsto f(e(y)(y))$ es un mapa de $A$ a $B$ . Entonces $e(x)(x) = f(e(x)(x))$ así que $e(x)(x)$ es un punto fijo de $f$ . QED.
Aquí está el teorema de Recurrencia escrito de manera que sea lo más parecido al teorema de Lawvere. A continuación explico por qué este es el teorema de Recursión.
Teorema de recursión: Supongamos que la elección contable se mantiene y $e : \mathbb{N} \to B^{\mathbb{N}}$ está en. Entonces cada relación total $R \subseteq B \times B$ tiene un punto fijo.
Decimos que $x \in B$ es el punto fijo de $R$ si $R(x,x)$ . Obsérvese que las relaciones totales también pueden verse como mapas multivaluados, por lo que se trata de un teorema de punto fijo que generaliza el caso del teorema de punto fijo de Lawvere en el que $A = \mathbb{N}$ .
Prueba. Porque $R$ es total, para cada $n \in \mathbb{N}$ hay $y \in B$ tal que $R(e(n)(n), y)$ . Por lo tanto, por elección contable, existe un mapa $c : \mathbb{N} \to B$ tal que $R(e(n)(n), c(n))$ para todos $n \in \mathbb{N}$ . Como $e$ es que existe $k \in \mathbb{N}$ tal que $e(k) = c$ . Pero entonces $e(k)(k)$ es un punto fijo de $R$ porque $e(k)(k) = c(k)$ . QED.
Por supuesto, te estás preguntando qué tiene que ver el teorema con el teorema de recursión de la teoría de la computabilidad. Nótese que la prueba es intuicionista y utiliza la elección contable, por lo que es válida en el topos efectivo. Para obtener la conexión con el teorema de recursión clásico, necesitamos entender cómo es el objeto de los mapas parciales computables en el topos efectivo. De hecho, no es más que el espacio de funciones $\mathbb{N} \to \mathbb{N}_\bot$ donde realmente no quiero entrar en la definición interna de $\mathbb{N} _{\bot}$ permítanme describirlo como un conjunto numerado: el conjunto subyacente de $\mathbb{N} _\bot$ es $\mathbb{N} \cup \lbrace \bot \rbrace$ . Un número $r$ realiza $\bot \in \mathbb{N} _\bot$ si el $r$ -la máquina de Turing diverge en la entrada $0$ y realiza $n \in \mathbb{N} _\bot$ si el $r$ -la máquina de Turing se detiene y sale $n$ en la entrada $0$ .
Otra forma de explicar el objeto de los mapas parciales computables $\mathbb{N} \to \mathbb{N} _\bot$ en el topos efectivo es que éste es el objeto de aquellos mapas parciales cuyo dominio es un subconjunto contable de $\mathbb{N}$ (que, por supuesto, no es más que la versión interna del teorema clásico de que los mapas parciales computables tienen conjuntos c.e. como dominios).
De todos modos, $\mathbb{N} \to \mathbb{N}_\bot$ es contable en el topos efectivo. Esto puede demostrarse a partir de los axiomas de computabilidad sintética, pero un atajo es simplemente observar que existe una enumeración efectiva de mapas parcialmente computables, que realiza una enumeración $\varphi : \mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)$ en el topos efectivo.. Pero entonces, ya que por $\lambda$ -cálculo $$(\mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)) \cong (\mathbb{N} \times \mathbb{N} \to \mathbb{N} _\bot) \cong \mathbb{N} \to \mathbb{N} _\bot$$ vemos que podemos aplicar el teorema de recursión a $\mathbb{N} \to \mathbb{N} _\bot$ . Por lo tanto, dado cualquier $f : \mathbb{N} \to \mathbb{N}$ , considere la relación total $R$ definido en $\mathbb{N} \to \mathbb{N} _\bot$ por $$R(u,v) \iff \exists k \in \mathbb{N} . u = \varphi_k \land v = \varphi_{f(k)}.$$ Hay un punto fijo $u$ por lo que por definición de $R$ hay $k$ tal que $u = \varphi_k$ y $u = \varphi_{f(k)}$ . Y tenemos como consecuencia el teorema de recursión habitual.
Hagamos otro, sólo para convencerte de que esto es el teorema de recursión. Hay una enumeración $W$ de todos los subconjuntos contables de $\mathbb{N}$ (sí, hay un número contable de subconjuntos de $\mathbb{N}$ en el topos efectivo, y eso es un axioma genial si te gusta fumar cosas raras). Un ejercicio típico de teorema de recursión pide $n$ tal que $W_n = \lbrace{ n \rbrace}$ . Porque los subconjuntos contables de $\mathbb{N}$ satisfacen la condición del teorema de recursividad, obtenemos dicho conjunto simplemente considerando la relación total $R$ definido por $$R(S,T) \iff \exists m \in \mathbb{N} . S = W_m \land T = \lbrace m\rbrace.$$ En efecto, un punto fijo es un conjunto contable $S$ tal que para algunos $m$ tenemos $S = W_m$ y $S = \lbrace m \rbrace$ .
Podría seguir, pero de hecho estoy preparando un artículo sobre esto que debería aparecer en arXiv en un par de días. Véase también mi material en computabilidad sintética (el material más antiguo tiene pruebas subóptimas del teorema de recursión).
