1
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ You seem to be making a distinction between functions and programs. What exactly is this distinction? Can you give a concrete example, please. (I suspect you are distinguishing between extensional and intensional behavior.) $\endgroup$ – Andrej Bauer Oct 14 '13 at 5:00
  • 1
    $\begingroup$ Unless we know more about your setup (what is your programming language), we cannot answer this. For instance, in certain programming languages, such as Haskell, the distinction you are describing does not exist. $\endgroup$ – Andrej Bauer Oct 14 '13 at 5:02
  • $\begingroup$ @Andrej Thanks - I updated the post to clarify. Your comment goes to the essence of my question: What is the right formalism for programs which take subroutines (neither of which is guaranteed to terminate, and neither of which can solve the Halting Problem)? $\endgroup$ – Jodag Oct 14 '13 at 5:13
  • $\begingroup$ @Jodag I'm not sure I fully understand your question, but the answer is likely to be to use some variant of Hoare logic. $\endgroup$ – Martin Berger Oct 14 '13 at 9:49
  • $\begingroup$ @Martin I posted a similar question with a more precise specification cstheory.stackexchange.com/questions/19381/… $\endgroup$ – Jodag Oct 14 '13 at 19:26
3
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ This of course is the correct answer, but let us see if @Jodag will recognize it as such. It may be a bit abstract. $\endgroup$ – Andrej Bauer Oct 14 '13 at 21:03
  • $\begingroup$ @AndrejBauer Most non-trivial programming languages are not known to have domain theoretic semantics that capture the relevant operational behaviour. That said, you can use some of the abstract theory of domain theory, when doing an operational proof of the relevant property. $\endgroup$ – Martin Berger Oct 14 '13 at 21:12
  • $\begingroup$ But we only need an adequate semantics for this discussion, not full abstraction. So domain theory is perfectly ok. $\endgroup$ – Andrej Bauer Oct 14 '13 at 21:31
  • $\begingroup$ @AndrejBauer Sure, but for most interesting language features there are no know domain-theoretic semantics, e.g. Scala's Implicits with their resolution-like parameter lookup, Haskell's compile-time meta-programming, Erlang's process supervision trees, Javascript's eval, etc etc. $\endgroup$ – Martin Berger Oct 16 '13 at 10:54
  • $\begingroup$ The principle of monotonicity of information processing (can't compute more output with less input) is fundamental. Domain theory is certainly a natural mathematical formalism for its expression. If there are features of programming languages that do not obviously fit into domain theory (I don't actually buy that, by the way, the ones you listed do, possibly with a little bit of elaboration), do you know how to express monotonicity outside a domain-theoretic context? In terms of operational observations maybe? $\endgroup$ – Andrej Bauer Oct 16 '13 at 12:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.