Funções Scott-contínuas: uma definição alternativa

Estou realmente lutando com esta propriedade:

Deixe que $X,Y$ ser espaços coerentes e ser uma função monótona. é contínuo se e somente se , para todos os modo que seja um conjunto direcionado.f f ( ⋃ x ∈ D x ) = ⋃ x ∈ D f ( x $f: Cl(X) \rightarrow Cl(Y)$$f$$f(\bigcup_{x\in D} x)=\bigcup_{x \in D}f(x)$$D \subseteq Cl(X)$$D$

Dirigido conjunto é definido assim: poset é um conjunto dirigido sse tal e . significa cliques de X: coerente .$D \subseteq$∃ z ∈ D x ⊆ z x ' ⊆ z C l ( X ) { x ⊆ | X | ∣ a , b ∈ x ⇒ a b $\forall x, x' \in D$ $\exists z \in D$$x \subseteq z$$x' \subseteq z$
$Cl(X)$$\{x \subseteq |X| \mid a,b \in x \Rightarrow a$$b \}$

Muitos livros dão isso como uma definição de funções contínuas de Scott , mas infelizmente não são meu professor. Ele nos deu essa definição de contínuo:

$f : Cl(X) \rightarrow Cl(Y)$ é contínuo se for monótono e , em que monótono é definido como: é monótono se$\forall x \in Cl(X), \forall b \in f(x), \exists x_0 \subseteq_{fin} x, b \in f(x_0)$
$f$$a \subseteq b \Rightarrow f(a) \subseteq f(b)$

Esta é a prova proposta que tenho, mas não consigo entender a última equação.

A prova de contínua implicaf ( ⋃ D ) = ⋃ f ( D $f$$f(\bigcup D)=\bigcup f(D)$ :
Seja $b \in f(\bigcup D)$ . Pela definição de continuidade, $\exists x_0 \subset_{fin} x \mid b \in f(x_0)$ . Observe que $x_0$ é a união de $\{ x_i \mid x_i \in D\}$ .
Se $D$ for direto, então: $\exists z \in D \mid x_i \subseteq z$ seguida, $x_0 \subseteq z$ . Pela definição de monotonia, $f(x_0)\subseteq f(z)$ então $b \in f(z)$ (???) $\subseteq \bigcup f(D)$ . E mesmo isso é verdade, devemos mostrar que $\bigcup f(D) = f(\bigcup D)$ , não apenas$\subseteq$ .

A prova da outra implicação é ainda pior, então não posso escrevê-la aqui ... Você pode me explicar como a prova pode funcionar?

A definição de continuidade usada pelo seu professor é a melhor. Ele diz muito concretamente o que significa continuidade.

Suponha que . Isso significa que, dada toda a informação de x , possivelmente um conjunto infinito de tokens (átomos), a função produz algum elemento que possui a informação atômica b . (Pode haver outras informações também, mas não estamos preocupadas com isso no momento.) A definição de seu professor diz que não é necessário examinar todas as informações infinitas de x para produzir as informações de saída b . Algum subconjunto finito de x é suficiente para produzi-lo.$b \in f(x)$$x$$b$$x$$b$$x$

(O livro de Melvin Fitting "Teoria da computabilidade, semântica e programação lógica", Oxford, 1987, chama essa propriedade de compacidade e define uma função contínua como monótona e compacta.)

Essa é a essência da continuidade. Para obter uma quantidade finita de informações sobre a saída de uma função, você só precisa de uma quantidade finita de informações sobre a entrada. A saída produzida pela função para uma entrada infinita é obtida reunindo as informações que produz para todas as aproximações finitas da entrada infinita. Em outras palavras, você não recebe nenhum salto mágico ao passar das aproximações finitas para a união infinita. Tudo o que você obtém no infinito, já deve estar em algum estágio finito.

A equação padrão é bonita de se olhar, mas não diz a você toda a intuição que expliquei acima. No entanto, matematicamente, é equivalente à definição do seu professor.$f(\bigcup_{x \in D} x) = \bigcup_{x \in D} f(x)$

Para mostrar que , que é suficiente para mostrar que f ( x ) está incluído na f ( ⋃ x ∈ D x ) , para cada x ∈ D . Mas isso se segue diretamente da monotonicidade de f, porque x ⊆ ⋃ x ∈ D x . Então, essa é a direção "fácil".$\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$

A outra direção, comprovada pelo seu professor, é a interessante: . Para ver isso, use a intuição que mencionei acima. Qualquer informação atômica b no lado esquerdo vem de alguma aproximação finita da entrada: x 0 ⊆ f i n ⋃ x ∈ D x . Ou seja, b ∈ f ( x 0 ) . Desde 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$é finito e está incluído na união do conjunto direcionado, deve haver algo no conjunto direcionado que seja maior que , talvez x 0 em si. Chame esse elemento z . Por monotonicidade, f ( x 0 ) ⊆ f ( z ) . Então, b ∈ f ( z ) . Desde z ∈ D , F ( z ) ⊆ ⋃ x ∈ D f ( x ) . Então agora $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$é visto também no lado direito. QED.

Como você observou, mostrar que a continuidade do professor implica que a bonita equação é fácil. O mais difícil é mostrar que a equação bonita, apesar de parecer que não está dizendo muito, realmente diz tudo na definição do professor.

Ocorreu-me tardiamente, depois que escrevi a última resposta, que a definição de continuidade do professor que eu estava explicando em minha resposta é a noção topológica de continuidade. A formulação algébrica de continuidade que geralmente é mencionada nos livros de ciência da computação esconde todas as intuições topológicas. (De fato, Dana Scott costuma escrever que evita deliberadamente formulações topológicas porque os cientistas da computação não estão familiarizados com isso.)

A ligação entre as formulações algébricas e topológicas é chamada dualidade de Stone , e agora está se tornando cada vez mais claro que essa ligação em si é extremamente importante para a Ciência da Computação.

Para uma exposição conceitual dessas conexões (e muito mais), consulte as informações, processos e jogos de Abramsky .