Zastosowania struktur metrycznych na posetach / sieciach w teorii CS

17

Ponieważ termin jest przeciążony, najpierw krótka definicja. Poset jest zbiorem $X$ wyposażonym w częściowy porządek $\le$ . Biorąc pod uwagę dwa elementy $a,b \in X$ , możemy zdefiniować (złączenie) jako ich najmniejszą górną granicę w i podobnie zdefiniować (spełnić) (połączyć) jako największą dolną granicę. $x \vee y$ $X$ $x \wedge y$

Krata to zestaw, w którym dowolne dwa elementy mają unikalne połączenie i unikalne połączenie.

Kraty (w tej formie) pojawiają się w teorii CS w (w skrócie) teorii subodularności (z podzbiorem sieci) i grupowania (sieci podziału), a także w teorii domen (której nie rozumiem zbyt dobrze) i statycznej analiza.

Ale interesują mnie aplikacje, które wykorzystują struktury metryczne na sieciach. Prosty przykład pochodzi z grupowania, w którym dowolna antymonotoniczna funkcja podmodularna (antimonotone oznacza, że jeśli ) indukuje metrykę $f : X \rightarrow R$ $x \le y, f(x) \le f(y)$

d (x, y) = 2 f (x \land y) - f (x) - f (y)

$d(x,y) = 2f(x \wedge y) - f(x) - f(y)$

Metryka ta została szeroko wykorzystana jako sposób porównania dwóch różnych klastrów zestawu danych.

Czy istnieją inne zastosowania sieci, które dbają o struktury metryczne? Byłem zainteresowany aplikacją teorii domen / analizy statycznej, ale jak dotąd nie widziałem potrzeby stosowania wskaźników .

— Suresh Venkat
źródło

12

Najpierw komentarz. Twoje pytanie zależy od tego, jak geometrycznie zamierzasz oznaczać słowo „metryczny”. Użycie ultrametrii w semantyce i analizie statycznej jest dość powszechne, ale ultrametryki mają raczej interpretację kombinatoryczną, a nie geometryczną. (Jest to wariant obserwacji, że teoria domen ma raczej kombinatoryczne niż geometryczne zastosowanie topologii).

Powiedziawszy to, dam ci przykład, jak to się dzieje w proofach programowych. Najpierw przypomnijmy sobie, że w proofie programowym chcemy pokazać, że obowiązuje formuła opisująca program. Ogólnie rzecz biorąc, ta formuła niekoniecznie musi być interpretowana za pomocą boolean, ale można ją wyciągnąć z elementów pewnej sieci wartości prawdy. Zatem prawdziwa formuła to tylko taka, która jest równa górze siatki.

Co więcej, przy określaniu programów samoreferencyjnych (na przykład programów, które szeroko wykorzystują kod samodopasowujący się) sprawy mogą być bardzo trudne. Zazwyczaj chcemy podać rekurencyjną specyfikację programu, ale może nie istnieć oczywista struktura indukcyjna, na której można zawiesić definicję. Aby rozwiązać ten problem, często pomocne jest wyposażenie sieci wartości prawdy w dodatkową strukturę metryczną. Następnie, jeśli możesz wykazać, że predykat, którego żądany punkt stały jest ściśle zwężający, możesz odwołać się do twierdzenia Banacha o punkcie stałym, aby stwierdzić, że żądany rekurencyjny predykat jest dobrze zdefiniowany.

Przypadek, który znam najbardziej, nazywa się „indeksowaniem kroków”. W tym ustawieniu bierzemy naszą siatkę wartości prawdy do zamkniętych w dół podzbiorów , których elementy możemy luźno interpretować jako „długości sekwencji oceny, w których zachowuje się właściwość”. Spotkania i złączenia są jak zwykle skrzyżowaniami i związkami, a ponieważ sieć jest kompletna, możemy również zdefiniować implikację Heytinga. Kratę można również wyposażyć w ultrametryczny, pozwalając, aby odległość między dwoma elementami kratowymi wynosiła , gdzie jest najmniejszym elementem w jednym zestawie, ale nie drugim. $\Omega$ $\mathbb{N}$ $2^{-n}$ $n$

Następnie mapa skurczów Banacha mówi nam, że predykat skurczowy ma unikalny punkt stały. Intuicyjnie oznacza to, że jeśli możemy zdefiniować predykat, który obowiązuje dla kroków, używając wersji, która zawiera dla kroków, to w rzeczywistości mamy jednoznaczną definicję predykatu. Jeśli następnie pokażemy, że predykat jest równy , to wiemy, że predykat zawsze zawiera program. $p : \Omega \to \Omega$ $n+1$ $n$ $\top = \mathbb{N}$

— Neel Krishnaswami
źródło

ah ciekawe. W odpowiedzi na twoje pytanie zależy mi tylko na tym, aby metryka była taka: spełnia nierówności trójkąta. Tak więc ultrametryki są idealnie w porządku. Jednak (i to jest moja wada w tym pytaniu) wydaje mi się, że użycie tej metryki tutaj ma charakter strukturalny, aby uzyskać dostęp do Banacha. Nie przejmujesz się metryką jako taką (a więc rzeczy takie jak przybliżenie metryki lub jej obliczenie są nieistotne). Czy to prawda?

