Prior work on finding domain-theoretic suprema of equivalent total functions?

Question

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?

Answer 1

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. It's a short and easy read, but your domain-fu will go way up for reading it.

Answer 2

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], 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, 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]). 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] 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).