Funkcje ciągłe Scotta: alternatywna definicja

Naprawdę walczę z tą właściwością:

Niech będą spacjami koherencyjnymi, a będzie funkcją monotoniczną. jest ciągłe wtedy i tylko wtedy, gdy , dla wszystkich takich, że jest zbiorem ukierunkowanym.f : C l ( X ) → C l ( Y ) f f ( ⋃ x ∈ D x ) = ⋃ x ∈ D f ( x ) D ⊆ C l ( X ) $X,Y$$f: Cl(X) \rightarrow Cl(Y)$$f$$f(\bigcup_{x\in D} x)=\bigcup_{x \in D}f(x)$$D \subseteq Cl(X)$$D$

Zestaw kierunkowy jest zdefiniowany w następujący sposób: POSET to zestaw ukierunkowany iff ∀ x , x ′ ∈ D ∃ z ∈ D taki i . oznacza kliki X: coherent .$D \subseteq$$\forall x, x' \in D$ $\exists z \in D$x ′ ⊆ z C l ( X ) { x ⊆ | X | ∣ a , b ∈ x ⇒ a b $x \subseteq z$$x' \subseteq z$
$Cl(X)$$\{x \subseteq |X| \mid a,b \in x \Rightarrow a$$b \}$

Wiele książek podaje to jako ciągłe funkcje Scotta , ale niestety nie mój nauczyciel. Podał nam definicję ciągłości:

