<blockquote>
<p>My question is this: If f is a Scott-continuous computable function, and is &quot;total&quot; (i.e. the elements of its domain are all finite, and it takes &quot;fully-defined&quot; values to &quot;fully-defined&quot; values), have techniques been developed for computing a maximal h such that f⊑h?</p>
<p>Of course, if the domain of f is a finite set, one can just represent f as a lookup table and then use elementary deduction to compute h. It's not necessarily efficient in practice, but it yields the correct answer. But what about functions over infinite domains?</p>
</blockquote>
<p>Scott-continuity rules out the lookup table approach. For a concrete counterexample, let's start with the Sierpinksi domain <span class="math-container">$O = \{\bot, \top\}$</span>, with order <span class="math-container">$\bot \sqsubseteq \top$</span>.
Intuitively, think of <span class="math-container">$\bot$</span> as nontermination, and <span class="math-container">$\top$</span> as termination. In Haskell terms, think of this as the domain interpreting expressions of type <span class="math-container">$()$</span> -- i.e., you either get back a unit or the expression fails to terminate. We'll also use <span class="math-container">$2$</span>, the booleans, and <span class="math-container">$2_\bot$</span>, the pointed booleans.</p>
<p>Now, suppose you have <span class="math-container">$f : O \to 2_\bot$</span>. You can't continuously complete this function, even though there are only a finite number of possible <span class="math-container">$f$</span>'s! The intuitive reason is that when you run <span class="math-container">$f(\bot)$</span>, there's no finite waiting period sufficiently long enough to decide that its return value is bottom -- if there were, then I could give you a function that spins for one second longer, and then returns the opposite of whatever you completed the function to. (Prove that any continuous <span class="math-container">$h : (O \to 2_\bot) \to (O \to 2)$</span> must return a constant function independent of its argument <span class="math-container">$f$</span>.)</p>
<p>Don't think of bottom as an extra element of the domain of values. This will lead you astray. Instead, think of elements of the domain as observations of a computation. Really do think of sitting in front of a terminal, waiting for your program to print something. Bottom represents your observation when the program is still running and hasn't printed anything to the screen -- it represents observing nothing.</p>
<p>The best book I know for developing the right intuitions is <a href="https://rads.stackoverflow.com/amzn/click/com/0521576512" rel="noreferrer" rel="nofollow noreferrer">Steve Vickers' <em>Topology via Logic</em></a>. It's a short and easy read, but your domain-fu will go way up for reading it.</p>

