En la teoría de dominios, ¿para qué se puede usar la estructura adicional presente en espacios métricos?

El capítulo de Smyth en el manual de lógica en informática y otras referencias describe cómo los espacios métricos pueden usarse como dominios. Entiendo que los espacios métricos completos dan puntos fijos únicos, pero no entiendo por qué los espacios métricos son importantes. Realmente agradecería cualquier idea sobre las siguientes preguntas.

¿Cuáles son buenos ejemplos del uso de espacios (ultra / cuasi / pseudo) métricos en semántica? En particular relacionado con cualquier ejemplo: ¿Por qué necesitamos la estructura métrica? ¿Qué carecen de -CPOs que los suministros métricos?$\omega$

Además: ¿es importante la propiedad de punto fijo única? ¿Qué es un buen ejemplo?

¡Gracias!

En relación con la estructura del dominio, la estructura métrica le brinda datos adicionales sobre el conjunto de operadores. Básicamente, puede comparar cualquiera de los dos elementos de un espacio métrico y además sabe cuánto dos elementos son diferentes, mientras que en los dominios la estructura del orden es parcial y no tiene una medida cuantitativa de cuánto difieren los elementos.

Pragmáticamente, esta estructura adicional es útil porque hace que resolver ecuaciones de dominio sea mucho más fácil. En los años 80, había muchos científicos informáticos holandeses que usaban ecuaciones espaciales métricas para modelar la concurrencia, pero también es de interés actual.

$2^{-n}$$n$) los espacios ultramétricos son la vida secreta de denotación de los modelos indexados por pasos. Ver el artículo de Birkedal, Stovring y Thamsborg "La solución teórica de categoría de ecuaciones espaciales métricas recursivas" para algunos trabajos recientes en esta área.

Ahora, todo este trabajo se ha centrado en obtener modelos, pero eso no es lo único que nos interesa: no podemos simplemente reemplazar órdenes parciales con estructura métrica en un modelo denotacional y esperar que signifique exactamente lo mismo cosa. Entonces, podría preguntarse cuál es el impacto de los modelos métricos en propiedades como la abstracción completa, por ejemplo.

$\mathrm{timeout}\;n\;e$$e$$n$

Este poder de resolución adicional es tanto la fuerza como la debilidad de las técnicas métricas. En su nota "Step Indexing: the Good, the Bad and the Ugly", Benton y Hur muestran que la estructura adicional de los modelos indexados por pasos es muy útil para dar pruebas de corrección de estilo de realización de lenguajes de programación implementados en términos de malas lenguas de bajo nivel. Sin embargo, la estructura adicional también les impide realizar optimizaciones que son, en cierto sentido, "demasiado efectivas", ya que puede dañar la información de distancia. Por lo tanto, los ayuda y les hace daño.

$D$$f$$\bot$$\bot$

Sin embargo, es posible que no quieras hacer eso. Por ejemplo, en mi propia investigación reciente (con Nick Benton), he estado trabajando en la programación de flujo de datos síncrono de orden superior. Aquí, la idea es que podamos modelar programas interactivos a través del tiempo como funciones de flujo. Naturalmente, queremos considerar definiciones recursivas (por ejemplo, imagine escribir una función que recibe un flujo de números como entradas y genera un flujo de números correspondiente a la suma de los elementos de flujo vistos hasta ahora).

Pero un objetivo explícito de este trabajo es garantizar que solo se permitan definiciones bien fundadas, al tiempo que se permiten definiciones recursivas. Entonces, modelizo flujos como espacios ultramétricos y funciona en ellos como mapas no costosos (como un aparte, esto generaliza la condición de causalidad de la programación reactiva). Según la métrica que uso, una definición protegida en las funciones de flujo corresponde a una función contractiva en los flujos, por lo que, según el teorema del punto fijo de Banach, existe un punto fijo único. Intuitivamente, la propiedad de unicidad significa que calcular puntos fijos funciona igual sin importar con qué elemento del espacio comencemos, por lo que podemos calcular puntos fijos de funciones contractivas en un espacio, incluso si el espacio no tiene un mínimo elemento en el sentido de la teoría del dominio.