I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates.  Given:$P$ is a family of programs, parameterized by a function $f$. Write $P_f$ for a particular program from this family.We know that $P_f$ is correct.$g$ is partial function from the same domain to the same range as $f$.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?
Using partial functions to prove correctness
lo.logic;functional programming;program verification;set theory
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.