$f : Cl(X) \rightarrow Cl(Y)$ jest ciągły iff jest monotoniczny i , gdzie monotoniczny jest zdefiniowany jako: jest monotoniczny iff$\forall x \in Cl(X), \forall b \in f(x), \exists x_0 \subseteq_{fin} x, b \in f(x_0)$
a ⊆ b ⇒ f ( a ) ⊆ f ( b $f$$a \subseteq b \Rightarrow f(a) \subseteq f(b)$

To proponowany dowód, który mam, ale nie rozumiem ostatniego równania.

Dowód ciągłości oznaczaf ( ⋃ D ) = ⋃ f ( D $f$$f(\bigcup D)=\bigcup f(D)$ :
Niech . Zgodnie z definicją ciągłości . Zauważ, że jest związkiem . Jeśli jest bezpośredni, to: a następnie . Z definicji monotonii so (???) . I nawet to prawda powinniśmy pokazać, że , nie tylko∃ x 0 ⊂ f i n x ∣ b ∈ f ( x 0 ) x 0 { x i ∣ x i ∈ D } D ∃ z ∈ D ∣ x i ⊆ z x 0 ⊆ z f ( x 0 ) ⊆ f ( z ) b ∈ $b \in f(\bigcup D)$$\exists x_0 \subset_{fin} x \mid b \in f(x_0)$$x_0$$\{ x_i \mid x_i \in D\}$
$D$$\exists z \in D \mid x_i \subseteq z$$x_0 \subseteq z$$f(x_0)\subseteq f(z)$$b \in f(z)$ $\subseteq \bigcup f(D)$$\bigcup f(D) = f(\bigcup D)$$\subseteq$ .

Dowód innej implikacji jest jeszcze gorszy, więc nie mogę go tutaj napisać ... Czy możesz mi wyjaśnić, w jaki sposób dowód może działać?

Definicja ciągłości stosowana przez twojego nauczyciela jest lepsza. Mówi ci konkretnie, co oznacza ciągłość.

Załóżmy, że . Oznacza to, że biorąc pod uwagę wszystkie informacje o x , być może nieskończony zestaw tokenów (atomów), funkcja wytwarza pewien element zawierający atomową informację b . (Może mieć również inne informacje, ale w tej chwili nie jesteśmy tym zainteresowani.) Definicja twojego nauczyciela mówi, że nie trzeba patrzeć na wszystkie nieskończone informacje x , aby uzyskać informacje wyjściowe b . Wystarczy skończony podzbiór x , aby go wytworzyć.$b \in f(x)$$x$$b$$x$$b$$x$

(Książka Melvina Fittinga „Teoria obliczalności, semantyka i programowanie logiczne”, Oxford, 1987, nazywa tę zwięzłość właściwości i definiuje funkcję ciągłą jako monotoniczną i zwartą.)

To jest istota ciągłości. Aby uzyskać skończoną ilość informacji na temat wyniku funkcji, potrzebujesz tylko skończonej ilości informacji na temat danych wejściowych. Dane wyjściowe wytworzone przez funkcję dla nieskończonego wejścia są uzyskiwane przez złożenie razem informacji, które produkuje dla wszystkich skończonych przybliżeń nieskończonego wejścia. Innymi słowy, nie dostajesz żadnego magicznego skoku, przechodząc od skończonych przybliżeń do ich nieskończonej jedności. Cokolwiek otrzymujesz w nieskończoności, powinieneś już być na pewnym skończonym etapie.

Standardowe równanie jest ładne, ale nie mówi o całej intuicji, którą wyjaśniłem powyżej. Jednak matematycznie jest to odpowiednik definicji nauczyciela.$f(\bigcup_{x \in D} x) = \bigcup_{x \in D} f(x)$

Aby pokazać, że , wystarczy, aby pokazać, że f ( x ) jest zawarte w F ( ⋃ x ∈ D x ) , dla każdego x ∈ D . Ale wynika to bezpośrednio z monotoniczności f, ponieważ x ⊆ ⋃ x ∈ D x . Jest to więc kierunek „łatwy”.$\bigcup_{x \in D} f(x) \subseteq f(\bigcup_{x \in D} x)$$f(x)$$f(\bigcup_{x \in D} x)$$x \in D$$f$$x \subseteq \bigcup_{x \in D} x$

Drugi kierunek, udowodniony przez twojego nauczyciela, jest interesujący: . Aby to zobaczyć, skorzystaj z intuicji, o której wspomniałem powyżej. Każda informacja atomowa b po lewej stronie pochodzi z pewnego skończonego przybliżenia wejścia: x 0 ⊆ f i n ⋃ x ∈ D x . To znaczy, b ∈ f ( x 0 ) . Ponieważ x $f(\bigcup_{x \in D} x) \subseteq \bigcup_{x \in D} f(x)$$b$$x_0 \subseteq_{fin} \bigcup_{x \in D} x$$b \in f(x_0)$$x_0$jest skończony i jest zawarty w unii zbioru kierowanego, musi być coś w zestawie kierowanym, który jest większy niż , być może sam x 0 . Nazwij ten element z . Przez monotoniczność, f ( x 0 ) ⊆ f ( z ) . Więc b ∈ f ( z ) . Ponieważ z ∈ D , f ( z ) ⊆ ⋃ x ∈ D f ( x ) . Więc teraz $x_0$$x_0$$z$$f(x_0) \subseteq f(z)$$b \in f(z)$$z \in D$$f(z) \subseteq \bigcup_{x \in D} f(x)$$b$widać również po prawej stronie. CO BYŁO DO OKAZANIA.

Jak zauważyłeś, wykazanie, że ciągłość nauczyciela implikuje ładne równanie, jest łatwe. Trudniej jest pokazać, że ładne równanie, choć wygląda na to, że nie mówi zbyt wiele, naprawdę mówi wszystko w definicji twojego nauczyciela.

Z opóźnieniem przyszło mi do głowy, po tym jak napisałem ostatnią odpowiedź, że definicja ciągłości nauczyciela, którą wyjaśniłam w mojej odpowiedzi, jest topologicznym pojęciem ciągłości. Algebraiczne sformułowanie ciągłości, która jest zwykle wspomniane informatyki podręcznikach ukrywa wszelkie topologicznych intuicje. (W rzeczywistości Dana Scott często pisała, że ​​celowo unikał sformułowań topologicznych, ponieważ informatyków nie jest z tym zaznajomiona.)

Związek między sformułowaniami algebraicznymi i topologicznymi nazywa się dualnością kamienną , a teraz staje się coraz bardziej jasne, że samo to połączenie jest niezwykle ważne dla informatyki.

Aby zapoznać się z koncepcyjnym przedstawieniem tych połączeń (i wiele innych), zobacz Informacje, procesy i gry Abramsky'ego .