Относительно доменной структуры метрическая структура дает вам дополнительные данные о наборе носителей. По сути, вы можете сравнить любые два элемента метрического пространства, и, кроме того, вы знаете, насколько эти два элемента различны, тогда как в доменах структура заказа является частичной, и у вас нет количественной оценки того, насколько элементы различаются.
С практической точки зрения, эта дополнительная структура полезна тем, что значительно упрощает решение уравнений области. Еще в 80-х годах было много голландских компьютерных ученых, использующих уравнения метрического пространства для моделирования параллелизма, но это также актуально.
2- нN) ультраметрические пространства - это секретная денотационная жизнь пошаговых моделей. См. Статью Биркедала, Стовринга и Тэмсборга "Теоретико-категоричное решение рекурсивных метрических пространственных уравнений", где приведены некоторые недавние работы в этой области.
Теперь вся эта работа была направлена на получение моделей вообще, но это не единственное, что нас интересует - мы не можем просто заменить частичные порядки метрической структурой в денотационной модели и ожидать, что она будет означать точно то же самое предмет. Поэтому вам может быть интересно, как метрические модели влияют на свойства, такие как полная абстракция, например.
т я м е уплотнительное ˙U тNееN
Эта дополнительная разрешающая способность - это как сила, так и слабость метрических методов. В своей заметке «Пошаговое индексирование: хорошее, плохое и уродливое» Бентон и Хур показывают, что дополнительная структура пошаговых моделей очень полезна для них, чтобы дать доказательства корректности в стиле реализуемости языков программирования, реализованных в терминах плохих языков низкого уровня. Однако дополнительная структура также удерживает их от выполнения оптимизаций, которые в некотором смысле «слишком эффективны», поскольку могут испортить информацию о расстоянии. Так что это помогает и вредит им.
Dе⊥⊥
Тем не менее, вы можете не захотеть этого делать. Например, в моем недавнем исследовании (с Ником Бентоном) я работал над программированием синхронных потоков данных более высокого порядка. Здесь идея заключается в том, что мы можем моделировать интерактивные программы во времени как функции потока. Естественно, мы хотим рассмотреть рекурсивные определения (например, представьте себе написание функции, которая получает поток чисел в качестве входных данных и выводит поток чисел, соответствующий сумме элементов потока, замеченных до сих пор).
Но явная цель этой работы состоит в том, чтобы гарантировать, что разрешены только обоснованные определения, и в то же время разрешены рекурсивные определения. Итак, я моделирую потоки как ультраметрические пространства и функционирую на них как нерасширенные карты (кроме того, это обобщает условие причинности реактивного программирования). Согласно метрике, которую я использую, защищенное определение для потоковых функций соответствует сжимающей функции на потоках, и поэтому по теореме Банаха о неподвижной точке существует единственная фиксированная точка. Интуитивно понятно, что свойство уникальности означает, что вычисление фиксированных точек работает одинаково независимо от того, с какого элемента пространства мы начинаем, поэтому в результате мы можем вычислить фиксированные точки сжимающих функций в пространстве, даже если пространство не имеет минимального элемент в смысле теории области.