W teorii domen, do czego można wykorzystać dodatkową strukturę występującą w przestrzeniach metrycznych?

Rozdział Smytta w podręczniku logiki w informatyce i inne źródła opisują, w jaki sposób przestrzeni metrycznych można użyć jako domen. Rozumiem, że pełne przestrzenie metryczne dają unikalne stałe punkty, ale nie rozumiem, dlaczego przestrzenie metryczne są ważne. Byłbym wdzięczny za wszelkie przemyślenia na następujące pytania.

Jakie są dobre przykłady wykorzystania przestrzeni metrycznej (ultra / quasi / pseudo) w semantyce? W szczególności dotyczy dowolnego przykładu: Dlaczego potrzebujemy struktury metryk? Czego brakuje -CPO, których dostarcza metryka?$\omega$

Ponadto: Czy unikalna właściwość stałego punktu jest ważna? Jaki jest dobry przykład?

Dzięki!

W stosunku do struktury domeny struktura metryk zapewnia dodatkowe dane dotyczące zestawu nośnych. Zasadniczo możesz porównać dowolne dwa elementy przestrzeni metrycznej, a ponadto wiesz, jak bardzo dwa elementy są różne, podczas gdy w domenach struktura zamówień jest częściowa i nie masz ilościowej miary, jak bardzo różnią się elementy.

Pragmatycznie, ta dodatkowa struktura jest przydatna, ponieważ znacznie ułatwia rozwiązywanie równań domen. W latach 80. wielu holenderskich informatyków używało równań przestrzeni metrycznej do modelowania współbieżności, ale jest to również przedmiotem zainteresowania.

Jeśli obserwujesz zwykłe miejsca (POPL / ICFP / ESOP / itp.), Zauważysz, że tak zwane modele indeksowane krokowo są obecnie wielkim biznesem, ponieważ pozwalają ci dać modele języków z kombinacjami funkcji (takie jak impredykatywny polimorfizm i stan wyższego rzędu), które są trudne do wyleczenia za pomocą klasycznych modeli teoretycznych. Jednak konstrukcje zastosowane w tych modelach są nawiedzająco podobne do rozwiązywania równań domenowych i naturalne jest zastanawianie się, do cholery, jakie jest połączenie. Lars Birkedal i jego współpracownicy wpadli na ogólny pomysł, że rozwiązywanie równań domenowych na przecinanie na dwie części (tj. Odległości między dowolnymi dwoma punktami mają postać dla niektórych$2^{-n}$$n$) przestrzenie ultrametryczne to tajne życie denotacyjne modeli o indeksie skokowym. Zobacz pracę Birkedala, Stovringa i Thamsborga „Teoretyczne rozwiązanie rekurencyjnych metrycznych równań przestrzeni”, aby zapoznać się z najnowszymi pracami w tej dziedzinie.

Teraz cała ta praca koncentrowała się na uzyskiwaniu modeli, ale nie jest to jedyna rzecz, która nas interesuje - nie możemy po prostu zastąpić zamówień częściowych strukturą metryczną w modelu denotacyjnym i oczekiwać, że będzie to oznaczać dokładnie to samo rzecz. Zastanawiasz się więc, jaki wpływ mają modele metryczne na właściwości, takie jak na przykład pełna abstrakcja.

Escardo pokazał w swoim artykule z 1999 r. „Metryczny model PCF”, że prosty model metryczny PCF był odpowiedni, ale nie w pełni abstrakcyjny - dodatkową strukturę metryczną można wykorzystać do modelowania stałych przekroczenia limitu czasu. Konkretnie, możesz wymodelować stałą która spowodowałaby błąd, gdyby nie powrócił lub mniej. Są to informacje, które model metryki może zobaczyć, ponieważ ma informacje o odległości, ale są to informacje, których model domeny nie może, ponieważ kolejność informacji nie mówi „jak oszacowana” jest wartość.$\mathrm{timeout}\;n\;e$$e$$n$

Ta dodatkowa moc rozdzielania jest zarówno siłą, jak i słabością technik metrycznych. W notatce „Indeksowanie kroków: dobre, złe i brzydkie” Benton i Hur pokazują, że dodatkowa struktura modeli indeksowanych krokowo jest dla nich bardzo przydatna, aby dać dowody poprawności w stylu wykonalności języków programowania zaimplementowanych w kategoriach złych języków niskiego poziomu. Jednak dodatkowa struktura uniemożliwia im także wykonywanie optymalizacji, które są w pewnym sensie „zbyt skuteczne”, ponieważ mogą zepsuć informacje o odległości. Więc to im pomaga i boli.

EDYCJA: Powinienem również podać przykład, kiedy twierdzenie Banacha o przestrzeni punktowej przestrzeni metrycznych może być przydatne. W domenach znajdujemy punkty stałe w zasadzie przez twierdzenie Kleene'a o punkcie stałym. Mówi to, że jeśli mamy wskazaną domenę i ciągłą funkcję , iteracja z daje nam najmniej ustalony punkt. Twierdzenie to nie zawiera żadnych twierdzeń o wyjątkowości stałych punktów w ogóle - iteracja po czymś innym niż może dać nam inne stałe punkty. Jeśli więc chcesz rozważyć definicje rekurencji w domenie, nie masz innego wyboru, jak przyznać się do nieterminacji.$D$$f$$\bot$$\bot$

Jednak możesz tego nie chcieć. Na przykład w moich własnych ostatnich badaniach (z Nickiem Bentonem) pracowałem nad programowaniem synchronicznego przepływu danych wyższego rzędu. Tutaj chodzi o to, że możemy modelować programy interaktywne w czasie jako funkcje strumieniowe. Oczywiście chcemy rozważyć definicje rekurencyjne (na przykład wyobraźmy sobie pisanie funkcji, która odbiera strumień liczb jako dane wejściowe i generuje strumień liczb odpowiadający sumie elementów strumienia widzianych do tej pory).

Jednak wyraźnym celem tej pracy jest zapewnienie, aby dozwolone były tylko dobrze uzasadnione definicje, przy jednoczesnym dopuszczeniu definicji rekurencyjnych. Tak więc modeluję strumienie jako przestrzenie ultrametryczne i funkcjonuję na nich jako nie ekspansywne mapy (na marginesie, to uogólnia warunek przyczynowości programowania reaktywnego). Zgodnie z metryką, której używam, strzeżona definicja funkcji strumienia odpowiada funkcji skurczowej w strumieniach, a zatem według twierdzenia Banacha o punkcie stałym istnieje unikalny punkt stały. Intuicyjnie właściwość unikatowości oznacza, że ​​obliczanie punktów stałych działa tak samo bez względu na to, od jakiego elementu przestrzeni zaczynamy, dzięki czemu możemy obliczyć stałe punkty funkcji skurczowych na przestrzeni, nawet jeśli przestrzeń nie ma minimalnego element w sensie teorii domen.