Topografía efectiva

En matemáticas, el topos efectivo ${\mathsf {Eff}}$ Introducido por Martin Hyland ( 1982 ) captura la idea matemática de efectividad dentro del marco teórico de categorías .

Preliminares

Realizabilidad de Kleene

El topos se basa en el álgebra combinatoria parcial dada por la primera álgebra de Kleene. ${\mathcal {K}}_{1}$ En la noción de realizabilidad recursiva de Kleene , a cualquier predicado se le asignan números de realización, es decir, un subconjunto de ${\mathbb {N} }$ . Las proposiciones extremales son $\top$ y $\bot$ , realizado por ${\mathbb {N} }$ y $\{\}$ Sin embargo, en general, este proceso asigna más datos a una proposición que un simple valor de verdad binario .

Una fórmula con $k$ Las variables libres darán lugar a un mapa en $({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}$ cuyos valores son subconjuntos de los números de realización correspondientes.

Topología de realizabilidad

${\mathsf {Eff}}$ es un ejemplo paradigmático de un topos realizable . Se trata de una clase de topoi elementales con una lógica interna intuicionista que satisface una forma de elección dependiente . Generalmente no son topoi de Grothendieck.

En particular, el topos efectivo es ${\mathsf {RT}}({\mathcal {K}}_{1})$ Se puede decir que otras construcciones de topos de realizabilidad abstraen algunos aspectos desempeñados por ${\mathbb {N} }$ aquí.

Definición

Existen varias formas de construir el topos efectivo, por ejemplo, mediante la noción de tripos, o como la completitud ex/reg de la categoría de ensamblajes . A continuación se presenta una definición explícita completamente desarrollada. ^{[ 1 ]}^{: 115}

Un objeto del topos efectivo es un conjunto $X$ equipado con una función $E:X^{2}\to {\mathcal {P}}(\mathbb {N} )$ que cumplen ciertas condiciones. Denotamos $n\in E(x,y)$ por $n\Vdash x=y$ . (La notación no está estandarizada; el uso de la $=$ El símbolo sobrecarga su significado normal, de manera similar a la notación. $P(X=Y)$ en teoría de la probabilidad .) De manera informal, esto significa que $n$ es un testigo computacional, o realizador de la igualdad $x=y$ Las condiciones que deben cumplirse son las siguientes:

Debe existir un programa $e$ de tal manera que para todos $n\in \mathbb {N}$ y $x,y\in X$ , si $n\Vdash x=y$ luego la salida de $e$ en $n$ , es decir, $\phi _{e}(n)$ (dónde $\phi _{e}$ es el $e$ -ésima función computable parcial ), se define y $\phi _ {e}(n)\Vdash y=x$ En resumen, $e$ toma un realizador de $x=y$ y produce un realizador de $y=x$ (a pesar de $x,y$ ). (Tenga en cuenta que $e$ no puede depender de $x,y$ y solo recibe al realizador de $x=y$ como entrada, sin más información sobre $x$ y $y$ .)
De manera similar, debe existir un programa que tome un realizador de $x=y$ y un realizador de $y=z$ y produce un realizador de $x=z$ (a pesar de $x,y,z$ ).

Un realizador de $x=x$ será llamado más simplemente un realizador de $x$ .

Una relación funcional de un objeto $X$ a un objeto $Y$ es una función $f:X\times Y\to {\mathcal {P}}(\mathbb {N} )$ , nuevamente satisfaciendo ciertas condiciones. Sugerentemente, denotamos . $n\in f(x,y)$ por $n\Vdash f(x)=y$ (de nuevo, esta es una notación especial; $f(x)$ no tiene significado por sí mismo). Esto significa informalmente que $n$ se da cuenta del hecho de que $f$ envía $x$ a $y$ , o “se da cuenta $f(x)=y$ Las condiciones son las siguientes:

Existe un programa que toma un realizador de $f(x)=y$ y produce un realizador de $x$ y un realizador de $y$ (a pesar de $x\in X,y\in Y$ ).
Existe un programa que toma un realizador de $f(x)=y$ y realizadores de $x=x'$ y $y=y'$ y produce un realizador de $f(x')=y'$ (a pesar de $x,x',y,y'$ ).
Existe un programa que toma a los realizadores de $f(x)=y$ y $f(x)=y'$ y produce un realizador de $y=y'$ (a pesar de $x,y,y'$ ).
Existe un programa $e$ de tal manera que para todos $x\in X$ y para todos los realizadores $n$ de $x$ , existe algo $y\in Y$ de tal manera que la salida $\phi _{e}(n)$ se da cuenta $f(x)=y$ .

Suponer $f$ es una relación funcional de $X$ a $Y$ y $g$ es una relación funcional de $Y$ a $Z$ . La composición $g\circ f$ es la relación funcional de $X$ a $Z$ definido por dejar que los realizadores de $(g\circ f)(x)=z$ sean los códigos de pares $(r,s)$ de tal manera que, para algunos $y\in Y$ , tenemos $r\Vdash f(x)=y$ y $s\Vdash g(y)=z$ . La relación funcional de identidad $\operatorname {id}$ sobre un objeto $X$ se define dejando que los realizadores de $\operatorname {id} (x)=y$ ser simplemente los realizadores de $x=y$ .

Los morfismos de $X$ a $Y$ en el topos efectivo son las relaciones funcionales de $X$ a $Y$ , cociente para identificar $f$ y $g$ cuando existe un programa que mapea realizadores de $f(x)=y$ a los realizadores de $g(x)=y$ (a pesar de $x,y$ ), y otro programa que asigna realizadores de $g(x)=y$ a los realizadores de $f(x)=y$ La composición de morfismos se induce en los cocientes mediante la composición a nivel de relaciones funcionales, y lo mismo ocurre con los morfismos identidad.

Relación con los ensamblajes

El topos efectivo surge como una completación de la categoría más simple de ensamblajes .

Un ensamblaje es un conjunto $X$ equipado con una función $R:X\to {\mathcal {P}}(\mathbb {N} )$ . Denotamos $n\in R(x)$ por $n\Vdash x$ , leer " $n$ se da cuenta $x$ ”. Cada asamblea $X$ puede ser interpretado como un objeto del topos efectivo, al declarar que $n$ se da cuenta $x=y$ cuando $x$ y $y$ son realmente iguales y $n$ los realiza en la asamblea $X$ . (Por lo tanto, los realizadores de $x$ en $X$ como objeto del topos efectivo, es decir, los realizadores de $x=x$ , son exactamente los realizadores de $x$ en $X$ como una asamblea.)

Un morfismo de ensamblajes $f:X\to Y$ es una función $f:X\to Y$ entre los conjuntos subyacentes de tal manera que exista un programa, independiente de $x\in X$ , que mapea a los realizadores de $x$ a los realizadores de $f(x)$ . Tal morfismo da lugar a un morfismo en el topos efectivo, representado por la relación funcional (todavía denotada $f$ ) dónde $f(x)=y$ se realiza si y solo si $f(x)$ en realidad es igual a $y$ y luego los realizadores de $f(x)=y$ son los pares de un realizador de $x$ y un realizador de $y$ .

Esta correspondencia convierte la categoría de ensamblajes en una subcategoría completa del topos efectivo.

La categoría de conjuntos es una subcategoría completa de la categoría de ensamblajes, a través del functor $\nabla$ que mapea un conjunto $X$ al ensamblaje con conjunto subyacente $X$ donde cada elemento se realiza mediante cada número natural. En particular, la categoría de conjuntos es también una subcategoría completa del topos efectivo. ^{[ 1 ]}^{: 117}

Operaciones categóricas en el topos efectivo

El topos efectivo es un topos elemental con objetos de números naturales . Esto significa que admite una serie de construcciones categóricas estándar, que se realizan explícitamente de la siguiente manera.

El objeto inicial es el ensamblaje vacío.
El objeto terminal es el ensamblaje de la unidad, un singleton donde el elemento único se realiza mediante cada número natural.
El objeto de los números naturales es $\mathbb {N}$ donde cada número natural se realiza únicamente por sí mismo.
El producto de dos objetos $X$ y $Y$ es el producto cartesiano de conjuntos $X\times Y$ donde un realizador de $(x,y)$ en $X\times Y$ es el código de un par de un realizador de $x$ y un realizador de $y$ .
El coproducto de $X$ y $Y$ es el coproducto de conjuntos $X+Y$ donde un realizador de $x\in X$ en $X+Y$ es el código de un par de 0 y un realizador de $x$ en $X$ y un realizador de $y\in Y$ en $X+Y$ es el código de un par de 1 y un realizador de $y$ en $Y$ .
El clasificador de subobjetos $\Omega$ es ${\mathcal {P}}(\mathbb {N} )$ donde un realizador de $P=Q$ es un par de un programa que devuelve un elemento de $Q$ dado un elemento de $P$ y un programa que devuelve un elemento de $P$ dado un elemento de $Q$ . No es (isomorfo a) un ensamblaje.

Propiedades

Relación con los conjuntos

Algunos objetos exhiben un predicado de existencia bastante trivial que depende únicamente de la validez de la relación de igualdad. $=$ " de conjuntos, de modo que la igualdad válida se mapea al conjunto superior $\mathbb {N}$ y rechazó los mapas de igualdad a $\{\}$ Esto da lugar a un functor completo y fiel . $\nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}$ fuera de la categoría de conjuntos , que tiene el functor de secciones globales que preserva el límite finito $\Gamma$ como su adjunto izquierdo . Esto se factoriza a través de una incrustación completa y fiel que preserva el límite finito. $\omega$ - ${\mathsf {Sets}}\to {\mathsf {Eff}}$ .

NNO

El topos tiene un objeto de números naturales. $N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle$ con simplemente $E_{\mathbb {N} }(n)=\{n\}$ . Oraciones verdaderas sobre $N$ son exactamente las sentencias realizadas recursivamente de la aritmética de Heyting ${\mathsf {HA}}$ .

Ahora flechas $N\to N$ puede entenderse como las funciones recursivas totales y esto también se cumple internamente para $N^{N}$ . Este último es el par dado por las funciones recursivas totales $\mathrm {TR}$ y una relación tal que $E_{\mathrm {TR} }(f)$ es el conjunto de códigos $e\in {\mathbb {N} }$ para $f$ Este último es un subconjunto de los números naturales, pero no un único elemento, ya que existen varios índices que calculan la misma función recursiva. Por lo tanto, en este caso, la segunda entrada de los objetos representa los datos de realización.

Con $N$ y funciones desde y hacia ella, así como con reglas simples para las relaciones de igualdad al formar productos finitos $\times$ , ahora se pueden definir de forma más amplia las operaciones hereditariamente efectivas. De nuevo se pueden pensar en funciones en $N^{N}$ como lo dan los índices y su igualdad está determinada por los objetos que calculan la misma función. Esta igualdad claramente impone una restricción a $N^{(N^{N})}$ , ya que estas funciones resultan ser solo aquellas funciones computables que también respetan adecuadamente la igualdad mencionada en su dominio. Etcétera. La situación para general $\langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle$ , igualdad (en el sentido de la $E$ Los derechos de propiedad intelectual (en dominio e imagen) deben ser respetados.

Propiedades y principios

Con esto se puede validar el principio de Markov. ${\mathrm {MP} }$ y el principio extendido de la Iglesia ${\mathrm {ECT} }_{0}$ (y una variante de segundo orden de la misma), que se reducen a una simple afirmación sobre un objeto como $N^{N}$ o $(1+1)^{N}$ Esto implica ${\mathrm {CT} }_{0}$ y la independencia de premisas ${\mathrm {IP} }_{0}$ .

Un principio de elección $N^{N}$ relacionado con la continuidad débil de Brouwer falla. Desde cualquier objeto, solo hay una cantidad numerable de flechas a $N$ . $\Omega ^{N}$ cumple con un principio de uniformidad. $N$ no es el coproducto contable de copias de $1$ Este topos no es una categoría de gavillas.

Análisis

El objeto $\langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle$ Es eficaz en un sentido formal y a partir de él se pueden definir secuencias de Cauchy computables . Mediante un cociente, el topos posee un objeto de números reales que no tiene subobjetos decidibles no triviales . Con la elección, la noción de reales de Dedekind coincide con la de Cauchy.

Propiedades y principios

El análisis aquí corresponde a la escuela recursiva del constructivismo. Rechaza la afirmación de que $x\leq 0\lor 0\leq x$ sería válido para todos los reales $x$ Las formulaciones del teorema del valor intermedio fallan y todas las funciones de los números reales a los números reales son demostrablemente continuas . Existe una sucesión de Specker y, por lo tanto, el teorema de Bolzano-Weierstrass falla.

Véase también

Lógica categórica

Referencias

^ Jaap van Oosten (2008) . Realizabilidad: una introducción a su lado categórico . Ciencia Elsevier. ISBN 9780444515841.

Hyland, JME (1982), "El topos efectivo" (PDF) , en Troelstra, AS; Dalen, D. van (eds.), Simposio del centenario de LEJ Brouwer (Noordwijkerhout, 1981) , Estudios de lógica y fundamentos de las matemáticas, vol. 110, Ámsterdam: Holanda Septentrional, págs. 165–216 , doi : 10.1016/S0049-237X(09)70129-6 , ISBN 978-0-444-86494-9, MR 0717245
Kleene, SC (1945). " Sobre la interpretación de la teoría numérica intuicionista". Journal of Symbolic Logic . 10 (4): 109– 124. doi : 10.2307/2269016 . JSTOR 2269016. S2CID 40471120 .
Phoa, Wesley (1992). Introducción a las fibraciones, la teoría de topos, el topos efectivo y los conjuntos modestos (Informe técnico). Laboratorio de Fundamentos de la Informática, Universidad de Edimburgo. CiteSeerX 10.1.1.112.4533 . ECS-LFCS-92-208.
Bernadet, Alexis; Graham-Lengrand, Stéphane (2013). "Una presentación sencilla del topos efectivo". arXiv : 1307.3832 [ cs.LO ].
Corfield, David; Ramesh, Sridhar; Schreiber, Urs; Bartels, Toby; Škoda, Zoran; Shulman, Mike; Trimble, Todd; Roberts, David; Holder, Thomas (22 de enero de 2023) [10 de julio de 2009], effective topos (19.ª ed.), nLab

[van-oosten-1] Jaap van Oosten (2008) . Realizabilidad: una introducción a su lado categórico . Ciencia Elsevier. ISBN 9780444515841.

[ 1 ]