<p>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.</p>

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

<ul>
<li><p>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".</p></li>
<li><p>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)$".</p></li>
</ul>

<p>Caveat: do <em>not</em> 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".</p>

<p>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). </p>

<p>Now, it is a matter of fact that for a reasonable programming language we have <em>monotonicity</em> 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.</p>

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

CC BY-SA 3.0
2013-10-14T21:27:39.383Z
2013-10-14T21:27:39.383Z
Andrej Bauer
<p>If I read you correctly, the intuition you have in mind goes like this:</p>

<p>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.</p>

<p>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. </p>

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

<p>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$. </p>

<p>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.</p>

<p>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 </p>

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

<p>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$. </p>

<p>Samson Abramsky and Achim Jung <a href="http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf" rel="nofollow">have a chapter on domain theory in the Handbook on Logic in Computer Science, which is freely available online</a>. </p>

CC BY-SA 3.0
2013-10-14T21:03:24.980Z
This of course is the correct answer, but let us see if @Jodag will recognize it as such. It may be a bit abstract.
Andrej Bauer
CC BY-SA 3.0
2013-10-14T21:12:36.463Z
@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.
Martin Berger
CC BY-SA 3.0
2013-10-14T21:31:00.477Z
But we only need an adequate semantics for this discussion, not full abstraction. So domain theory is perfectly ok.
Andrej Bauer
CC BY-SA 3.0
2013-10-16T10:54:03.497Z
@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.
Martin Berger
CC BY-SA 3.0
2013-10-16T12:52:00.987Z
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?
Andrej Bauer
CC BY-SA 3.0
2013-10-14T20:52:59.923Z
2013-10-14T20:52:59.923Z
Neel Krishnaswami
<p>I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates.  Given:</p>

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

<p>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.</p>

<p>Most importantly, <strong>if we use functions</strong> instead of programs <strong>the claim is <em>not</em> correct</strong>.  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?</p>

<hr>

<p>By <em>program</em>, 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.</p>

<p>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?</p>

CC BY-SA 3.0
2013-10-14T05:00:54.917Z
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.)
Andrej Bauer
CC BY-SA 3.0
2013-10-14T05:02:09.063Z
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.
Andrej Bauer
CC BY-SA 3.0
2013-10-14T05:13:29.330Z
@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)?
Jodag
CC BY-SA 3.0
2013-10-14T09:49:44.837Z
@Jodag I'm not sure I fully understand your question, but the answer is likely to be to use some variant of Hoare logic.
Martin Berger
CC BY-SA 3.0
2013-10-14T19:26:02.647Z
@Martin I posted a similar question with a more precise specification http://cstheory.stackexchange.com/questions/19381/program-transformation-using-partial-functions-which-preserve-partial-correctnes
Jodag
CC BY-SA 3.0
2013-10-14T21:04:54.673Z
You cannot "not refer to any programming language" because I could think of a programming language which can solve the halting problem. Anyhow, Neel's answer is what you are looking for.
Andrej Bauer
<lo.logic><functional-programming><program-verification><set-theory>
Using partial functions to prove correctness
Jodag
# Using partial functions to prove correctness

(Asked by: username_0 on 2013-10-14)

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?

**Tags:** lo.logic, functional-programming, program-verification, set-theory

> **Comments:**
> **username_1**: 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.)  
> **username_1**: 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.  
> **username_0**: @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)?  
> **username_2**: @username_0 I'm not sure I fully understand your question, but the answer is likely to be to use some variant of Hoare logic.  
> **username_0**: @Martin I posted a similar question with a more precise specification http://cstheory.stackexchange.com/questions/19381/program-transformation-using-partial-functions-which-preserve-partial-correctnes  
> **username_1**: You cannot "not refer to any programming language" because I could think of a programming language which can solve the halting problem. Anyhow, Neel's answer is what you are looking for.  

---

## 2 answers

### Answer by username_1 on 2013-10-14. Score: 3 | Accepted answer

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 by username_3 on 2013-10-14. Score: 4

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](http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf).

> **Comments:**
> **username_1**: This of course is the correct answer, but let us see if @username_0 will recognize it as such. It may be a bit abstract.  
> **username_2**: @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.  
> **username_1**: But we only need an adequate semantics for this discussion, not full abstraction. So domain theory is perfectly ok.  
> **username_2**: @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.  
> **username_1**: 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?  

---

