Primero, un comentario. Su pregunta depende de cuán geométricamente pretenda que signifique la palabra "métrica". Es razonablemente común usar ultramétricos en semántica y análisis estático, pero los ultramétricos tienden a tener una interpretación combinatoria en lugar de geométrica. (Esta es una variante de la observación de que la teoría de dominio tiene el sabor de un uso combinatorio en lugar de geométrico de la topología).
Dicho esto, te daré un ejemplo de cómo surge esto en las pruebas de programa. Primero, recuerde que en una prueba de programa, queremos mostrar que una fórmula que describe un programa es válida. En general, esta fórmula no necesariamente debe interpretarse con los booleanos, sino que puede extraerse de los elementos de una red de valores de verdad. Entonces, una fórmula verdadera es solo una que es igual a la parte superior de la red.
Además, cuando se especifican programas muy autorreferenciales (por ejemplo, programas que hacen un uso extensivo del código de modificación automática), los asuntos pueden ser muy difíciles. Por lo general, queremos dar una especificación recursiva del programa, pero puede que no haya una estructura inductiva obvia sobre la cual colgar la definición. Para resolver este problema, a menudo es útil equipar la red de valores de verdad con una estructura métrica adicional. Entonces, si puede demostrar que el predicado cuyo punto fijo que desea es estrictamente contractual, puede recurrir al teorema del punto fijo de Banach para concluir que el predicado recursivo que desea está bien definido.
El caso con el que estoy más familiarizado se llama "indexación por pasos". En este contexto, tomamos nuestra red de valores de verdad como subconjuntos cerrados hacia abajo de N , cuyos elementos podemos interpretar libremente como "las longitudes de las secuencias de evaluación en las que se mantiene la propiedad". Las reuniones y las uniones son intersecciones y uniones, como de costumbre, y dado que la red está completa, también podemos definir la implicación de Heyting. La red también se puede equipar con una unidad ultramétrica al permitir que la distancia entre dos elementos de red sea 2 - n , donde n es el elemento más pequeño en un conjunto pero no en el otro.ΩN2−nn
Luego, el mapa de contracción de Banach nos dice que un predicado contractivo tiene un punto fijo único. Intuitivamente, esto dice que si podemos definir un predicado que se cumple para n + 1 pasos usando una versión que se cumple para n pasos, entonces tenemos una definición inequívoca de un predicado. Si luego mostramos que el predicado es igual a ⊤ = N , entonces sabemos que el predicado siempre es válido para el programa.p:Ω→Ωn+1n⊤=N
Como alternativa a los CPO más utilizados, Arnold y Nivat exploraron (métricas) espacios métricos como dominios de semántica denotacional [1]. En su tesis, Bonsangue [2] exploró las dualidades entre la semántica denotacional y la semántica axiomática. Lo menciono aquí porque ofrece una imagen general muy completa.
[1]: A Arnold, M Nivat: Interpretaciones métricas de árboles infinitos y semántica de programas recursivos no deterministas. Theor Comput Sci. 11: 181-205 (1980).
[2]: MM Bonsangue Dualidad topológica en semántica volumen 8 de ENTCS, Elsevier 1998.
fuente
Aquí hay uno (de, casualmente, la parte superior de mi cola de lectura):
Swarat Chaudhuri, Sumit Gulwani y Roberto Lublinerman. Análisis de continuidad de programas. POPL 2010.
Los autores dan una semántica denotacional para un lenguaje imperativo con bucles simples, interpretando expresiones como funciones de valores en un espacio métrico de producto subyacente. El punto es determinar qué programas representan funciones continuas, incluso en presencia de "if" y bucles. Incluso permiten preguntas sobre la continuidad restringida a ciertas entradas y salidas. (Esto es importante para analizar el algoritmo de Dijkstra, que es continuo en su longitud de ruta, pero no en la ruta real).
Todavía no he visto nada que requiera un espacio métrico, parece que podría haberse hecho usando una topología general hasta ahora, pero solo estoy en la página 3. :)
fuente
Disculpas por agregar otra respuesta, pero esta no está relacionada con mi otra anterior.
Un espacio métrico que uso habitualmente para irritar (¿o es educar?) A los estudiantes de concurrencia es el de las huellas infinitas. La topología que induce es precisamente la que Alpern y Schneider [1] usaron para caracterizar las propiedades de seguridad y vitalidad como límite cerrado y denso, respectivamente.
En retrospectiva, me doy cuenta de que esta respuesta también carece del ingrediente esencial de una estructura reticular o poset. Sin embargo, esta estructura reticular está presente cuando se sube un nivel a lo que Clarkson y Schneider llaman hiperpropiedades [2]. Sin embargo, al momento de escribir esto no me queda claro cómo levantar la métrica.
[1] B Alpern y FB Schneider. Definiendo vitalidad. IPL, 21 (4): 181–185, 1985.
[2] MR Clarkson y FB Schneider. Hiperpropiedades CSF, p51-65, IEEE, 2008.
fuente