— Suresh Venkat

4

Tak, nie dbamy o metrykę. Jest to w rzeczywistości źródłem dyskomfortu w przypadku modeli metrycznych lub indeksowanych krokowo - dlaczego śledzimy informacje, na których nam tak naprawdę nie zależy? Wykazanie, że model był stabilny w klasie przybliżeń metryki (być może zachowawczej w odniesieniu do kurczliwości) faktycznie zwiększyłoby z nim komfort.

— Neel Krishnaswami

9

Jako alternatywa dla najczęściej używanych CPO, Arnold i Nivat badali (kompletne) przestrzenie metryczne jako dziedziny semantyki denotacyjnej [1]. W swojej pracy Bonsangue [2] badał dualności między semantyką denotacyjną i semantyką aksomatyczną. Wspominam o tym tutaj, ponieważ daje to bardzo kompleksowy ogólny obraz.

[1]: A Arnold, M. Nivat: Metryczne interpretacje nieskończonych drzew i semantyka nie deterministycznych programów rekurencyjnych. Teoria Comput. Sci. 11: 181-205 (1980).
[2]: MM Bonsangue Topological Duality in Semantics tom 8 ENTCS, Elsevier 1998.

— Kai
źródło

Fantastycznie - nie wiedziałem, że ta praca jest online!

— Neel Krishnaswami

3

Daję Marcello (Bonsangue) informację, że mówi się o nim. (Być może dołączy.)

— Dave Clarke

5

Oto jeden (przypadkowo z góry mojej kolejki do czytania):

Swarat Chaudhuri, Sumit Gulwani i Roberto Lublinerman. Analiza ciągłości programów. POPL 2010.

Autorzy podają semantykę denotacyjną dla języka imperatywnego z prostymi pętlami, interpretując wyrażenia jako funkcje na podstawie wartości w podstawowej przestrzeni metrycznej produktu. Chodzi o to, aby określić, które programy reprezentują funkcje ciągłe, nawet w obecności „if” i pętli. Pozwalają nawet na pytania dotyczące ciągłości ograniczone do niektórych danych wejściowych i wyjściowych. (Jest to ważne przy analizie algorytmu Dijkstry, który ma ciągłą długość ścieżki, ale nie rzeczywistą ścieżkę.)

Nie widziałem jeszcze niczego, co wymagałoby przestrzeni metrycznej - wydaje się, że do tej pory można było to zrobić przy użyciu ogólnej topologii - ale jestem tylko na stronie 3. :)

— Neil Toronto
źródło

1

oczywiście nie ma tu posetu ani kraty, jak w poprzedniej odpowiedzi. tego mi brakuje.

— Suresh Venkat

3

Przepraszamy za dodanie kolejnej odpowiedzi, ale ta nie ma związku z moją drugą powyżej.

Przestrzenią metryczną, której rutynowo używam, by drażnić (a może edukować?) Studentów współbieżności, są nieskończone ślady. Indukowana przez niego topologia jest dokładnie tym, którego Alpern i Schneider [1] wykorzystali do scharakteryzowania właściwości bezpieczeństwa i żywotności odpowiednio jako zamknięte i gęste.

\begin{array}{rcl} d : Σ^{ω} \times Σ^{ω} & ⟶ & R_{\geq 0} \\ (σ, τ) & \mapsto & 2^{- sup {i \in N | σ |_{i} = τ |_{i}}} \end{array}

$\begin{array}{@{}rcl} d : \Sigma^\omega\times\Sigma^\omega & \longrightarrow & \mathbb{R}_{{}\ge 0}\\ % (\sigma,\tau) & \mapsto & 2^{-\sup \{~i\in\mathbb{N} ~|~ \sigma|_i = \tau|_i~\}} \end{array}$

σ |_{i}

$\sigma|_i$

σ

$\sigma$

i

$i$

2^{- \infty} = 0

$2^{-\infty} = 0$

Patrząc wstecz, zdaję sobie sprawę, że w tej odpowiedzi również brakuje istotnego składnika struktury sieci lub struktury poety. Taka struktura sieci jest jednak obecna, gdy przechodzimy o jeden poziom wyżej, jak Clarkson i Schneider nazywają hiperproperty [2]. W chwili pisania tego tekstu nie jestem jednak pewien, jak podnieść metrykę.

[1] B Alpern i FB Schneider. Definiowanie żywotności. IPL, 21 (4): 181–185, 1985.
[2] MR Clarkson i FB Schneider. Hyperproperties. CSF, s. 51–65, IEEE, 2008.

— Kai
źródło

\sum_{k = 1}^{n} k = n (n + 1) / 2

$\sum_{k=1}^n k = {n(n+1)}/{2}$

@HCH dzięki, odpowiednio zredagowałem swój post i usunąłem rażące wołanie o porady dotyczące formatowania.

— Kai

Niezła formuła!

— Hsien-Chih Chang 張顯之