Primeiro, um comentário. Sua pergunta depende de como geometricamente você pretende significar a palavra "métrica". É razoavelmente comum usar a ultrametria na semântica e na análise estática, mas a ultrametria tende a ter uma interpretação combinatória e não geométrica. (Essa é uma variante da observação de que a teoria do domínio tem o sabor de um uso combinatório e não geométrico da topologia.)
Dito isto, vou dar um exemplo de como isso aparece nas provas do programa. Primeiro, lembre-se de que em uma prova de programa, queremos mostrar que uma fórmula que descreve um programa é válida. Em geral, essa fórmula não precisa necessariamente ser interpretada com os booleanos, mas pode ser extraída dos elementos de alguma estrutura de valores de verdade. Então uma fórmula verdadeira é apenas uma que é igual ao topo da rede.
Além disso, ao especificar programas muito auto-referenciais (por exemplo, programas que fazem uso extensivo de código auto-modificador), as coisas podem ficar muito difíceis. Em geral, queremos fornecer uma especificação recursiva do programa, mas pode não haver uma estrutura indutiva óbvia sobre a qual basear a definição. Para resolver esse problema, geralmente é útil equipar a estrutura do valor verdade com estrutura métrica extra. Então, se você puder mostrar que o predicado cujo ponto fixo você deseja é estritamente contrativo, poderá recorrer ao teorema do ponto fixo de Banach para concluir que o predicado recursivo desejado está bem definido.
O caso com o qual estou mais familiarizado é chamado de "indexação por etapas". Nesse cenário, consideramos nossa estrutura dos valores de verdade como subconjuntos de N fechados para baixo , cujos elementos podemos interpretar livremente como "os comprimentos das seqüências de avaliação nas quais a propriedade se mantém". Reuniões e uniões são interseções e uniões, como sempre, e, como a estrutura está completa, também podemos definir a implicação de Heyting. A treliça também pode ser equipada com um ultramétrico, deixando a distância entre dois elementos da treliça ser 2 - n , onde n é o menor elemento em um conjunto, mas não no outro.ΩN2−nn
Então, o mapa de contração de Banach thoerem nos diz que um predicado contrativo tem um ponto fixo único. Intuitivamente, isso diz que, se podemos definir um predicado que vale para n + 1 etapas usando uma versão que vale para n etapas, então na verdade temos uma definição inequívoca de predicado. Se mostrarmos que o predicado é igual a ⊤ = N , sabemos que o predicado sempre se aplica ao programa.p:Ω→Ωn+1n⊤=N
Como alternativa aos CPOs mais usados, Arnold e Nivat exploraram (métricos) espaços métricos como domínios da semântica denotacional [1]. Em sua tese, Bonsangue [2] explorou dualidades entre essa semântica denotacional e semântica axiomática. Menciono aqui porque fornece uma imagem geral muito abrangente.
[1]: A Arnold, M Nivat: Interpretações métricas de árvores infinitas e semântica de programas recursivos não determinísticos. Theor. Comput. Sci. 11: 181-205 (1980).
[2]: Dualidade topológica MM de vários idiomas em Semântica, volume 8 do ENTCS, Elsevier 1998.
fonte
Aqui está um (de, coincidentemente, o topo da minha fila de leitura):
Swarat Chaudhuri, Sumit Gulwani e Roberto Lublinerman. Análise de continuidade de programas. POPL 2010.
Os autores fornecem uma semântica denotacional para uma linguagem imperativa com loops simples, interpretando expressões como funções de valores em um espaço métrico do produto subjacente. O objetivo é determinar quais programas representam funções contínuas, mesmo na presença de "se" e loops. Eles ainda permitem perguntas sobre continuidade restrita a certas entradas e saídas. (Isso é importante para analisar o algoritmo de Dijkstra, que é contínuo no comprimento do caminho, mas não no caminho real.)
Ainda não vi nada que exija um espaço métrico - parece que poderia ter sido feito usando topologia geral até agora -, mas estou apenas na página 3. :)
fonte
Desculpas por adicionar outra resposta, mas esta não está relacionada à minha outra acima.
Os espaços métricos que eu costumo usar para irritar (ou educar?) Os alunos de simultaneidade são os de traços infinitos. A topologia que induz é precisamente a que Alpern e Schneider [1] usaram para caracterizar as propriedades de segurança e vivacidade como limite fechado e denso, respectivamente.
Em retrospecto, percebo que essa resposta também não possui o ingrediente essencial de uma estrutura de treliça ou poset. Contudo, essa estrutura de treliça está presente quando se move um nível acima do que Clarkson e Schneider chamam de hiperproperties [2]. No momento em que escrevo, não está claro para mim como elevar a métrica.
[1] B Alpern e FB Schneider. Definindo vivacidade. IPL, 21 (4): 181-185, 1985.
[2] MR Clarkson e FB Schneider. Hiperproperties. CSF, p51-65, IEEE, 2008.
fonte