Capítulo 14. Semántica de funciones y límites de equivalencia
Cuando dos formulaciones describen «las mismas funciones», ¿qué operación permite recuperar una desde la otra? ¿Se conserva sólo el valor, la composición, la estructura categórica o además la computabilidad? La palabra «equivalencia» no puede sustituir esas verificaciones.
Continuidad. El paso de flechas a gráficas y las reglas de traducción se fijaron en el capítulo 13. Allí ya vimos que una interpretación puede confundir términos y que una inclusión de mapas computables en conjuntos puede ser fiel sin ser plena. Las aplicaciones parciales pertenecen a TF-CAT-006, su clasificador a TF-CAT-008, los traductores de nombres a TF-CAT-009 y las imposibilidades de decidir comportamientos a TF-CAT-010. Este capítulo no identifica ZF, la teoría de tipos y una categoría como teorías globalmente equivalentes. Compara estructuras, funtores y códigos bajo contratos expresos.
14.1. Cuatro niveles de equivalencia
Definición 14.1.1 — Contrato de equivalencia de funciones
Para evitar que una semejanza de notación se convierta en identidad injustificada, distinguimos cuatro afirmaciones con tipos de datos diferentes:
- Equivalencia extensional relativa a dominio y codominio fijados: \(f=g:A\to B\) cuando sus valores coinciden; para aplicaciones parciales también deben coincidir los dominios efectivos.
- Isomorfismo de presentaciones: se especifican biyecciones de objetos o portadores y las aplicaciones se transportan mediante ellas. Un isomorfismo es una afirmación estructural, no una implementación computable.
- Equivalencia categórica: se suministran funtores \(F:\mathcal C\rightleftarrows\mathcal D:G\) e isomorfismos naturales \(GF\cong1_{\mathcal C}\) y \(FG\cong1_{\mathcal D}\). No se exige que los objetos de ambas categorías coincidan literalmente.
- Equivalencia efectiva de representaciones: hay algoritmos uniformes que traducen los nombres válidos en ambas direcciones sin cambiar su denotación; no basta con tener una biyección de conjuntos de nombres.
Cada afirmación obliga a explicitar fuente, destino, igualdad considerada, inversa o recuperación, y principios de construcción. Una equivalencia de categorías no afirma por sí sola que los objetos o sus códigos puedan identificarse computablemente; una equivalencia de nombres no decide por sí sola la igualdad de los objetos nombrados.
Teorema 14.1.2 — Criterio de equivalencia categórica con representantes suministrados
Sean \(\mathcal C,\mathcal D\) categorías localmente pequeñas y \(F:\mathcal C\to\mathcal D\) un funtor. Supóngase que (i) para todos \(A,A'\), la aplicación \(F_{A,A'}:\operatorname{Hom}_{\mathcal C}(A,A')\to\operatorname{Hom}_{\mathcal D}(FA,FA')\) es biyectiva, y (ii) se han suministrado para cada objeto \(D\) un objeto \(G_0D\) de \(\mathcal C\) y un isomorfismo \(\varepsilon_D:F(G_0D)\xrightarrow{\sim}D\). Entonces se construye un funtor \(G:\mathcal D\to\mathcal C\) y se tienen isomorfismos naturales \(FG\cong1_{\mathcal D}\) y \(1_{\mathcal C}\cong GF\). Recíprocamente, un funtor dotado de cuasiinverso y tales isomorfismos es plenamente fiel y esencialmente sobreyectivo. El enunciado inverso sobre esencial sobreyectividad sin datos elegidos no se utiliza aquí como permiso para escoger simultáneamente representantes en ZF sin AC.
Demostración (construcción). En los objetos, pongamos \(GD=G_0D\). Dada \(u:D\to D'\), la plenitud y fidelidad proporcionan una única flecha \(Gu:GD\to GD'\) cuya imagen satisface
\[F(Gu)=\varepsilon_{D'}^{-1}\circ u\circ\varepsilon_D.\tag{14.1}\]
La identidad satisface (14.1) con \(u=1_D\) porque el lado derecho es \(1_{FGD}\); por inyectividad de \(F_{GD,GD}\), \(G(1_D)=1_{GD}\). Si \(u:D\to D'\) y \(v:D'\to D''\), entonces
\[F(Gv\circ Gu)=(\varepsilon_{D''}^{-1}v\varepsilon_{D'})(\varepsilon_{D'}^{-1}u\varepsilon_D) =\varepsilon_{D''}^{-1}(vu)\varepsilon_D=F(G(vu)),\]
y la fidelidad fuerza \(G(vu)=Gv\,Gu\). Así \(G\) es funtor. Reescrita como \(u\varepsilon_D=\varepsilon_{D'}F(Gu)\), (14.1) expresa exactamente la naturalidad de \(\varepsilon:FG\Rightarrow1_{\mathcal D}\).
Para \(A\in\mathcal C\) usemos la biyectividad de \(F_{A,GFA}\) para definir \(\eta_A:A\to GFA\) mediante \(F(\eta_A)=\varepsilon_{FA}^{-1}\). La misma construcción aplicada a \(\varepsilon_{FA}\) produce \(\theta_A:GFA\to A\) con \(F(\theta_A)=\varepsilon_{FA}\); se tiene \(F(\theta_A\eta_A)=1_{FA}\) y \(F(\eta_A\theta_A)=1_{FGFA}\), y por fidelidad ambas composiciones son identidades. Para \(f:A\to A'\), la naturalidad de \(\varepsilon\) con respecto a \(Ff\) da
\[F(GFf)\varepsilon_{FA}^{-1}=\varepsilon_{FA'}^{-1}Ff, \quad\text{luego}\quad GFf\,\eta_A=\eta_{A'}f\]
por fidelidad; \(\eta:1_{\mathcal C}\Rightarrow GF\) es un isomorfismo natural. Se ha construido el cuasiinverso sin una elección adicional: los representantes \(G_0D,\varepsilon_D\) eran datos de entrada, y cada flecha recuperada es única.
Recíproca. Sean \(G,\eta:1\Rightarrow GF\) y \(\varepsilon:FG\Rightarrow1\) isomorfismos naturales. Cada \(D\) es isomorfo a \(FGD\), de modo que la sobreyectividad esencial está provista con testigos. Si \(Ff=Fg\), entonces \(GFf=GFg\) y, por naturalidad de \(\eta\), \(\eta_{A'}f=\eta_{A'}g\), luego \(f=g\); \(F\) es fiel. Para la plenitud, dado \(u:FA\to FA'\), definamos el automorfismo natural de \(F\), \(\beta_A=\varepsilon_{FA}\circ F\eta_A:FA\to FA\). La naturalidad de ambos isomorfismos da \(\beta_{A'}Ff=Ff\beta_A\). Apliquemos \(G\) a \(u'=\beta_{A'}u\beta_A^{-1}\) y pongamos \(h=\eta_{A'}^{-1}\circ G(u')\circ\eta_A\). La naturalidad de \(\varepsilon\) proporciona \(Fh=\beta_{A'}^{-1}u'\beta_A=u\). Luego \(F\) es pleno. No se exigió que los isomorfismos originales satisficieran previamente identidades triangulares: el automorfismo \(\beta\) corrige esa diferencia. \(\square\)
Ejemplo 14.1.3 — Categorías equivalentes sin ser isomorfas
Sea \(\mathcal C\) la categoría terminal con un objeto \(*\) y una flecha. Sea \(\mathcal D\) el grupoide con dos objetos distintos \(0,1\) y exactamente una flecha entre cada par ordenado; por unicidad, cada flecha tiene inversa. El funtor \(F:\mathcal C\to\mathcal D\) envía \(*\) a \(0\). Es pleno y fiel porque \(\operatorname{Hom}_{\mathcal C}(*,*)\) y \(\operatorname{Hom}_{\mathcal D}(0,0)\) son singletons. Ambos objetos de \(\mathcal D\) son isomorfos a \(0\); el funtor \(G\) envía ambos a \(*\) y todas las flechas a \(1_*\). Los isomorfismos \(FGD\to D\) son las flechas únicas de \(0\) a \(D\), y \(GF=1_{\mathcal C}\). Sin embargo, no hay isomorfismo de categorías: un isomorfismo estricto exigiría una función biyectiva entre sus conjuntos de objetos, de cardinalidades uno y dos. Equivalencia no es identidad ni isomorfismo estricto.
Contraejemplo 14.1.4 — Plenitud y fidelidad sin equivalencia
Considérese la inclusión \(I:\mathbf{Set}_{\ne\varnothing}\hookrightarrow\mathbf{Set}\) de la subcategoría plena de los conjuntos no vacíos. Para objetos \(A,B\ne\varnothing\), los hom-conjuntos en ambas categorías son el mismo conjunto de aplicaciones \(A\to B\): \(I\) es pleno y fiel. Pero \(\varnothing\) no es isomorfo a la imagen de ningún conjunto no vacío: una biyección entre ambos implicaría que el conjunto no vacío carece de elementos. Por tanto, \(I\) no es esencialmente sobreyectivo ni equivalencia. La existencia de aplicaciones adecuadas entre los objetos ya presentes no garantiza que el modelo de destino no tenga objetos nuevos.
TF-CAT-006 construye mapas parciales como spans y su codificación en Set (TF-DEF-00021, TF-THM-00051); TF-CAT-008 formula el clasificador \(L(B)\) en topoi y estudia la composición levantada (TF-THM-00062, TF-THM-00068). La presente sección identifica la operación de Kleisli entre mapas etiquetados (TF-DEF-00061), que no debe confundirse con la composición ordinaria de dos flechas de tipos incompatibles. Mapa del recorrido.
14.2. Aplicaciones parciales y la composición que corresponde a su codificación
Definición 14.2.1 — Función parcial etiquetada y composición de Kleisli
En \(\mathbf{Set}\) clásico, para un conjunto \(B\) definimos \(M(B)=B\sqcup\{\bot\}\), donde \(\bot\) lleva una etiqueta disjunta de los elementos de \(B\) (aunque \(B\) ya contenga un símbolo escrito \(\bot\)). Escribimos \(\operatorname{some}(b)\) para la inyección de \(B\) y \(\operatorname{none}\) para la otra sumanda. Una flecha \(u:A\to M(B)\) representa una función parcial \(A\rightharpoonup B\). Para \(u:A\to M(B)\) y \(v:B\to M(C)\), definimos la composición etiquetada por
\[ (v\star u)(a)=\begin{cases}\operatorname{none},&u(a)=\operatorname{none},\\v(b),&u(a)=\operatorname{some}(b).\end{cases}\tag{14.2}\]
Esta operación tiene tipo \(A\to M(C)\); \(v\circ u\) no está, en general, tipada, puesto que el dominio de \(v\) es \(B\) y el codominio de \(u\) es \(M(B)\). La unidad parcial etiquetada es \(\eta_A(a)=\operatorname{some}(a)\).
Teorema 14.2.2 — Correspondencia exacta entre aplicaciones parciales y flechas etiquetadas
En ZF clásico, para cualesquiera conjuntos \(A,B\) existe una biyección
\[\operatorname{Par}_{\mathbf{Set}}(A,B)\ \cong\ \operatorname{Set}(A,M(B)),\tag{14.3}\]
que transporta la composición parcial a \(\star\) y las identidades a \(\eta\). En consecuencia, la categoría de aplicaciones parciales de conjuntos y la categoría cuyos objetos son conjuntos y cuyas flechas \(A\to B\) son funciones \(A\to M(B)\) con composición (14.2) son isomorfas por un funtor identidad en los objetos. No se afirma que sean la categoría ordinaria \(\mathbf{Set}\).
Demostración. Represéntese una aplicación parcial por \(D\subseteq A\) y \(f:D\to B\), identificando pares equivalentes mediante su misma relación gráfica. Definamos
\[\Phi(D,f)(a)=\begin{cases}\operatorname{some}(f(a)),&a\in D,\\\operatorname{none},&a\notin D.\end{cases}\]
En ZF clásico el tercero excluido separa los dos casos; no se escoge ningún valor de una fibra. Recíprocamente, para \(u:A\to M(B)\), pongamos \(D_u=\{a\in A:u(a)\in\operatorname{some}(B)\}\) y \(f_u(a)=b\) cuando \(u(a)=\operatorname{some}(b)\); la inyectividad de la etiqueta hace único ese \(b\). Si \(u(a)=\operatorname{none}\), entonces \(a\notin D_u\). Se sigue por separación de casos que \(\Phi(D_u,f_u)=u\) punto a punto y que \(D_{\Phi(D,f)}=D\) con valores \(f\); las construcciones son inversas.
Sean \((D,f):A\rightharpoonup B\) y \((E,g):B\rightharpoonup C\). La composición parcial está definida exactamente en \(\{a\in D:f(a)\in E\}\) y allí vale \(g(f(a))\), según TF-THM-00043. Si \(a\notin D\), (14.2) devuelve \(\operatorname{none}\); si \(a\in D\) pero \(f(a)\notin E\), también; en el caso restante, (14.2) devuelve \(\operatorname{some}(g(f(a)))\). Por los tres casos, \(\Phi(g\circ_{\mathrm{par}}f)=\Phi(g)\star\Phi(f)\). La identidad total \(1_A\) se convierte en \(\eta_A\). La asociatividad y las leyes de identidad de \(\star\) se transportan desde la categoría de mapas parciales, ya probada; también se verifican directamente separando los casos \(\operatorname{none}\) y \(\operatorname{some}\). El isomorfismo de categorías resulta porque la biyección (14.3) es identidad en objetos y respeta todas las composiciones. \(\square\)
Ejemplo 14.2.3 — Tabla de propagación de la indefinición
Sean \(A=\{x,y\}\), \(B=\{b\}\), \(C=\{c\}\). Póngase \(u(x)=\operatorname{some}(b)\), \(u(y)=\operatorname{none}\) y \(v(b)=\operatorname{some}(c)\). Entonces \((v\star u)(x)=\operatorname{some}(c)\) y \((v\star u)(y)=\operatorname{none}\). La composición conserva el dominio \(\{x\}\) y no «rellena» por defecto el valor de \(y\). Si se pretendiera escribir \(v(u(y))\), se intentaría aplicar una flecha definida en \(B\) a un dato de \(M(B)\): el término ni siquiera tendría el tipo correcto. Pregunta pedagógica: ¿qué valor obtendría \(v\star u\) si \(v(b)=\operatorname{none}\)? Ambos argumentos resultarían indefinidos, y el dominio compuesto sería vacío.
TF-CAT-010 distingue igualdad sintáctica de equivalencia extensional (TF-DEF-00040) y estudia nombres de objetos representados (TF-DEF-00044); TF-CAT-012 separa los índices totales de las funciones que denotan (TF-DEF-00051). Aquí el paso adicional es suministrar traductores computables en ambos sentidos bajo el modelo de realizadores, con la hipótesis exacta de TF-THM-00111. No inferir esa efectividad de un isomorfismo abstracto. Mapa del recorrido.
14.3. Representaciones: mismo objeto no significa mismos algoritmos
Definición 14.3.1 — Sistema de nombres naturales
Como modelo discreto suficiente para exhibir el fenómeno, una representación por nombres naturales de un conjunto \(X\) es una sobreyección parcial \(\delta:D_\delta\subseteq\mathbb N\to X\). Un \(n\in D_\delta\) es un nombre de \(\delta(n)\). Esto es un subcaso de los espacios representados del capítulo 9, cuyos nombres pueden ser secuencias infinitas; no afirmamos que las representaciones mediante naturales cubran todos los espacios representados. Para una función total \(f:X\to Y\), un realizador de \(f\) entre \(\delta_X,\delta_Y\) es un algoritmo parcial \(F\) que termina para cada nombre válido \(n\in D_{\delta_X}\), produce un nombre válido de salida y cumple \(\delta_Y(F(n))=f(\delta_X(n))\). No se exige que termine en entradas inválidas.
Definición 14.3.2 — Reducibilidad y equivalencia computable de representaciones
Para representaciones \(\delta,\gamma\) de un mismo conjunto \(X\), escribimos \(\delta\preceq_c\gamma\) si existe un programa traductor parcial \(T\), definido sobre todos los nombres \(\delta\)-válidos, tal que
\[n\in D_\delta\implies T(n)\in D_\gamma\quad\text{y}\quad\gamma(T(n))=\delta(n).\tag{14.4}\]
Escribimos \(\delta\equiv_c\gamma\) si hay traductores en ambos sentidos. El símbolo \(\preceq_c\) expresa que un nombre \(\delta\) puede convertirse algorítmicamente en uno \(\gamma\); invertir verbalmente el símbolo sin revisar (14.4) induce errores. Los traductores actúan sobre nombres y no necesitan decidir la igualdad de objetos ni disponer de inversas como funciones entre conjuntos de nombres.
Teorema 14.3.3 — Las equivalencias de nombres transportan la computabilidad
La relación \(\preceq_c\) es reflexiva y transitiva; \(\equiv_c\) es una relación de equivalencia. Si \(f:X\to Y\) es computable desde \(\delta_X\) hacia \(\delta_Y\), y se conocen \(\delta'_X\preceq_c\delta_X\) y \(\delta_Y\preceq_c\delta'_Y\), entonces \(f\) es computable desde \(\delta'_X\) hacia \(\delta'_Y\). Por tanto, reemplazar cualquiera de las representaciones de entrada y salida por otras computablemente equivalentes preserva la clase de funciones totales realizables en ambas direcciones.
Demostración. La identidad \(T(n)=n\) verifica reflexividad, y si \(T\) traduce \(\delta\) a \(\gamma\) y \(S\) traduce \(\gamma\) a \(\lambda\), entonces \(S(T(n))\) termina en todo nombre \(\delta\)-válido; además \(\lambda(S(T(n)))=\gamma(T(n))=\delta(n)\). La composición efectiva es un programa por cierre de los programas parciales bajo composición. Esto prueba transitividad y, con simetría incorporada por definición, que \(\equiv_c\) es equivalencia.
Para el transporte de \(f\), sean \(T_X\) el traductor de \(\delta'_X\) a \(\delta_X\), \(F\) un realizador de \(f\) desde \(\delta_X\) a \(\delta_Y\), y \(T_Y\) el traductor de \(\delta_Y\) a \(\delta'_Y\). En cada entrada válida \(n\) el compuesto \(T_Y(F(T_X(n)))\) termina, da un nombre válido de \(Y\), y
\[\delta'_Y(T_Y(F(T_X(n))))=\delta_Y(F(T_X(n)))=f(\delta_X(T_X(n)))=f(\delta'_X(n)).\]
Es, pues, un realizador del mismo \(f\). Usando los traductores contrarios se obtiene la implicación recíproca cuando ambas representaciones son equivalentes. No hay aquí un algoritmo para encontrar traductores a partir de una simple biyección semántica: su existencia efectiva es hipótesis explícita. \(\square\)
Contraejemplo 14.3.4 — Dos nombres biyectivos sin traductor computable
Trabajemos en ZF clásico y fijemos el conjunto de parada no decidible \(K=\{n:V(n,n)\downarrow\}\) de TF-THM-00095. Construyamos la permutación \(p:\mathbb N\to\mathbb N\) que, para cada \(n\), intercambia \(2n\) con \(2n+1\) si \(n\in K\), y deja ambos fijos si \(n\notin K\). Cada pareja es disjunta de las otras y \(p(p(m))=m\); \(p\) es una biyección explícitamente definida como conjunto, sin AC. No es computable: si lo fuera, al calcular \(p(2n)\) y comprobar si es impar se decidiría \(n\in K\).
Sobre el mismo conjunto \(X=\mathbb N\), consideremos las representaciones totales y biyectivas \(\delta_0(m)=m\) y \(\delta_p(m)=p(m)\). Para traducir un nombre \(m\) de \(\delta_0\) a uno de \(\delta_p\), necesariamente \(p(T(m))=m\); al ser \(p^{-1}=p\), necesariamente \(T(m)=p(m)\). Tal traductor no puede ser computable. En el otro sentido la ecuación \(\delta_0(S(m))=\delta_p(m)\) también exige \(S(m)=p(m)\). Así ambas representaciones son isomorfas como presentaciones conjuntistas, incluso biyectivas, pero \(\delta_0\not\equiv_c\delta_p\). En particular, la función identidad \(X\to X\) no es computable en el contrato mixto \((\delta_0,\delta_p)\), aunque sí lo es con \((\delta_0,\delta_0)\) o \((\delta_p,\delta_p)\). La semántica subyacente no determina por sí sola el costo de traducir sus nombres. \(\square\)
14.4. Cocientes semánticos y barreras de decisión
Definición 14.4.1 — Cociente de índices por denotación
Fijada una numeración \(e\mapsto\varphi_e\) de funciones parciales computables \(\mathbb N\rightharpoonup\mathbb N\), definimos \(e\sim e'\) si tienen el mismo dominio y los mismos valores en él. ZF forma el cociente conjuntista \(Q=\mathbb N/{\sim}\) y la proyección \(q:e\mapsto[e]\). El cociente clasifica denotaciones, no programas ni pruebas de igualdad; como conjunto existe por separación y reemplazo. Una codificación computable con igualdad decidible de este cociente requeriría una función total computable \(c:\mathbb N\to\mathbb N\) con
\[c(e)=c(e')\iff e\sim e'.\tag{14.5}\]
Tal requisito es adicional al cociente abstracto. La prueba de factorización por el cociente ya figura en TF-THM-00099; aquí se examina la restricción efectiva.
Teorema 14.4.2 — No existe un cociente universal efectivo con igualdad decidible
No hay función total computable \(c:\mathbb N\to\mathbb N\) que satisfaga (14.5). Más generalmente, tampoco existe una reducción computable total de los índices hacia un sistema de códigos con igualdad decidible que identifique exactamente las clases extensionales de las funciones parciales.
Demostración. Supongamos que existe \(c\). Dados dos índices \(e,e'\), calculemos \(c(e)\) y \(c(e')\), que terminan por totalidad, y comparemos los enteros resultantes, cuya igualdad es decidible. Por (14.5), el procedimiento responde «iguales» si y sólo si \(\varphi_e=\varphi_{e'}\) como aplicaciones parciales. Contradice la indecidibilidad de la equivalencia de índices, demostrada —con un resultado más fuerte de no semidecidibilidad— en TF-THM-00080. Para un sistema de códigos \(C\) con decisor de igualdad, sustitúyase la comparación de enteros por ese decisor; el mismo argumento funciona. La existencia abstracta de \(Q\) no queda cuestionada: lo imposible es añadirle simultáneamente estos datos de computación y decisión en la numeración fijada. \(\square\)
Los elementos generalizados de TF-CAT-002 y las sondas representables de TF-CAT-013 prueban igualdad precomponiendo \(f,g:A\to B\) con \(x:X\to A\). En esta sección, los observadores \(t_i:B\to C_i\) separan flechas postcomponiendo (TF-DEF-00065, TF-THM-00113). TF-CAT-015 distingue formalmente ambas direcciones al estudiar familias generadoras (TF-DEF-00069). No se identifica una familia separadora con un procedimiento de decisión. Mapa del recorrido.
14.5. Observadores y transporte de coordenadas
Definición 14.5.1 — Familia de observadores y separación
Sea \(\mathcal C\) una categoría y sea \((t_i:B\to C_i)_{i\in I}\) una familia especificada de flechas (para una familia pequeña, \(I\) es un conjunto; el enunciado vale asimismo para una colección de sondas bien tipadas). Dos flechas paralelas \(f,g:A\to B\) son indistinguibles por esos observadores cuando \(t_i f=t_i g\) para todo \(i\). La familia es conjuntamente monomórfica si, para todos \(A,f,g\), esta condición implica \(f=g\). No presupone que los observadores constituyan un conjunto completo de funciones ni que su igualdad sea decidible.
Teorema 14.5.2 — Criterio exacto de recuperación por observadores
Una familia \((t_i:B\to C_i)\) distingue todas las flechas con codominio \(B\) si y sólo si es conjuntamente monomórfica. Si contiene \(1_B\), siempre distingue todas las flechas. En cambio, un conjunto de observadores insuficiente puede identificar flechas distintas aunque cada una esté perfectamente definida.
Demostración. Decir que distingue todas las flechas es, por definición expandida, afirmar para todo \(A\) y todas \(f,g:A\to B\) que \([\forall i\;t_i f=t_i g]\Rightarrow f=g\), exactamente la condición de monomorfía conjunta. Si algún \(t_j=1_B\), entonces de \(t_j f=t_jg\) se obtiene \(1_B f=1_Bg\), esto es, \(f=g\) por la ley de identidad. A la inversa, si la familia no es conjuntamente monomórfica, la negación de la implicación universal proporciona, en lógica clásica, testigos \(A,f,g\) con \(f\ne g\) y \(t_i f=t_i g\) para todos los \(i\); aun sin invocar ese paso clásico, la definición indica la obstrucción exacta. No se confunde este criterio de postcomposición con Yoneda elemental, que recupera una flecha por naturalidad de todas las precomposiciones con sondas \(X\to A\). \(\square\)
Ejemplo 14.5.3 — Un observador constante no distingue dos funciones
En \(\mathbf{Set}\), tome \(A=\{*\}\), \(B=\{0,1\}\), \(f(*)=0\), \(g(*)=1\), y el único observador \(t:B\to\{*\}\). Aunque \(f\ne g\), ambas composiciones \(tf,tg\) son la única flecha \(A\to\{*\}\). La familia \(\{t\}\) no es conjuntamente monomórfica. Añadir \(1_B\) separa inmediatamente \(f\) de \(g\). Así la pregunta «¿estas funciones son observacionalmente iguales?» está incompleta hasta declarar qué experimentos están disponibles.
Teorema 14.5.4 — El cambio de coordenadas transporta funciones, pero no por sí solo algoritmos
Sean biyecciones de conjuntos \(e_A:A\xrightarrow{\sim}A'\) y \(e_B:B\xrightarrow{\sim}B'\). La asignación
\[T_{e_A,e_B}:\operatorname{Set}(A,B)\to\operatorname{Set}(A',B'),\quad f\longmapsto e_B\circ f\circ e_A^{-1}\tag{14.6}\]
es biyectiva, con inversa \(h\mapsto e_B^{-1}\circ h\circ e_A\); preserva y refleja la igualdad de funciones. Dados además \(e_C:C\xrightarrow{\sim}C'\), cumple
\[T_{e_A,e_C}(g\circ f)=T_{e_B,e_C}(g)\circ T_{e_A,e_B}(f).\tag{14.7}\]
Sin hipótesis efectivas sobre las biyecciones (y sus inversas) no se infiere que \(T\) preserve la computabilidad.
Demostración. Para cada \(f:A\to B\) se tiene \(e_B^{-1}(e_Bfe_A^{-1})e_A=f\) por las identidades de inversa; para \(h:A'\to B'\) se tiene \(e_B(e_B^{-1}he_A)e_A^{-1}=h\). Las transformaciones son inversas, así que la igualdad se preserva y refleja. Para (14.7), expándase el lado derecho:
\[(e_Cge_B^{-1})(e_Bfe_A^{-1})=e_Cg(e_B^{-1}e_B)fe_A^{-1}=e_Cgf e_A^{-1}.\]
En cuanto a computabilidad, el contraejemplo 14.3.4 suministra una biyección no computable \(p:\mathbb N\to\mathbb N\). Tómense \(A=B=A'=B'=\mathbb N\), \(e_A=1_{\mathbb N}\), \(e_B=p\) y \(f=1_{\mathbb N}\): \(f\) es computable, pero \(T_{e_A,e_B}(f)=p\) no lo es. Si, en cambio, las biyecciones e inversas se realizan por algoritmos en representaciones compatibles, el compuesto (14.6) sí es computable por cierre bajo composición, como en el teorema 14.3.3. El obstáculo no está en las leyes algebraicas, sino en que la presentación puede esconder información no computable. \(\square\)
14.6. Cuadro de control y auditoría fundacional
| Equivalencia alegada | Invariante demostrado | Dato imprescindible | Lo que no se obtiene |
|---|---|---|---|
| Categorías equivalentes | Hom y composición recuperables hasta isomorfismo natural | Cuasiinverso o representantes/isomorfismos ya dados | Igualdad literal de objetos; AC a partir de esencial sobreyectividad |
| Función parcial \(\leftrightarrow A\to B\sqcup\{\bot\}\) | Dominios y valores; composición de Kleisli | En ZF clásico, separación por pertenencia; constructivamente, decisión de dominio o levantamiento adecuado | Composición ordinaria de Set; algoritmo de parada |
| Representaciones \(\delta\equiv_c\gamma\) | Computabilidad total preservada por traducción | Programas traductores en ambas direcciones | Decisión de igualdad semántica |
| Cociente extensional de programas | Una clase por comportamiento | Relación \(e\sim e'\) bien definida | Código computable canónico universal con igualdad decidible |
| Observadores \(t_i\) | Igualdad recuperable si y sólo si son conjuntamente monomórficos | Familia de experimentos explicitada | Separación mediante un observador constante |
| Transporte por isomorfismos | Identidades, composición e igualdad extensional | Biyecciones e inversas | Computabilidad sin realizadores de los cambios de coordenadas |
Lectura guiada (MA-PED). (a) Recupere de (14.1) por qué fidelidad es indispensable para la composición de \(G\). (b) Explique por qué \(\star\) tiene un tipo correcto mientras \(v\circ u\) puede no tenerlo. (c) Para \(p\), calcule \(p(2n)\) bajo las dos hipótesis \(n\in K\) y \(n\notin K\); señale el decisor que surgiría si hubiese un traductor. (d) Identifique dónde el teorema 14.4.2 usa totalidad y dónde usa decidibilidad. (e) Compare las familias \(\{t:B\to1\}\) y \(\{1_B\}\): ¿qué igualdad detecta cada una? (f) Refute la afirmación «si dos conjuntos son isomorfos, todos los algoritmos se transportan» indicando el paso no efectivo de (14.6).
Auditoría matemática. Las pruebas de 14.1.2 separan datos de representantes y existencia débil; ninguna elección global se infiere de la sobreyectividad esencial en solitario. 14.2 presupone \(\mathbf{Set}\) clásico para separar dominios arbitrarios: la presencia de un clasificador de aplicaciones parciales en un topos no convierte automáticamente todo dominio en complementado. 14.3 trabaja con nombres naturales y programas parciales que terminan en nombres válidos; no extiende sin hipótesis la demostración a todos los espacios representados de Baire. 14.4 usa una numeración efectiva fija y equivalencia extensional de funciones parciales; su contradicción es una reducción a la indecidibilidad anterior, no un nuevo axioma. 14.5 distingue postcomposición observacional de precomposición de Yoneda y separa biyección de isomorfismo computable.
Fuentes de cotejo: capítulo 13 y sus referencias; nLab, «Equivalence of categories», https://ncatlab.org/nlab/show/equivalence+of+categories (advierte sobre elección y sobreyectividad esencial); nLab, «Partial function», https://ncatlab.org/nlab/show/partial+function (span monomórfico y mónada de posibilidad); V. Brattka, «Computability over topological structures», https://cca-net.de/vasco/publications/model.pdf, §3 (reducciones y equivalencia efectiva de representaciones). Estos recursos son cotejos conceptuales: las pruebas anteriores declaran hipótesis y desarrollan sus propios argumentos.
Formalización independiente verificada y parcial: PR #118 fusionada en main (cabeza 9541a9d8115a7ee3629abd1b60fcff1befa65fc8, integración a89e73c153ca110a0d1e5794f67b59194f00fddb) tras Lean #53 y Quarto #287 en completed/success para la cabeza final. Cuatro teoremas Lean y una definición cubren la identidad semántica con traductores totales suministrados de TF-THM-00111, sólo el caso de un observador inyectivo en Set de TF-THM-00113 y las identidades algebraicas conjuntistas de TF-THM-00114. No certifican la computabilidad de traductores, equivalencias de categorías abstractas, la construcción Kleisli ni indecidibilidad. Consulte TF-LEAN-014; no se efectuó compilación local.