Co możemy udowodnić za pomocą nieskończonych wykresów, że bez nich nie możemy udowodnić?

Jest to kontynuacja pytanie na ten temat nieskończonych wykresach.

Odpowiedzi i komentarze do tego pytania zawierają listę obiektów i sytuacji, które są naturalnie modelowane przez nieskończone wykresy. Ale istnieją również liczne twierdzenia o grafach nieskończonych (patrz rozdział 8 w książce Diestela), z których na przykład bardzo popularny jest nieskończony lemat Koeniga .

Teraz mam następujące pytanie: Co możemy udowodnić za pomocą nieskończonych wykresów, że nie możemy udowodnić bez nich? A dokładniej, jaki jest przykład, w którym modelujemy coś jako graf nieskończony, a następnie powołujemy się na twierdzenie o grafach nieskończonych, a ostatecznie udowodniliśmy coś o pierwotnym problemie - nie wiedząc, jak to udowodnić inaczej?

Oto przykład z przetwarzania rozproszonego:

1. Tło

1.1 Asynchroniczny model pamięci współdzielonej

Rozważmy zbiór rozproszonych węzłów komunikujących się za pomocą zmiennych pamięci współużytkowanej. Istnieje przeciwnik, który kontroluje, kiedy węzeł podejmuje kroki i kiedy dostarcza wiadomości. Obliczenia są asynchroniczne , tzn. Przeciwnik może opóźnić kroki węzłów o dowolną (skończoną) ilość czasu.
Można myśleć o kroku węzła jako przejściu stanu jego lokalnego automatu (zgodnie z algorytmem), w którym następny stan jest określony przez aktualny stan i obserwacje węzła od ostatniego kroku.

1.2 Bezpieczeństwo i żywotność

Podczas formalnego wnioskowania o właściwościach algorytmu asynchronicznego rozróżniamy właściwości bezpieczeństwa i żywotności. Nieformalnie właściwość bezpieczeństwa może być interpretowana jako gwarancja, że ​​nigdy nie wydarzy się coś „złego”. (Na przykład dla wzajemnego wykluczenia właściwością bezpieczeństwa byłoby to, że żadne dwa węzły nie wchodzą jednocześnie do sekcji krytycznej.) Z drugiej strony, żywotność można interpretować jako „coś dobrego w końcu się wydarzy”, np .: każdy węzeł ostatecznie się kończy.

${M}$$M$$\alpha,\beta \in M$$2^{-n}$$n$$\alpha$$\beta$

$S$$P\subseteq M$$P$$M\setminus P$

Stosowanie lematu Infinity Koeniga

Nie zawsze łatwo jest stwierdzić, czy określona właściwość jest właściwością bezpieczeństwa: Rozważ implementację obiektów atomowych do odczytu / zapisu na podstawowych zmiennych pamięci wspólnej. Taka implementacja powinna obsługiwać żądania i ich odpowiedzi w taki sposób, aby wyglądały, jakby zdarzyły się w pewnym momencie i nie naruszały kolejności wywoływania. (Ze względu na działanie asynchroniczne rzeczywisty czas między żądaniem a odpowiedzią może być różny od zera). Atomowość jest również znana jako Linearyzowalność . Sekcja 13.1 [A] daje dowód, że atomowość jest właściwością bezpieczeństwa. Dowód wykorzystuje lemat Koeniga, aby pokazać, że granica dowolnej nieskończonej sekwencji egzekucji (z których każda spełnia Atomowość) również spełnia Atomowość.

[A] N. Lynch. Algorytmy rozproszone. Morgan Kaufmann, 1996.