7.5: Топос типів поведінки
- Page ID
- 66443
Тепер, коли ми обговорили логіку в топосі снопа, ми повертаємося до нашого мотивуючого прикладу, топосу типів поведінки. Почнемо з обговорення топологічного простору, на якому типами поведінки будуть снопи, простір, який називається інтервальною областю.
Зауваження 7.75. Зауважте, що вище ми дуже інтуїтивно думали про час, наприклад, коли ми обговорювали людей, які турбуються про новини. Тепер ми будемо думати про час по-іншому, але немає необхідності змінювати свої відповіді або переглядати інтуїтивне мислення, зроблене вище.
7.5.1 Інтервальний домен
Інтервальна область\(\mathbb{I}\)\(\mathbb{R}\) - це специфічний топологічний простір, який ми будемо використовувати для моделювання інтервалів часу.
Іншими словами, нас буде цікавити категорія Shv (\(\mathbb{I}\)\(\mathbb{R}\)) снопів на інтервальній області.
Щоб дати топологічний простір, потрібно дати пару (X, Op), де X - набір «точок», а Op - топологія на X; див. Визначення 7.25.
Множина точок для\(\mathbb{I}\)\(\mathbb{R}\) - це те, що всіх скінченних замкнутих інтервалів
\(\mathbb{I}\)\(\mathbb{R}\):= {[d, u]\(\subseteq\)\(\mathbb{R}\) | d ≤ u}.
Для a < b in\(\mathbb{R}\) давайте o\(_{[a,b]}\) позначимо множину o\(_{[a,b]}\) := {[d, u]\(\in\)\(\mathbb{I}\)\(\mathbb{R}\) | a < d ≤ u < b}; вони називаються базові відкриті набори. Топологія Op визначається цими основними відкритими множинами тим, що підмножина U відкрита, якщо це об'єднання деякої колекції основних відкритих множин.
Так, наприклад, o\(_{[0,5]}\) є відкритою множиною: вона містить кожен [d, u], що міститься у відкритому інтервалі {x\(\in\)\(\mathbb{R}\) | 0 < x < 5}. Аналогічно\(_{[4,8]}\) це і відкритий набір, але зверніть увагу, що\(_{[0,5]}\)\(\bigcup\) \(_{[4,8]}\)\(\neq\)йти далі\(_{[0,8]}\). Дійсно, інтервал [2, 6] знаходиться в правій частині, але не ліворуч.
1. Поясніть, чому [2, 6]\(\in\) o\(_{[0,8]}\).
2. Поясніть, чому [2, 6]\(\not \in\) o\(_{[0,5]}\)\(\bigcup\) o\(_{[4,8]}\). ♦
Нехай Оп позначають відкриті набори ІК, як описано вище, а нехай БТ: = Шв (\(\mathbb{I}\)\(\mathbb{R}\), Оп) позначають топос снопів на цьому просторі.
Ми називаємо це топосом типів поведінки. Існує важливий підпростір\(\mathbb{I}\)\(\mathbb{R}\), а саме звичайний простір дійсних чисел\(\mathbb{R}\).
Ми бачимо\(\mathbb{R}\) як підпростір\(\mathbb{I}\)\(\mathbb{R}\) через ізоморфізм
\(\mathbb{R}\)\(\cong\){[d, u]\(\in\)\(\mathbb{I}\)\(\mathbb{R}\) | д = у}.
Ми обговорювали звичайну топологію на\(\mathbb{R}\) прикладі 7.26, але ми також отримуємо топологію,\(\mathbb{R}\) оскільки вона є підмножиною\(\mathbb{I}\)\(\mathbb{R}\); тобто у нас є топологія підпростору, як описано у Вправі 7.32. Вони згодні, так як читач може перевірити.
Показати, що підмножина U\(\subseteq\)\(\mathbb{R}\) відкрита в топології підпростору,\(\mathbb{R}\)\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) якщо U\(\mathbb{R}\) відкритий у звичайній топології на\(\mathbb{R}\) визначеній у прикладі 7.26. ♦
7.5.2 Снопи на\(\mathbb{I}\)\(\mathbb{R}\)
Ми не можемо заглиблюватися в більшу глибину про сноп топос BT = Shv (\(\mathbb{I}\)\(\mathbb{R}\), Op), з міркувань простору; ми посилаємо зацікавленого читача до розділу 7.6. У цьому розділі ми коротко обговоримо, що означає бути снопом\(\mathbb{I}\)\(\mathbb{R}\), наводячи кілька прикладів, включаючи класифікатор підоб'єктів.
Що таке сноп на\(\mathbb{I}\)\(\mathbb{R}\)? Сніп S на інтервальній області (\(\mathbb{I}\)\(\mathbb{R}\), Op) є функтором S: Op\(^{op}\) → Set: він призначає кожному відкритому множині U множину S (U); як ми повинні це інтерпретувати? Елемент s\(\in\) S (U) - це те, що говорить, що це «подія, яка відбувається протягом усього інтервалу U». Враховуючи це U-подія s разом із відкритою підмножиною V\(\subseteq\) U, існує V -подія s |,\(_{V}\) яка говорить нам, що таке s, якщо ми розглядаємо це як подію, що відбувається протягом V.
Якщо U =\(\bigcup_{i \in I} U_{i}\) і ми можемо знайти відповідні U\(_{i}\) -події (s\(_{i}\)) для кожного i\(\in\) I, то умова сніпа (визначення 7.35) говорить про те, що вони мають унікальне склеювання, тобто
A U -подія\(\in\) s S (U), яка охоплює всі з них: s | (_ {U_ {i}}}\) = s\(_{i}\) для кожного i\(\in\) I. Ми сказали в розділі 7.5.1, що кожен відкритий набір U\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) може бути записаний як об'єднання основних відкритих наборів o\(_{[a,b]}\).
Це означає, що будь-який сніп S визначається його значеннями S (o\(_{[a,b]}\)) на цих основних відкритих множинях. Крім того, умова снопа передбачає, що вони постійно змінюються в певному сенсі, що ми можемо висловити формально як
\(S\left(o_{[a, b]}\right) \cong \lim _{\epsilon>0} S\left(o_{[a-\epsilon, b+\epsilon]}\right)\)
Однак замість того, щоб вникати в подробиці, опишемо кілька видів снопів, які можуть представляти інтерес.
Для будь-якого набору A існує сніп A\(\in\) Shv (\(\mathbb{I}\)\(\mathbb{R}\)), який присвоює кожному відкритому множині U множина A (U) := A. Це дозволяє нам посилатися на цілі числа, або дійсні числа, або букви алфавіту, ніби вони були поведінкою. Що за поведінка 7\(\in\) N? Це така поведінка, яка ніколи не змінюється: це завжди сім. Таким чином A називається постійним сніпом на А.
Виправте будь-який топологічний простір (X, Op\(_{X}\)). Потім йде сніп F\(_{X}\) локальних функцій від\(\mathbb{I}\)\(\mathbb{R}\) до X.
Тобто для будь-якого відкритого множини U\(\in\) Оп\(_{\mathbb{I}\mathbb{R}}\), ми присвоюємо\(_{X}\) множину F (U) := {f: U → X | f безперервне}. Існує також сніп G\(_{X}\) локальних функцій на підпросторі\(\mathbb{R}\)\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\). Тобто для будь-якого відкритого множини U\(\in\) Оп\(_{\mathbb{I}\mathbb{R}}\) ми привласнюємо\(_{X}\) множина G (U) := {f: U\(\mathbb{R}\) → X | f безперервна}.
Давайте перевіримо, що приклад 7.78 має сенс. Виправте будь-який топологічний простір (X, Op\(_{X}\)) та будь-яку підмножину R\(\subseteq\)\(\mathbb{I}\)\(\mathbb{R}\) інтервального домену.
Визначити H\(_{X}\) (U) := {f: U R → X | f є безперервним}.
1. H -\(_{X}\) пресніп? Якщо ні, то чому б і ні; якщо так, то які карти обмежень?
2. Чи\(_{X}\) є Н сніп? Чому чи чому ні? ♦
Ще одне джерело прикладів походить зі світу відкритих гібридних динамічних систем. Це машини, поведінка яких є сумішшю безперервних рухів - як правило, уявляються траєкторіями через векторне поле - і дискретні стрибки. Ці стрибки уявляються викликаними сигналами, які спонтанно надходять. За будь-який проміжок часу гібридна система має певні речі, які вона може робити, і певні речі, які вона не може. Хоча ми не будемо робити це точно тут, існує конструкція для перетворення будь-якої гібридної системи в сніп на ІК; ми наведемо посилання в розділі 7.6.
Ми називаємо снопи\(\mathbb{I}\)\(\mathbb{R}\) як типи поведінки, оскільки майже будь-яка поведінка, яку можна собі уявити, є типом поведінки. Звичайно, складний тип поведінки, такий як те, як хтось діє, коли він закоханий, було б надзвичайно важко записати. Але ідея проста: для будь-якого інтервалу часу, скажімо, триденний інтервал (d, d + 3), нехай L (d, d + 3) позначають їх, щоб падіння можливої поведінки людина, яка закохана може зробити. Очевидно, що це великий, громіздкий набір, і ніхто не хотів би зробити точним. Але в тій мірі, в якій можна уявити, що така поведінка відбувається через час, вони могли уявити собі відповідний сніп.
Суб'єктний класифікатор як сноп на ІК. У будь-якому топосі снопа підпредметний класифікатор Ω сам по собі є сніпом. Він відповідає за значення істини в топосі.
Як ми вже говорили в розділі 7.4.1, коли мова йде про снопи на топологічному просторі (X, Op), значення істинності є відкритими підмножинами U\(\in\) Op.
БТ - топос снопів на просторі (\(\mathbb{I}\)\(\mathbb{R}\), Оп), як визначено в розділі 7.5.1. Як завжди, підоб'єктний класифікатор Ω присвоює будь-якому U\(\in\) Оп множину відкритих підмножин U, тому це значення істинності. Але що вони означають? Ідея полягає в тому, що кожна пропозиція, така як «Боб любить погоду», повертає відкритий набір U, ніби щоб відповісти, що Боб любить погоду «... протягом усього періоду часу U». Давайте вивчимо це трохи більше. Припустимо, Бобу подобається погода протягом усього інтервалу (0, 5) і протягом усього інтервалу (4, 8). Напевно, ми б зробили висновок, що Бобу подобається погода протягом усього інтервалу (0, 8). Але як щодо більш зловісного твердження «одна пара очей залишилася спостерігати за позицією р». Тоді тільки тому, що це правда на (0, 5) і на (4, 8), не означає, що це було правдою на (0, 8): можливо, відбулася зміна зміни, де один спостерігач був звільнений від своєї посади іншим спостерігачем. Як інший приклад розглянемо твердження «фондовий ринок не пішов вниз більш ніж на 10 пунктів». Це може бути вірно на (0, 5) і true on (4, 8), але не на (0, 8). Для того, щоб захопити семантику таких тверджень, як ці твердження, які потребують часу для оцінки, ми повинні використовувати простір,\(\mathbb{I}\)\(\mathbb{R}\) а не простір\(\mathbb{R}\).
7.5.3 Докази безпеки в тимчасовій логіці
Зараз ми маємо принаймні основне уявлення про те, що стає доказом безпеки, скажімо, для автономних транспортних засобів або літаків у національній системі повітряного простору. Насправді, основні ідеї цієї глави вийшли з проекту між MIT, Honeywell Inc., і NASA [SSV18]. Передумовою для проекту було те, що Національна система повітряного простору складається з безлічі різних взаємодіючих систем: взаємодій між літаками, кожна з яких є взаємодією між фізикою, людьми, датчиками та виконавчими механізмами, кожна з яких є взаємодією між ще більш основними частинами. Така ж історія буде триматися для парку автономних транспортних засобів, як у вступі до цієї глави.
Припустимо, що кожна з систем на будь-якому рівні гарантовано задовольнить деяку властивість. Наприклад, можливо, можна припустити, що двигун або відсутній газ, має зламану паливну магістраль, або виконує накази водія чи пілота. Якщо в паливній магістралі стався розрив, датчики будуть сповіщати людину протягом трьох секунд і т.д. кожен з компонентів взаємодіє з рядом різних змінних. У випадку з літаками пілот взаємодіє з радіо, положеннями циферблатів, положенням подрулювального пристрою та візуальними даними перед нею. Компонент тут пілот гарантовано зберігає ці змінні в деякому відношенні: «якщо я щось бачу, я щось скажу» або «якщо циферблати знаходяться в положенні bad_pos, я буду залучати подрулювач протягом 1 секунди». Ми називаємо ці гарантії поведінки контрактами.
Все перераховане вище можна захопити в топос БТ типів поведінки. Змінні - це типи поведінки: висотомір - це змінна, значення якої θ\(\in\)\(\mathbb{R}\)\(_{≥0}\) постійно змінюється щодо часу. Підрулюючий пристрій також є постійно мінливою змінною, значення якої знаходиться в діапазоні [0, 1] і т.д.
Гарантовані відносини поведінкових контрактів задаються предикатами на змінних. Наприклад, якщо пілот завжди включатиме підрулюючий пристрій протягом однієї секунди з дисплея, що знаходяться в позиції bad_pos, це може бути захоплено предикатом p: циферблати × підрулювачі → Ω. Хоча ми не виписали формальну мову для p, можна було б уявити присудок p (D, T) для D: циферблатів та T: підрулювачів як
\ (\ begin {вирівняний}
\ для всіх (t:\ mathbb {R}). @_ {t} &\ left (\ ім'я оператора {bad} _ {-}\ ім'я оператора {pos} (D)\ праворуч)\ Стрілка вправо\\
&\ існує (r:\ mathbb {R})\ cdot (0 <r<1)\ клин\ для всіх\ ліворуч (r^ {\ prime}:\ mathbb {R}\ праворуч)\ cdot 0\ leq r^ {\ прайм}\ leq 5\ Стрілка вправо @_ {t+r+r^ {\ прайм}} (\ текст {зайнятий} (Т)).
\ кінець {вирівняний}\) (7.82)
Тут @\(_{t}\) - це модальність, як ми обговорювали у Визначенні 7.69; насправді це виявляється одним із типу 3. з Пропозиції 7.71, але ми не можемо перейти до цього. Для пропозиції q твердження @\(_{t}\) (q) говорить, що q вірно в деякому досить невеликому районі навколо t. Отже (7.82) говорить: «Починаючи протягом однієї секунди кожного разу, коли циферблати говорять, що ми знаходимося в поганому положенні, я буду залучати подрулювачі протягом п'яти секунд».
Враховуючи фактичне відтворення поза подіями протягом періоду часу U, тобто фактичного розділу D\(\in\) циферблатів (U) та секції T\(\in\) підрулювачів (U), присудок Eq. (7.82) буде триматися на певних частинок U, а не на інших, і це істинне значення р. Сподіваємось, пілот підтримує свій контракт на поведінку в усі часи, коли вона летить, і в цьому випадку значення істини буде вірним протягом усього цього інтервалу U. Але якщо пілот розриває її контракт через певні проміжки часу, то цей факт записується в Ω.
Логіка дозволяє нам записувати аксіоми, подібні до того, що показано в еквалайзері (7.82), а потім міркувати з них: наприклад, якщо пілот і літак, і принаймні один з трьох радарів дотримується свого контракту, то безпечне поділ буде збережено. Ми не можемо дати більш детальну інформацію тут, але ці питання були детально опрацьовані в [SS18]; див. Розділ 7.6.