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?