CC BY-SA 3.0
2011-04-11T12:54:22.773Z
What does "continuously complete" mean?
Robin Green
CC BY-SA 3.0
2011-04-11T13:03:23.280Z
I mean there is no continuous function $h$ which is a completion in the sense you defined.
Neel Krishnaswami
CC BY-SA 3.0
2011-04-11T14:50:00.847Z
Ah, OK. Sorry, when I said "represent f as a lookup table", I was thinking of applying f to only "fully-defined" values (which isn't a faithful representation!). I should have been explicit about that. Certainly, there will be cases where f is the only h such that f⊑h. So I believe your objection is based on a misunderstanding. And I think it can be fruitful to consider bottom an extra element of the domain of values. I don't understand why your answer shows that having access to definedness and Scott-continuity are incompatible. The programmer (or the code generator) just has to be careful.
Robin Green
CC BY-SA 3.0
2011-04-11T16:11:06.473Z
What's a pointed boolean ?
Suresh Venkat
CC BY-SA 3.0
2011-04-11T18:12:41.500Z
@Suresh, pointed Boolean is the three member poset $\{true, false, \bot\}$, where $\bot$ is below the other two. You can think of it as not-known/undefined/no-information about the value. This can be done with any set, i.e. add an element below all elements and leave the rest as incomparable (this is sometimes called the flat domain).
Kaveh
CC BY-SA 3.0
2011-04-11T18:16:34.100Z
@Robin, Neel is right. It seems that you are confusing the particular case that you have in mind with domain theoretic notions. It might be better if you state your question without using domain theory.
Kaveh
CC BY-SA 3.0
2011-04-11T11:31:04.937Z
2011-04-11T11:31:04.937Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>It's been several years since this was asked, but then again, there's only that many mentions of domain theory in the forum, so let me try to set some things straight for the sake of my own understanding at least. To skip my disclaimer blah-blah, just scroll down to the bold-face letters.</p>

<p>Possibly confused by Kaveh's justified clarification questions, you write "fully-defined means maximal, yes", but in the original post you had already written "[...] $f$ is [...] "total" (i.e. the elements of its domain are all finite, and it takes "fully-defined" values to "fully-defined" values) [...]", which suggested to me that you treat "total" and "fully defined" as synonyms---as indeed I do: you can't get more partial than the undefined $\bot$, and no more defined than some total element. But: I don't agree with the condition that the inputs of $f$ be "finite" (either domain-theoretically or in their number).</p>

<p>In fact, by (the usual) definition, a continuous function $f : A \to B$, for arbitrary data types $A$, $B$, is <em>total</em> whenever for all $x \in A$, if $x$ is total then also $f(x)$ is total. This presupposes of course that we agree on a notion of totality for <em>base types</em>, and the obvious choice is to ban everything that involves $\bot$ (assuming that we are working with <em>flat</em> domains, there's just one such element, but there are possibly more in the non-flat case).</p>

<p>Maximality and totality in domain theory are two quite different things. At <em>flat</em> base types they coincide, but at higher types they generally don't. There are examples in <a href="https://zbmath.org/?q=an:0828.06001" rel="nofollow noreferrer">[Stoltenberg-Hansen et al 1994, section 8.3]</a>, but since you already mention Haskell and laziness, let me just recall that in the <em>non-flat</em> domain $\mathbb{N}_\ast$ of lazy natural numbers you have the maximal but not total element $\{\bot, S\bot, SS\bot,\ldots \}$. Just to be complete, an example of a total but not maximal element at type, e.g., $\mathbb{B}_\bot \to \mathbb{B}_\bot$ would be the function determined by $\bot \mapsto \bot$ and $x \mapsto \mathtt{tt}$ for $x \neq \bot$, which is total but strictly below the function having $x \mapsto tt$ for all $x$.</p>

<p>Concerning <a href="https://cstheory.stackexchange.com/a/5993/10146">Neel's answer</a>, though I appreciate its pragmatic intuition and I'm going to take his "this will lead you astray" warning seriously, I still feel that I should stress the obvious good theoretical reasons to want to talk about undefinedness as a bona-fide value: it's the way to thematize computational partiality while conveniently using mathematically total mappings, and so end up with an accurate and rich enough theory. Besides, on the pragmatic level, we do have functions that are either provably or <em>by definition</em> undefined (no pun) at certain inputs; think here of how one uses <code>Maybe</code> in Haskell, or the very idea of exception handling in general for that matter, as devices that treat undefinedness as a value.</p>

<p>So I may be lacking basic intuition that Neel has, and therefore be missing his point altogether, but to me a function $f$ as an element of a domain is the <em>known</em> or <em>expected</em> program behavior <em>in its ideal entirety</em> (things are a bit different if we work with more tangible representations of domains, like information systems, where we may assume to only know <em>parts</em> of the behavior of programs); in particular, I do not talk about some <em>implementation</em> of $f$ that might run faster or slower than others so that I might never be sure of its termination. On this basis, my answer below differs from Neel's quite radically (and I'd appreciate feedback or corrections on this, from Neel or anyone).</p>

<p>So, finally, <strong>to answer the question</strong>. We assume that $f$ is total and that $g$ is above $f$. I understand that you ask what the maximal $g^{\max}$ above $f$ is.</p>

<p>First a quick remark: we can prove that $g$ is also total (which is sometimes called "extension lemma"), so it would arguably make more sense, from the point of view of effectivity, to ask about "minimal" totality instead of "maximal" totality: if $h$ is some element (possibly partial), what is a minimal way to extend it to an $f$ which will be total? (that we can extend it to a total at all is the content of the fundamental <em>density theorem</em>, see <a href="https://zbmath.org/?q=an:1148.68405" rel="nofollow noreferrer">[Normann 2008]</a>). And then: if $f$ is already total, what is a minimal <em>equivalent</em> total $g$ (that is, a total $g$ which agrees with $f$ on its total inputs)? Of relevance here is the characterization by <a href="https://zbmath.org/?q=an:0599.03051" rel="nofollow noreferrer">[Longo &amp; Moggi 1984]</a> of two totals being equivalent exactly when they have a total intersection.</p>

<p>But back to the "maximal" totality. One more thing we can prove is that two totals are equivalent if and only if they are bounded. From this follows that, given a total $f$, a first answer to your question is
$$g^{\max} = \bigsqcup \{g \mid g \mbox{ is total and equivalent to }f\} .$$
This thing <em>does</em> exist, since domains are bounded-complete.</p>

<p>But I say "a first answer", because I can't think clearly now of an actual <em>technique</em>, as you specifically ask, of providing this supremum. In other words, I'm not sure of how constructive all the relevant steps are in this thread of thought. Perhaps someone can comment on this aspect (or I might, if I find the time to think about it with a clear head).</p>

CC BY-SA 3.0
2015-02-13T11:01:59.493Z
2015-02-13T11:01:59.493Z
2017-04-13T12:32:28.743Z
Basil
<p>In slightly more down-to-earth terms, this question is sort of about lazy evaluation in functional programming - except that it's more ambitious in general than just seeking what a typical Haskell programmer would consider "least-strict". If the previous sentence made no sense to you, don't worry, ignore it.</p>

<p>In domain theory, we examine posets, and for the purposes of this question we will consider a poset to represent the set of possible partially-specified values of a type in a non-strict programming language, such that two partial values $x$ and $y$ are ordered as $x \sqsubseteq y$ iff $y$ is $x$ "plus zero or more extra bits of information". In other words, $x \sqsubseteq y$ iff y is a version of $x$ where zero or more of the "holes" or "thunks" (if any) have been filled in.</p>

<p>We can (and do) extend this partial order to Scott-continuous functions, by stipulating that $f \sqsubseteq g$ iff for all $x$, $f(x) \sqsubseteq g(x)$.</p>

<p>However, note that in the case of Scott-continuous functions, $f$ can be $\sqsubseteq$ $g$ even if $g$ is distinguishable from $f$ <em>but does not provide any extra information</em>. This can be the case if $g$ provides the same information "more parsimoniously" (or "more lazily", depending on how you want to look at it).</p>

<p>My question is this: If $f$ is a Scott-continuous computable function, and is "total" (i.e. the elements of its domain are all finite, and it takes "fully-defined" values to "fully-defined" values), have techniques been developed for computing a maximal $h$ such that $f \sqsubseteq h$?</p>

<p>Of course, if the domain of $f$ is a finite set, one can just represent $f$ as a lookup table and then use elementary deduction to compute $h$. It's not necessarily efficient in practice, but it yields the correct answer. But what about functions over infinite domains?</p>

CC BY-SA 3.0
2011-04-10T05:57:12.260Z
Do you possibly mean 'minimal h' such that $f \le h$ ?
Suresh Venkat
CC BY-SA 3.0
2011-04-10T06:21:42.333Z
No, the minimal such h would be f.
Robin Green
CC BY-SA 3.0
2011-04-10T08:00:25.333Z
Can't we do the trivial algorithm? Assuming $f \in [D \to E]$, for a given value $x\in D$, find a maximal $y\in E$ above $f(x)$ and define $h(x)=y$. If we have a way to find a maximal  element in $E$ above a given one then we can do this. I also think this is optimal w.r.t. the problem of finding a maximal element in the $E$ above a given element. (I am assuming that there is at least a maximal element above any given element in $E$, o.w. there is no maximal $h$.)
Kaveh
CC BY-SA 3.0
2011-04-10T08:26:17.157Z
Such a h is unlikely to be Scott-continuous. I forgot to mention that it should be.
Robin Green
CC BY-SA 3.0
2011-04-11T07:06:39.693Z
clarification questions: 1. how do we representation $f$? the part about $f$ being total is not clear, 2. by "fully-defined" do you mean the maximal elements of the domains? 3. are you using "finite" in its domain theoretic sense (i.e. way-below itself)?
Kaveh
CC BY-SA 3.0
2011-04-11T07:40:49.253Z
f is represented as a pure function which, unlike a Haskell function, has full access to the definedness of each component of its argument. For example, if its argument is a domain representing a pair of booleans, f can determine whether the first component of the pair is defined and true, defined and false, or undefined (aka a "hole" or "thunk"). This is more powerful but also more dangerous (discontinuous functions possible). Fully-defined means maximal, yes. I'm using finite in the ordinary mathematical sense. I don't know much about domain theory - I've only just started reading about it.
Robin Green
CC BY-SA 3.0
2011-04-11T11:02:58.720Z
Robin, "having access to definedness" and "Scott-continuous" are incompatible properties. There's not enough room in the comment box, so I'll add an answer explaining why this is so.
Neel Krishnaswami
CC BY-SA 3.0
2011-04-11T18:19:52.617Z
Either we are talking about a general domain theoretic question, in which case I don't understand what you mean by represented by a pure function, or you have a particular domain in mind in which case you should state the question not as a general domain theory question but by defining the particular domain you are talking about and ask the question for that domain. (continuity is w.r.t. the topology, and AFAIR any computable function is continuous w.r.t. the topology induced by information refinement order relation). Vicker's book that Neel suggested is quite nice and readable. (more)
Kaveh
<pl.programming-languages><functional-programming><domain-theory>
Prior work on finding domain-theoretic suprema of equivalent total functions?
Robin Green
# Prior work on finding domain-theoretic suprema of equivalent total functions?

(Asked by: username_0 on 2011-04-09)

In slightly more down-to-earth terms, this question is sort of about lazy evaluation in functional programming - except that it's more ambitious in general than just seeking what a typical Haskell programmer would consider "least-strict". If the previous sentence made no sense to you, don't worry, ignore it.

In domain theory, we examine posets, and for the purposes of this question we will consider a poset to represent the set of possible partially-specified values of a type in a non-strict programming language, such that two partial values $x$ and $y$ are ordered as $x \sqsubseteq y$ iff $y$ is $x$ "plus zero or more extra bits of information". In other words, $x \sqsubseteq y$ iff y is a version of $x$ where zero or more of the "holes" or "thunks" (if any) have been filled in.

We can (and do) extend this partial order to Scott-continuous functions, by stipulating that $f \sqsubseteq g$ iff for all $x$, $f(x) \sqsubseteq g(x)$.

However, note that in the case of Scott-continuous functions, $f$ can be $\sqsubseteq$ $g$ even if $g$ is distinguishable from $f$ *but does not provide any extra information*. This can be the case if $g$ provides the same information "more parsimoniously" (or "more lazily", depending on how you want to look at it).

My question is this: If $f$ is a Scott-continuous computable function, and is "total" (i.e. the elements of its domain are all finite, and it takes "fully-defined" values to "fully-defined" values), have techniques been developed for computing a maximal $h$ such that $f \sqsubseteq h$?

Of course, if the domain of $f$ is a finite set, one can just represent $f$ as a lookup table and then use elementary deduction to compute $h$. It's not necessarily efficient in practice, but it yields the correct answer. But what about functions over infinite domains?

**Tags:** pl.programming-languages, functional-programming, domain-theory
> **Comments:**
> **username_1**: Do you possibly mean 'minimal h' such that $f \le h$ ?  
> **username_0**: No, the minimal such h would be f.  
> **username_2**: Can't we do the trivial algorithm? Assuming $f \in [D \to E]$, for a given value $x\in D$, find a maximal $y\in E$ above $f(x)$ and define $h(x)=y$. If we have a way to find a maximal  element in $E$ above a given one then we can do this. I also think this is optimal w.r.t. the problem of finding a maximal element in the $E$ above a given element. (I am assuming that there is at least a maximal element above any given element in $E$, o.w. there is no maximal $h$.)  
> **username_0**: Such a h is unlikely to be Scott-continuous. I forgot to mention that it should be.  
> **username_2**: clarification questions: 1. how do we representation $f$? the part about $f$ being total is not clear, 2. by "fully-defined" do you mean the maximal elements of the domains? 3. are you using "finite" in its domain theoretic sense (i.e. way-below itself)?  
> **username_0**: f is represented as a pure function which, unlike a Haskell function, has full access to the definedness of each component of its argument. For example, if its argument is a domain representing a pair of booleans, f can determine whether the first component of the pair is defined and true, defined and false, or undefined (aka a "hole" or "thunk"). This is more powerful but also more dangerous (discontinuous functions possible). Fully-defined means maximal, yes. I'm using finite in the ordinary mathematical sense. I don't know much about domain theory - I've only just started reading about it.  
> **username_3**: Robin, "having access to definedness" and "Scott-continuous" are incompatible properties. There's not enough room in the comment box, so I'll add an answer explaining why this is so.  
> **username_2**: Either we are talking about a general domain theoretic question, in which case I don't understand what you mean by represented by a pure function, or you have a particular domain in mind in which case you should state the question not as a general domain theory question but by defining the particular domain you are talking about and ask the question for that domain. (continuity is w.r.t. the topology, and AFAIR any computable function is continuous w.r.t. the topology induced by information refinement order relation). Vicker's book that Neel suggested is quite nice and readable. (more)  

---

## 2 answers

### Answer by username_3 on 2011-04-11. Score: 5

> My question is this: If f is a Scott-continuous computable function, and is "total" (i.e. the elements of its domain are all finite, and it takes "fully-defined" values to "fully-defined" values), have techniques been developed for computing a maximal h such that f⊑h?
>
> Of course, if the domain of f is a finite set, one can just represent f as a lookup table and then use elementary deduction to compute h. It's not necessarily efficient in practice, but it yields the correct answer. But what about functions over infinite domains?

Scott-continuity rules out the lookup table approach. For a concrete counterexample, let's start with the Sierpinksi domain $O = \{\bot, \top\}$, with order $\bot \sqsubseteq \top$.
Intuitively, think of $\bot$ as nontermination, and $\top$ as termination. In Haskell terms, think of this as the domain interpreting expressions of type $()$ -- i.e., you either get back a unit or the expression fails to terminate. We'll also use $2$, the booleans, and $2\_\bot$, the pointed booleans.

Now, suppose you have $f : O \to 2\_\bot$. You can't continuously complete this function, even though there are only a finite number of possible $f$'s! The intuitive reason is that when you run $f(\bot)$, there's no finite waiting period sufficiently long enough to decide that its return value is bottom -- if there were, then I could give you a function that spins for one second longer, and then returns the opposite of whatever you completed the function to. (Prove that any continuous $h : (O \to 2\_\bot) \to (O \to 2)$ must return a constant function independent of its argument $f$.)

Don't think of bottom as an extra element of the domain of values. This will lead you astray. Instead, think of elements of the domain as observations of a computation. Really do think of sitting in front of a terminal, waiting for your program to print something. Bottom represents your observation when the program is still running and hasn't printed anything to the screen -- it represents observing nothing.

The best book I know for developing the right intuitions is [Steve Vickers' *Topology via Logic*](https://rads.stackoverflow.com/amzn/click/com/0521576512). It's a short and easy read, but your domain-fu will go way up for reading it.

> **Comments:**
> **username_0**: What does "continuously complete" mean?  
> **username_3**: I mean there is no continuous function $h$ which is a completion in the sense you defined.  
> **username_0**: Ah, OK. Sorry, when I said "represent f as a lookup table", I was thinking of applying f to only "fully-defined" values (which isn't a faithful representation!). I should have been explicit about that. Certainly, there will be cases where f is the only h such that f⊑h. So I believe your objection is based on a misunderstanding. And I think it can be fruitful to consider bottom an extra element of the domain of values. I don't understand why your answer shows that having access to definedness and Scott-continuity are incompatible. The programmer (or the code generator) just has to be careful.  
> **username_1**: What's a pointed boolean ?  
> **username_2**: @Suresh, pointed Boolean is the three member poset $\{true, false, \bot\}$, where $\bot$ is below the other two. You can think of it as not-known/undefined/no-information about the value. This can be done with any set, i.e. add an element below all elements and leave the rest as incomparable (this is sometimes called the flat domain).  
> **username_2**: @Robin, Neel is right. It seems that you are confusing the particular case that you have in mind with domain theoretic notions. It might be better if you state your question without using domain theory.  

---

### Answer by username_4 on 2015-02-13. Score: 0

It's been several years since this was asked, but then again, there's only that many mentions of domain theory in the forum, so let me try to set some things straight for the sake of my own understanding at least. To skip my disclaimer blah-blah, just scroll down to the bold-face letters.

Possibly confused by Kaveh's justified clarification questions, you write "fully-defined means maximal, yes", but in the original post you had already written "[...] $f$ is [...] "total" (i.e. the elements of its domain are all finite, and it takes "fully-defined" values to "fully-defined" values) [...]", which suggested to me that you treat "total" and "fully defined" as synonyms---as indeed I do: you can't get more partial than the undefined $\bot$, and no more defined than some total element. But: I don't agree with the condition that the inputs of $f$ be "finite" (either domain-theoretically or in their number).

In fact, by (the usual) definition, a continuous function $f : A \to B$, for arbitrary data types $A$, $B$, is *total* whenever for all $x \in A$, if $x$ is total then also $f(x)$ is total. This presupposes of course that we agree on a notion of totality for *base types*, and the obvious choice is to ban everything that involves $\bot$ (assuming that we are working with *flat* domains, there's just one such element, but there are possibly more in the non-flat case).

Maximality and totality in domain theory are two quite different things. At *flat* base types they coincide, but at higher types they generally don't. There are examples in [[Stoltenberg-Hansen et al 1994, section 8.3]](https://zbmath.org/?q=an:0828.06001), but since you already mention Haskell and laziness, let me just recall that in the *non-flat* domain $\mathbb{N}\_\ast$ of lazy natural numbers you have the maximal but not total element $\{\bot, S\bot, SS\bot,\ldots \}$. Just to be complete, an example of a total but not maximal element at type, e.g., $\mathbb{B}\_\bot \to \mathbb{B}\_\bot$ would be the function determined by $\bot \mapsto \bot$ and $x \mapsto \mathtt{tt}$ for $x \neq \bot$, which is total but strictly below the function having $x \mapsto tt$ for all $x$.

Concerning [Neel's answer](https://cstheory.stackexchange.com/a/5993/10146), though I appreciate its pragmatic intuition and I'm going to take his "this will lead you astray" warning seriously, I still feel that I should stress the obvious good theoretical reasons to want to talk about undefinedness as a bona-fide value: it's the way to thematize computational partiality while conveniently using mathematically total mappings, and so end up with an accurate and rich enough theory. Besides, on the pragmatic level, we do have functions that are either provably or *by definition* undefined (no pun) at certain inputs; think here of how one uses `Maybe` in Haskell, or the very idea of exception handling in general for that matter, as devices that treat undefinedness as a value.

So I may be lacking basic intuition that Neel has, and therefore be missing his point altogether, but to me a function $f$ as an element of a domain is the *known* or *expected* program behavior *in its ideal entirety* (things are a bit different if we work with more tangible representations of domains, like information systems, where we may assume to only know *parts* of the behavior of programs); in particular, I do not talk about some *implementation* of $f$ that might run faster or slower than others so that I might never be sure of its termination. On this basis, my answer below differs from Neel's quite radically (and I'd appreciate feedback or corrections on this, from Neel or anyone).

So, finally, **to answer the question**. We assume that $f$ is total and that $g$ is above $f$. I understand that you ask what the maximal $g^{\max}$ above $f$ is.

First a quick remark: we can prove that $g$ is also total (which is sometimes called "extension lemma"), so it would arguably make more sense, from the point of view of effectivity, to ask about "minimal" totality instead of "maximal" totality: if $h$ is some element (possibly partial), what is a minimal way to extend it to an $f$ which will be total? (that we can extend it to a total at all is the content of the fundamental *density theorem*, see [[Normann 2008]](https://zbmath.org/?q=an:1148.68405)). And then: if $f$ is already total, what is a minimal *equivalent* total $g$ (that is, a total $g$ which agrees with $f$ on its total inputs)? Of relevance here is the characterization by [[Longo & Moggi 1984]](https://zbmath.org/?q=an:0599.03051) of two totals being equivalent exactly when they have a total intersection.

But back to the "maximal" totality. One more thing we can prove is that two totals are equivalent if and only if they are bounded. From this follows that, given a total $f$, a first answer to your question is
$$g^{\max} = \bigsqcup \{g \mid g \mbox{ is total and equivalent to }f\} .$$
This thing *does* exist, since domains are bounded-complete.

But I say "a first answer", because I can't think clearly now of an actual *technique*, as you specifically ask, of providing this supremum. In other words, I'm not sure of how constructive all the relevant steps are in this thread of thought. Perhaps someone can comment on this aspect (or I might, if I find the time to think about it with a clear head).


---

