7
$\begingroup$

I am working on writing an easy to read document about denotational semantics of the lambda calculus. For that I introduce CPOs, monotonicity and continuity. A CPO is a set $M$ with a partial order $\leq$ and a bottom element $\bot$, requiring $\bot$ to be the smallest element in $M$ and the existence of the least upper bound ($\bigsqcup$) for every chain $d_0 \leq d_1 \leq d_2 \leq ...$ in $M$. A function $f$ between two CPOs $M$, $N$ is monotone, if for all $a, b \in M$ the following holds:

$$a \leq b \implies f(a) \leq f(b)$$

A function $f$ between two CPOs $M$, $N$ is continuous, if it is monotone and for all chains $d_0 \leq d_1 \leq d_2 \leq \dots$ we have

$$f(\bigsqcup_{i \in \mathbb{N}} d_i) = \bigsqcup_{i \in \mathbb{N}} f(d_i).$$

I want to give my readers a good intuition about the meaning of these definitions. However, I don't have one I could write down. Following Glynn Winskel in his book »The Formal Semantics of Programming Languages« (1993), $a \leq b$ has to be read as $a$ approximates $b$ (page 72), meaning $b$ has at least as much information as $a$. This leads to monotone functions reflecting more information about the input in more information about the output (page 122). This is somewhat understandable for me. However, the explanation of continuity is not clear for me:

As we shall see, that computable functions should be continuous follows from the idea that the appearance of a unit of information in the output of a computable function should only depend on the presence of finitely many units of information in the input.

(page 73)

This is still unclear to me after reading the stream example in section 8.2 (pages 121–123), or this answer.

So my final question is: How do I convince my readers that computable functions are continuous? Why is there no computable function which is not continuous?

It would be nice if you can give me answers/examples which do not require the rigorous introduction of computability or fix-point theory, since I do not want to focus on those things. Also it would be great if it is not necessary to know the lambda calculus and its denotational semantics in advance, because I want to (and have to) introduce monotonicity and continuity before them.

EDIT: By computable I mean Turing-computable. Please correct me if I misunderstand Winskels definition of computable on page 337, since it is not explicitly defined as Turing-computable but in an equivalent (at least in my eyes) manner.

Also I want to point out another source I found which tries to explain my problem. But still I don't understand its example, since it is basically the same as the stream example from Winskel.

EDIT 2: It would also be a good start in helping me to understand the matter to show that every computable function is monotone, i.e. there exists no non-monotone computable function.

$\endgroup$
6
$\begingroup$

There are several ways to explain "computable implies continuous", I shall give here two such explanations.

Turing machines compute continuous maps

Suppose we have a Turing machine which takes possibly infinite amount of input written down on an input tape. It writes the result on an output tape, where the output cells are write-once. There are workign tapes. The machine may run forever, filling up the outputs cells. This is known as a type two machine. (The argument for other kinds of machines is going to be similar but simpler.)

The following should be obvious: when the machine writes into an output cell, its workings up to that point only depends on a finite portion of the input tape, for the simple reason that in finitely many computation steps it could not have moved the input head past some point. Therefore, every input tape that agrees with the given one up to that point would have caused the machine to write the same answer to the same output cell.

But this is a form of continuity, if we put the correct topology on the spaces of input and output tapes.

First we put topology on the set $\Sigma$ of symbols that can be written onto tape cells. For this we just pick the discrete topology. A tape is an infinite sequence of symbols, so an element of $\Sigma^\omega$, which is a product of $\Sigma$'s. Let's put the product topology on it.

Recall that a basic open set on $\Sigma^\omega$ for the product topology is of the form $U(a_0, \ldots, a_{n-1}) = \{\alpha \in \Sigma^\omega \mid \forall i < n . \, \alpha_i = a_i\}$, where $a_0, \ldots, a_i \in \Sigma$. That is, a basic open set fixes an initial portion of the sequence to the given values $a_0, \ldots, a_n$.

Now we may check that the function $f : \Sigma^\omega \to \Sigma^\omega$ computed by the machine is indeed continuous. Take a basic open set $V = U(a_0, \ldots, a_{n-1})$ and let $W = f^{-1}(V)$. We need to verify that $W$ is open. For this purpose, consider any $\alpha \in W$. If we find a basic open set $W'$ such that $\alpha \in W' \subseteq W$, then we're done.

Because $\alpha \in W$, we have $f(\alpha) \in U$. Thus on input $\alpha$ the machine produces an output tape starting with $a_0, a_1, \ldots, a_{n-1}$. By the time it writes out these cells it has inspected at most the first $k$ cells of the input, for some $k \in \mathbb{N}$. We may take $W' := U(\alpha_0, \ldots, \alpha_k)$ and verify that $\alpha \in W' \subseteq W$. It is obvious that $\alpha \in W'$. To prove $W' \subseteq W$ take any $\beta \in W'$ and observe that $f(\alpha)$ and $f(\beta)$ agree on the first $n$ values of the output. This implies that $f(\beta) \in V$ and hence $\beta \in W$, as required.

Computable maps are continuous as maps between algebraic $\omega$CPOs

