7.5: Un topos de tipos de comportamiento
- Page ID
- 112333
Ahora que hemos discutido la lógica en una gavilla topos, volvemos a nuestro ejemplo motivador, un topos de tipos de comportamiento. Comenzamos discutiendo el espacio topológico en el que los tipos de comportamiento serán poleas, un espacio llamado dominio de intervalo.
OBSERVACIÓN 7.75. Tenga en cuenta que anteriormente, estábamos pensando muy intuitivamente en el tiempo, por ejemplo, cuando discutimos que la gente estaba preocupada por las noticias. Ahora vamos a estar pensando en el tiempo de una manera diferente, pero no hay necesidad de cambiar tus respuestas o reconsiderar el pensamiento intuitivo hecho anteriormente.
7.5.1 El dominio de intervalo
El dominio de intervalo\(\mathbb{I}\)\(\mathbb{R}\) es un espacio topológico específico, que utilizaremos para modelar intervalos de tiempo.
Es decir, nos interesará la categoría Shv (\(\mathbb{I}\)\(\mathbb{R}\)) de poleas en el dominio de intervalo.
Para dar un espacio topológico, se debe dar un par (X, Op), donde X es un conjunto de 'puntos' y Op es una topología en X; ver Definición 7.25.
El conjunto de puntos para\(\mathbb{I}\)\(\mathbb{R}\) es el de todos los intervalos cerrados finitos
\(\mathbb{I}\)\(\mathbb{R}\):= {[d, u]\(\subseteq\)\(\mathbb{R}\) | d ≤ u}.
Para a < b in\(\mathbb{R}\), vamos a\(_{[a,b]}\) denotar el conjunto o\(_{[a,b]}\) := {[d, u]\(\in\)\(\mathbb{I}\)\(\mathbb{R}\) | a < d ≤ u < b}; estos se llaman conjuntos básicos abiertos. La topología Op está determinada por estos conjuntos abiertos básicos en que un subconjunto U está abierto si es la unión de alguna colección de conjuntos abiertos básicos.
Así, por ejemplo, o\(_{[0,5]}\) es un conjunto abierto: contiene cada [d, u] contenido en el intervalo abierto {x\(\in\)\(\mathbb{R}\) | 0 < x < 5}. Del mismo modo o\(_{[4,8]}\) es un conjunto abierto, pero tenga en cuenta que o\(_{[0,5]}\)\(\bigcup\) o\(_{[4,8]}\)\(\neq\) o o\(_{[0,8]}\). En efecto, el intervalo [2, 6] está en el lado derecho pero no en el izquierdo.
1. Explique por qué [2, 6]\(\in\) o\(_{[0,8]}\).
2. Explique por qué [2, 6]\(\not \in\) o\(_{[0,5]}\)\(\bigcup\) o\(_{[4,8]}\). ♦
Deje que Op denote los conjuntos abiertos de IR, como se describió anteriormente, y dejar que BT: = Shv (\(\mathbb{I}\)\(\mathbb{R}\), Op) denote los topos de poleas en este espacio.
Lo llamamos los topos de los tipos de comportamiento. Existe un subespacio importante de\(\mathbb{I}\)\(\mathbb{R}\), a saber, el espacio habitual de los números reales\(\mathbb{R}\).
Vemos\(\mathbb{R}\) como un subespacio de\(\mathbb{I}\)\(\mathbb{R}\) vía el isomorfismo
\(\mathbb{R}\)\(\cong\){[d, u]\(\in\)\(\mathbb{I}\)\(\mathbb{R}\) | d = u}.
Discutimos la topología habitual\(\mathbb{R}\) en el Ejemplo 7.26, pero también obtenemos una topología\(\mathbb{R}\) porque es un subconjunto de\(\mathbb{I}\)\(\mathbb{R}\); es decir, tenemos la topología subespacial como se describe en el Ejercicio 7.32. Estos concuerdan, como puede comprobar el lector.
Mostrar que un subconjunto U\(\subseteq\)\(\mathbb{R}\) está abierto en la topología subespacial de\(\mathbb{R}\)\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) iff U\(\mathbb{R}\) está abierto en la topología habitual en\(\mathbb{R}\) definida en el Ejemplo 7.26. ♦
7.5.2 Poleas\(\mathbb{I}\)\(\mathbb{R}\)
No podemos profundizar mucho sobre los topos de gavilla BT = Shv (\(\mathbb{I}\)\(\mathbb{R}\), Op), por razones de espacio; remitimos al lector interesado a la Sección 7.6. En esta sección discutiremos brevemente lo que significa ser una gavilla\(\mathbb{I}\)\(\mathbb{R}\), dando algunos ejemplos incluyendo el del clasificador subobjeto.
¿En qué consiste una gavilla\(\mathbb{I}\)\(\mathbb{R}\)? Una gavilla S en el dominio de intervalo (\(\mathbb{I}\)\(\mathbb{R}\), Op) es un functor S: Op\(^{op}\) → Set: asigna a cada conjunto abierto U un conjunto S (U); ¿cómo debemos interpretar esto? Un elemento s\(\in\) S (U) es algo que dice que es un “evento que se lleva a cabo a lo largo del intervalo U”. Dado este U -evento s junto con un subconjunto abierto de V\(\subseteq\) U, hay un V -evento s |\(_{V}\) que nos dice qué es s si lo consideramos como un evento que tiene lugar a lo largo de V.
Si U =\(\bigcup_{i \in I} U_{i}\) y podemos encontrar U\(_{i}\) -eventos coincidentes para cada i\(\in\) I, entonces la condición de gavilla (Definición 7.35) dice que tienen un pegado único, i.e.\(_{i}\)
un U -evento s\(\in\) S (U) que abarca todos ellos: s | (_ {U_ {i}}}\) = s\(_{i}\) para cada i\(\in\) I. Decíamos en la Sección 7.5.1 que cada conjunto abierto U\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) puede escribirse como la unión de conjuntos abiertos básicos o\(_{[a,b]}\).
Esto implica que cualquier gavilla S está determinada por sus valores S (o\(_{[a,b]}\)) en estos conjuntos básicos abiertos. La condición de gavilla implica además que éstas varían continuamente en cierto sentido, lo que podemos expresar formalmente como
\(S\left(o_{[a, b]}\right) \cong \lim _{\epsilon>0} S\left(o_{[a-\epsilon, b+\epsilon]}\right)\)
Sin embargo, en lugar de entrar en los detalles, describimos algunos tipos de poleas que pueden ser de interés.
Para cualquier conjunto A hay una gavilla A\(\in\) Shv (\(\mathbb{I}\)\(\mathbb{R}\)) que asigna a cada conjunto abierto U el conjunto A (U) := A. Esto nos permite referirnos a números enteros, o números reales, o letras de un alfabeto, como si fueran comportamientos. ¿Qué tipo de comportamiento es 7\(\in\) N? Es el tipo de comportamiento que nunca cambia: siempre son siete. Así A se llama la gavilla constante sobre A.
Arreglar cualquier espacio topológico (X, Op\(_{X}\)). Después hay una gavilla F\(_{X}\) de funciones locales desde\(\mathbb{I}\)\(\mathbb{R}\) hasta X.
Es decir, para cualquier conjunto abierto U\(\in\) Op\(_{\mathbb{I}\mathbb{R}}\), asignamos el conjunto F\(_{X}\) (U) := {f: U → X | f es continuo}. También está la gavilla G\(_{X}\) de funciones locales en el subespacio\(\mathbb{R}\)\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\). Es decir, para cualquier conjunto abierto U\(\in\) Op\(_{\mathbb{I}\mathbb{R}}\), asignamos el conjunto G\(_{X}\) (U) := {f: U\(\mathbb{R}\) → X | f es continuo}.
Comprobemos que el Ejemplo 7.78 tenga sentido. Arreglar cualquier espacio topológico (X, Op\(_{X}\)) y cualquier subconjunto R\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) del dominio de intervalo.
Definir H\(_{X}\) (U) := {f: U R → X | f es continuo}.
1. ¿H es\(_{X}\) un presheaf? Si no, por qué no; si es así, ¿cuáles son los mapas de restricción?
2. ¿H es\(_{X}\) una gavilla? ¿Por qué o por qué no? ♦
Otra fuente de ejemplos proviene del mundo de los sistemas dinámicos híbridos abiertos. Se trata de máquinas cuyo comportamiento es una mezcla de movimientos continuos, generalmente imaginados como trayectorias a través de un campo vectorial, y saltos discretos. Estos saltos se imaginan como causados por señales que llegan espontáneamente. En cualquier intervalo de tiempo, un sistema híbrido tiene ciertas cosas que puede hacer y ciertas cosas que no puede. Aunque no vamos a hacer esto preciso aquí, existe una construcción para convertir cualquier sistema híbrido en una gavilla sobre IR; daremos referencias en la Sección 7.6.
Nos referimos a poleas on\(\mathbb{I}\)\(\mathbb{R}\) como tipos de comportamiento porque casi cualquier tipo de comportamiento que uno pueda imaginar es un tipo de comportamiento. Por supuesto, un tipo de comportamiento complejo como la forma en que alguien actúa cuando está enamorado sería extremadamente difícil de anotar. Pero la idea es sencilla: para cualquier intervalo de tiempo, digamos un intervalo de tres días (d, d + 3), dejar que L (d, d + 3) denote estos para caer posibles comportamientos que una persona que está enamorada posiblemente podría hacer. Obviamente es un conjunto grande y poco manejable, y nadie querría hacer precisos. Pero en la medida en que uno pueda imaginar ese tipo de comportamiento como ocurriendo a través del tiempo, podrían imaginar la gavilla correspondiente.
El clasificador subobjeto como gavilla en IR. En cualquier topos de gavilla, el subobjeto clasificador Ω es en sí mismo una gavilla. Es responsable de los valores de verdad en los topos.
Como dijimos en la Sección 7.4.1, cuando se trata de poleas en un espacio topológico (X, Op), los valores de verdad son subconjuntos abiertos U\(\in\) Op.
BT son los topos de poleas en el espacio (\(\mathbb{I}\)\(\mathbb{R}\), Op), como se define en la Sección 7.5.1. Como siempre, el clasificador de subobjetos Ω asigna a cualquier U\(\in\) Op el conjunto de subconjuntos abiertos de U, por lo que estos son los valores de verdad. Pero, ¿qué quieren decir? La idea es que cada proposición, como “A Bob le gusta el clima” le devuelva un set abierto U, como para responder que a Bob le gusta el clima “... a lo largo del periodo de tiempo U”. Exploremos esto un poco más. Supongamos que a Bob le gusta el clima durante todo el intervalo (0, 5) y a lo largo del intervalo (4, 8). Probablemente concluiríamos que a Bob le gusta el clima durante todo el intervalo (0, 8). Pero, ¿qué pasa con la declaración más ominosa “un solo par de ojos se ha quedado mirando la posición p.” Entonces solo porque sea cierto en (0, 5) y en (4, 8), no implica que haya sido cierto en (0, 8): puede haber habido un cambio de turno, donde un vigilante fue relevado de su cargo por otro vigilante. Como otro ejemplo, considere la afirmación “el mercado de valores no bajó en más de 10 puntos”. Esto podría ser cierto en (0, 5) y verdadero en (4, 8) pero no en (0, 8). Para capturar la semántica de enunciados como estos enunciados que tardan en evaluarse debemos utilizar el espacio\(\mathbb{I}\)\(\mathbb{R}\) más que el espacio\(\mathbb{R}\).
7.5.3 Pruebas de seguridad en la lógica temporal
Ahora tenemos al menos una idea básica de lo que implica una prueba de seguridad, digamos para los vehículos autónomos, o aviones en el sistema aéreo nacional. De hecho, las ideas subyacentes de este capítulo salieron de un proyecto entre el MIT, Honeywell Inc., y la NASA [SSV18]. El trasfondo del proyecto fue que el Sistema Nacional de Espacio Aéreo consiste en muchos sistemas diferentes que interactúan: interacciones entre aviones, cada uno de los cuales es una interacción entre física, humanos, sensores y actuadores, cada uno de los cuales es una interacción entre partes aún más básicas. El mismo tipo de historia sostendría para una flota de vehículos autónomos, como en la introducción a este capítulo.
Supongamos que cada uno de los sistemas a cualquier nivel está garantizado para satisfacer alguna propiedad. Por ejemplo, tal vez podamos suponer que un motor está sin gasolina, tiene una línea de combustible rota, o está siguiendo las órdenes de un conductor o piloto humano. Si hay una ruptura en la línea de combustible, los sensores alertarán al humano en tres segundos, etc. Cada uno de los componentes interactúa con una serie de variables diferentes. En el caso de los aviones, un piloto interactúa con la radio, las posiciones de los diales, la posición del propulsor, y los datos visuales frente a ella. El componente aquí el piloto está garantizado para mantener estas variables en alguna relación: “si veo algo, voy a decir algo” o “si los diales están en posición bad_pos, voy a enganchar el propulsor dentro de 1 segundo”. A estas garantías las llamamos contratos de comportamiento.
Todo lo anterior se puede capturar en los topos BT de tipos de comportamiento. Las variables son tipos de comportamiento: el altímetro es una variable cuyo valor θ\(\in\)\(\mathbb{R}\)\(_{≥0}\) está cambiando continuamente con respecto al tiempo. El propulsión también es una variable que cambia continuamente cuyo valor está en el rango [0, 1], etc.
Los contratos de comportamiento de relaciones garantizadas son dados por predicados sobre variables. Por ejemplo, si el piloto siempre activará el propulsor dentro de un segundo de los diales de visualización estando en posición bad_pos, esto puede ser capturado por un predicado p: diales × propulsores → Ω. Si bien no hemos escrito un lenguaje formal para p, uno podría imaginar el predicado p (D, T) para D: diales y T: propulsores como
\ (\ begin {alineado}
\ forall (t:\ mathbb {R}). @_ {t} &\ izquierda (\ nombreoperador {malo} _ {-}\ nombreoperador {pos} (D)\ derecha)\ Derecha\\
&\ existe (r:\ mathbb {R})\ cdot (0<r<1)\ cuña\ forall\ left (r^ {\ prime}:\ mathbb {R}\ derecha)\ cdot 0\ leq r^ {\ prime}\ leq 5\ Rightarrow @_ {t+r+r^ {\ prime}} (\ text {engaged} (T)).
\ end {alineado}\) (7.82)
Aquí @\(_{t}\) es una modalidad, como discutimos en la Definición 7.69; de hecho resulta ser una de tipo 3. de la Proposición 7.71, pero no podemos entrar en eso. Para una proposición q, la declaración @\(_{t}\) (q) dice que q es cierto en algún barrio lo suficientemente pequeño alrededor de t. Entonces (7.82) dice “comenzando dentro de un segundo de cada vez que los diales digan que estamos en una mala posición, voy a enganchar los propulsores durante cinco segundos”.
Dado un juego real fuera de eventos durante un período de tiempo U, es decir,\(\in\) los diales reales de la sección D (U) y los\(\in\) propulsores de la sección T (U), el predicado Ec. (7.82) se mantendrá en ciertas partes de U y no en otras, y esto es el valor de verdad de p. Ojalá la piloto mantenga su contrato de comportamiento en todo momento que esté volando, en cuyo caso el valor de verdad será cierto a lo largo de ese intervalo U. Pero si la piloto rompe su contrato a lo largo de ciertos intervalos, entonces este hecho se registra en Ω.
La lógica nos permite registrar axiomas como el que se muestra en la Ecuación (7.82) y luego razonar a partir de ellos: por ejemplo, si el piloto y el avión, y al menos uno de los tres radares mantiene su contrato entonces se mantendrá la separación segura. No podemos dar más detalles aquí, pero estos asuntos han sido resueltos en detalle en [SS18]; ver Sección 7.6.