Using partial functions to prove correctness

Question

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given:

1. $P$ is a family of programs, parameterized by a function $f$. Write $P_f$ for a particular program from this family.
2. We know that $P_f$ is correct.
3. $g$ is partial function from the same domain to the same range as $f$.
4. Moreover, $g$ is a subset of $f$; that is, for all $x$ where $g(x)$ is defined, $g(x) = f(x)$.

I'd like to show that $P_g$, wherever it terminates, gives the correct answer. This seems intuitively obvious. However, I'm struggling to find the appropriate math for it.

Most importantly, if we use functions instead of programs the claim is not correct. For example, if $Q$ is a multivariable function, $Q(f,n)$ does not in general equal $Q(g,n)$, even if they're both defined. However, if we think of $Q$ not as a function but as a program, which gets to use $f$ and $g$ as oracles, then they are. What is the proper way to show that mathematically? Or, even simpler: What is the correct mathematical term for $Q$? If it's not a function, what is it?

---

By program, I mean "algorithm which makes use of an other algorithm"; I'm not referring to any particular language or implementation. Note that even in functional languages like Haskell, due to the Halting Problem, a program is not truly a function: a program isn't guaranteed to terminate, whereas the concept of terminating doesn't apply to functions. A function of $f$ can depend on whether $f$ terminates, but no program which uses $f$ as a subroutine can.

Indeed, this is the essence of waht I'm struggling with: What is the appropriate mathematical formalism for a program which uses other programs as subroutines?

Answer 1

I will attempt to write the same answer as Neel with fewer technicalities (and therefore not really correct). By the way, you are using very strange terminology, which I will avoid.

For each type $T$ appearing in a programming language we can define a partial order $\leq_T$ as follows:

• on the integers we define $p \leq_{\mathtt{int}} q$ to mean: "if $p$ terminates then $q$ terminates and they evaluate to the same integer value".

• on the function type $A \to B$ we define $p \leq_{A \to B} q$ to mean: "for all $x: A$, $p(x) \leq_B q(x)$".

Caveat: do not think that because I called it a "function type" it has anything to do with your use of the word "function". I am using standard terminology: the type of "things" which accept $A$ and return $B$ is called a "function type".

Observe that $f \leq_{\mathtt{int} \to \mathtt{int}} g$ means: "if $f(n)$ terminates then so does $g(n)$ and $f(n) = g(n)$", which you expressed by saying that "$f$ is a subset of $g$" (probably because someone baked in set theory into you a long time ago, and now it's doing some harm).

Now, it is a matter of fact that for a reasonable programming language we have monotonicity of every $p : A \to B$, namely if $x \leq_A y$ then $p(x) \leq_B p(y)$. When we look at what monotonicity means for $P : (\mathtt{int} \to \mathtt{int}) \to \mathtt{int}$ we get the notion you are looking for: if $f \leq_{\mathtt{int} \to \mathtt{int}} g$ then, either $P(f)$ is undefined or both $P(f)$ and $P(g)$ are defined an equal.

If you'd like to know more, have a look at domain theory where these concepts are properly developed.

Answer 2

If I read you correctly, the intuition you have in mind goes like this:

Suppose we have a program $P$, which takes a function as an argument. Further suppose that we have two functions $f$ and $g$, such that $f$ terminates on a subset of the inputs $g$ terminates on, but agrees with $g$ whenever they both terminate.

Now, if $P\;g$ is partially correct, then you want to argue that $P\;f$ must also be partially correct. After all, the "only thing" that $P$ can do with its functional parameter is to apply it (what you call "use as an oracle"), and so $P\;f$ must compute the same values as $P\;g$, possibly terminating less often.

This is more or less exactly the intuition underlying domain theory. The idea is that we can interpret computations at a particular type as CPPOs, or chain-complete pointed partial orders.

That is, a CPPO is a triple $(X, \bot, \leq)$, with $X$ as the set of elements denoting computations, $\bot$ as the nonterminating computation, and $\leq$ as a partial order representing how close to fully defined a computation is. $\bot$ is the least element in this partial order, and the chain-completeness condition says that if you have a countable chain $x_0 \leq x_1 \leq \ldots$, then the chain has a least upper bound $\bigsqcup_{i \in \mathbb{N}} x_i$.

Programs are interpreted by continuous functions between CPPOs, with the idea that continuity is a stand-in for computability. That is, a function $f : X \to Y$ should be a monotone function which preserves lubs.

In particular, the set of continuous functions $X \to Y$ also forms a CPPO, with the least element given by $\lambda x.\;\bot_Y$, and the order given pointwise, so that

$$f \leq_{X \to Y} g \iff \forall x \in X.\; f\;x \leq_Y g\;x$$

Then the property you want follows more or less instantaneously. Suppose we have a continuous $P : (X \to Y) \to Z$. Then $f$ being "less defined" than $g$ amounts to saying that $f \leq g$. Then, by the continuity of $P$, it follows that $P\;f \leq P\;g$.

Samson Abramsky and Achim Jung have a chapter on domain theory in the Handbook on Logic in Computer Science, which is freely available online.