First, let me note that what you defined is usually called "$\omega$CPO" ($\omega$ in the name indicates we only require suprema of chains).

In denotational semantics datatypes correspond to $\omega$CPOs. In fact, they correspond to algebraic $\omega$CPOs (is this in your thesis?), which are $\omega$CPOs for which the compact elements form a base. Here are some definitions.

Definition: Let $D$ be an $\omega$CPO. An element $d \in D$ is compact if, for every chain $x_0 \leq x_1 \leq \cdots$ such that $d \leq \bigsqcup_i x_i$, there exists $j$ such that $d \leq x_j$.

Definition: An $\omega$CPO is algebraic if every $x \in D$ is the supremum of compact elements below it.

The intuition behind compact elements is that they contain "finite information". A good example is $\mathcal{P}(\mathbb{N})$, the powerset of natural numbers ordered by $\subseteq$, where the compact elements are precisely the finite subsets of $\mathbb{N}$ (exercise!). Another example: in the $\omega$CPO of continuous functions $\mathbb{N} \to \mathbb{N}_\bot$ the compact elements are those partial functions that are equal to $\bot$ everywhere, except at finitely many arguments.

To say that an $\omega$CPO is algbraic is to say that every element is completely determined by the finite pieces of information that approximate it. It is a fact that in denotational semantics datatypes correspond to algebraic $\omega$CPOs, unless we are doing something very unusual.

We can now explain why every computable map is continuous. Suppose $D$ and $E$ are $\omega$CPOS and $f : D \to E$ computable. Suppose $x \in D$, $e \in E$, $e$ is compact, and $e \leq f(x)$. Intuitively, this say that "finite piece of information $e$ appears in the output $f(x)$". Because $f$ is computable, it must be the case that it computed the information $e$ by accessing only a finite amount of information about $x$, i.e., there is a compact $d \in D$ such that $d \leq x$ and $e \leq f(d)$. This argument should be compared to the Turing machine argument above. We have established:

Lemma: If $f : D \to E$ is computable and $e \leq f(x)$ for some $x \in D$ and a compact $e \in E$, then there is compact $d \in D$ such that $d \leq x$ and $e \leq f(d)$.

We can usethe lemma to show that a computable $f$ is continuous. Suppose $x_0 \leq x_1 \leq \cdots$ is a chain in $D$. Because $f$ is monotone, we already know that $\bigsqcup_i f(x_i) \leq f(\bigsqcup_i x_i)$, but we also need the inequality $f(\bigsqcup_i x_i) \leq \bigsqcup_i f(x_i)$. Because $E$ is algebraic, it suffices to show that, whenever $e \in E$ is compact and $e \leq f(\bigsqcup_i x_i)$ then $e \leq \bigsqcup_i f(x_i)$. So assume $e \leq f(\bigsqcup_i x_i)$. By the lemma there exists a compact $d \in D$ such that $d \leq \bigsqcup_i x_i$ and $e \leq f(d)$. Because $d$ is compact, there exists $j$ such that $d \leq x_j$, hence by monotonicity of $f$ we have $e \leq f(d) \leq f(x_j) \leq \bigsqcup_i f(x_i)$. We are done.

$\endgroup$
  • $\begingroup$ What definition of continuity are you using and how is it similar to the one I specified? I am not familiar with the terms basic open set and topology. Can I assume that a topology in this case is analogous to an order? $\endgroup$ – user3389669 Sep 8 '17 at 11:48
  • 1
    $\begingroup$ These are basic concepts in topology, look them up in any textbook on topology. I don't quite understand. You're writing an explanation about computability and continuity, but you are not familiar with the standard definition of continuity? (The one you're using is a special case.) It would help if you explained a bit your background and your motivation, then perhaps I can give you advice that is better than "learn to walk before you run". $\endgroup$ – Andrej Bauer Sep 8 '17 at 15:31
  • $\begingroup$ To be honest: I'm a computer science student and I'm working on my master's thesis. My task is basically to construct a denotational semantics for the lambda calculus (the way Dana Scott did in early 70s). My primary source is the book »Semantik von Programmiersprachen« by Rudolf Berghammer (german). From there I have the definitions. Unfortunately in that book continuity is motivated using the theory of fixed points. My thesis should present only what is really needed to construct the domain suited for a denot. sem. of the lambda calculus, so I skip that part. $\endgroup$ – user3389669 Sep 8 '17 at 17:41
  • $\begingroup$ [continuation] My work on the construction and the proofs is done (it is also an important aspect of my work to extend the existent proofs such that no gaps be open). To give my thesis the finishing touch, I want to motivate every definition intuitively, such that it can be easily read by other young computer scientists. However, as you can see, I lack intuition myself. $\endgroup$ – user3389669 Sep 8 '17 at 17:45
  • 3
    $\begingroup$ Thank you for the explanation. That makes a lot of sense. First, I don't think Dana Scott used CPOs. He used continuous lattices, and I highly recommend his Data types as lattices. That will give you some historical perspective – beware of making up fake history! I will supplement my answer to motivate the continuity in CPOs. $\endgroup$ – Andrej Bauer Sep 8 '17 at 18:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.