<p>In [dB80] Hitchcock and Park's analysis of the termination properties
of recursion is proven to correspond to a semantic analysis based on
the so-called Egli-Milner interpretation of relations [Egl75, Plo76],
which expresses <em>erratic</em> nondeterminism. This notion captures
that a nondeterministic union of relations is correct if it generates
at least one computation leading to a desired result (even in the
presence of a nonterminating computation). This appears to correspond
to what you are trying to do.</p>

<p>Next characterize the meaning of a statement $S$ as a function $f_S$
mapping each initial state $\sigma$ to some nonempty set of states,
possibly containing $\bot$, such that $f_S$ is strict in the sense
that $f_S(\bot) = \{\bot\}$. The nondeterministic choice between
statements $S_1$ and $S_2$ is described by the function mapping each
initial state $\sigma$ to the union of the individual results $f_{S_1}
(\sigma) \cup f_{S_2} (\sigma)$. Thus, whenever $S_1$ or $S_2$ has the
nondeterministic possibility of producing an undesirable result, then
so does their nondeterministic choice. As the resulting sets of final
states one obtains in this analysis the so-called Egli-Milner
powerset of states:</p>

<p>${\cal P}_{\text{E--M}}(S) = \{ ~s\subseteq S_\bot ~|~ s$ is finite and nonempty, or contains $\bot\}$</p>

<p>Why are infinite subsets of $S$ not considered possible sets of final
states in this model? Under the assumption that all basic building
blocks of relational terms produce only finite, nonempty sets of
possible final states, an infinite set of possible final states can
only be generated when an infinite computation is possible. This can
be seen as follows. Structure the set of all possible computations
starting in a given state $\sigma_0$ as a tree with root $\sigma_0$
and states as nodes. The set of leaves is then exactly the set of
possible final states reachable from $\sigma_0$, except for $\bot$,
which might be missing among the leaves but is represented in the set
of final states by the fact that there is an infinite path in the
tree. By the assumption above, and since only finite nondeterministic
choice is available, this tree is finitely branching. Thus, there is
only a finite number of leaves at any given finite depth. Consequently
an infinite number of possible final states can only be generated in
the presence of an infinite computation (an application of König's
lemma [Kön32]).</p>

<p>$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ is a poset for
$\sqsubseteq_{\text{E--M}}$ defined by: for $s,t\in{\cal
  P}_{\text{E--M}}(S)$,</p>

<p>$
  s\sqsubseteq_{\text{E--M}} t\quad = \quad
  (\bot\in s \land s\setminus\{\bot\}\subseteq t)
  \lor (\bot\notin s \land s=t)~.
$</p>

<p>Here, $\bot$ can be seen as a placeholder through which
$\sqsubseteq_{\text{E--M}}$-greater sets can be generated by inserting
more states in lieu of $\bot$. Therefore, $\{\bot\}$ is the least
element of $({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$.
Furthermore, the poset $({\cal
  P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ possesses lub's for
$\omega$-chains. Similarly, the strict functions from $S\cup\{\bot\}$
to ${\cal P}_{\text{E--M}}(S)$ are partially ordered by the pointwise
extension of $\sqsubseteq_{\text{E--M}}$. Moreover, the least such
function is $\lambda\sigma.\{\bot\}$ and lub's of $\omega$-chains of
such functions exist, too.</p>

<p>[dB80] JW de Bakker. <em>Mathematical Theory of Program Correctness</em>.
Prentice Hall, 1980.</p>

<p>[Egl75] H Egli. A mathematical model for nondeterministic
computations. Technical report, ETH Zürich, 1975.</p>

<p>[Kön32] D König. Theorie der endlichen und unendlichen Graphen.
Technical report, Leipzig, 1932.</p>

<p>[Plo76] GD Plotkin. A powerdomain construction. <em>SIAM Journal on
  Computation</em>, 5(3):452-487, 1976.</p>

<p>Disclaimer: this is taken almost verbatim from a book I once co-authored:</p>

<p>WP de Roever and K Engelhardt. <em>Data Refinement: Model-Oriented
  Proof Methods and their Comparison</em>. Cambridge University Press, 1998.</p>

CC BY-SA 3.0
2011-07-14T12:41:25.750Z
The phrase "this is taken almost verbatium from a book I once co-authored" should probably be prefixed with "Extra Awesomeness:" not "Disclaimer:" :-D. Thanks, this is very helpful.
Rob Simmons
CC BY-SA 3.0
2011-07-16T17:28:43.550Z
One way of looking at nondeterminism (and the way I want to look at it) is that it is a form of *underspecification* - a program with a nondeterministic choice is *refined* by the program that always takes the first choice, always takes the second choice, or (see McIver and Morgan's extensive work in this particular area) *the program that takes one choice or the other with probability .5*. So the loop that non-deterministically doesn't terminate is refined by the loop that *never* terminates, and also by your coin-flip loop that terminates (with probability 1)
Rob Simmons
CC BY-SA 3.0
2011-07-14T06:18:02.613Z
2011-07-14T06:26:42.230Z
2011-07-14T06:26:42.230Z
Kai
<p>Here's a "track B" question if there ever was one. Summary: the first thing I think of when I try to give a semantics to non-deterministic programs results in a semantics where I can't prove things about loops that only terminate non-deterministicaly. Surely someone has worked out what to do in this situation, or at least pointed out that it's hard, but I don't know how to go about looking for it (hence the "reference request" tag).</p>

<h2>Background</h2>

<p>I want to model an while-language with non-determinism. I think this is the obvious (or at least the naive) way to model such a language with a Smyth powerdomain, but correct me if I'm wrong. We will model the meaning of a command in this language is as a function whose domain is the set $S$ of states and whose codomain is the set ${\cal P}(S)_\bot = \{ \bot \} \cup {\cal P}(S)$, where $\bot$ is a least element representing non-termination and ${\cal P}(S)$ is the powerset of states.</p>

<p>We interpret commands as maps from states $\sigma$ to either the non-termination event $\bot$ or to sets of states $\{ \sigma_1, \sigma_2, \ldots \}$ which represent possible outcomes. $P \circledast Q$ is non-deterministic choice.</p>

<ul>
<li>$⟦\mathbf{skip}⟧\sigma = \{ \sigma \}$</li>
<li>$⟦x := E⟧\sigma = \{ \sigma[(⟦E⟧\sigma)/x] \}$</li>
<li>$⟦\mathbf{abort}⟧\sigma = \bot$</li>
<li>$⟦\mathbf{if}~E~\mathbf{then}~P~\mathbf{else}~Q⟧\sigma = ⟦P⟧\sigma$ if $⟦E⟧\sigma = \mathit{true}$, otherwise $⟦Q⟧\sigma$</li>
<li>$⟦P \circledast Q⟧\sigma = \bot$ if $⟦P⟧\sigma = \bot$ or $⟦Q⟧\sigma = \bot$, otherwise $⟦P⟧\sigma \cup ⟦Q⟧\sigma$</li>
<li>$⟦P; Q⟧\sigma = \bot$ if $⟦P⟧\sigma = \bot$ or $⟦Q⟧\tau = \bot$ for some $\tau \in ⟦P⟧\sigma$, otherwise $\bigcup_{\tau \in ⟦P⟧\sigma} ⟦Q⟧\tau$</li>
</ul>

<p>There's a directed complete partial order $\sqsubseteq$, where $\bot \sqsubseteq S&#39;$ for any $S&#39; \in {\cal P}(S)_\bot$ and $S_1 \sqsubseteq S_2$ if both $S_1$ and $S_2$ are proper sets and $S_1 \supseteq S_2$, and we can extend this to functions $f$ from $S$ to ${\cal P}(S)_\bot$ pointwise: $f_1 \sqsubseteq f_2$ if $f_1(\sigma) \sqsubseteq f_2(\sigma)$ for every $\sigma$, and $f_\bot$ is the function that maps every state to $\bot$.</p>

<p>The meaning of a loop is $⟦\mathbf{while}~E~\mathbf{do}~P⟧\sigma$ is the least upper bound of the chain $f_\bot \sqsubseteq f(f_\bot) \sqsubseteq f(f(f_\bot)) \sqsubseteq \ldots$, where $f(g)(\sigma) = \{\sigma\}$ if $⟦E⟧(\sigma) = \mathit{false}$, otherwise $\bot$ if $⟦P⟧\sigma = \bot$ or $g(\tau) = \bot$ for some $\tau \in ⟦P⟧\sigma$, otherwise $\bigcup_{\tau \in ⟦P⟧\sigma}g(\tau)$. (This definition assumes that the $f$ I just defined is Scott continuous, but I think it's safe to leave that aside.)</p>

<h2>Question</h2>

<p>Consider this program:</p>

<p>$x := 0;$<br/>
$b := \mathsf{true};$<br/>
$\mathbf{while}~b~\mathbf{do}$<br/>
$\qquad x := x + 2;$<br/>
$\qquad b := \mathsf{false} \circledast b := \mathsf{true}$</p>

<p>Intuitively, this is a loop that can return any positive even number or not terminate, and that corresponds to what we can prove about this loop using the weakest liberal precondition (it is possible to show that $\exists n. x = 2n$ is a loop invariant). However, because the loop has the ability not to terminate (we can refine the non-deterministic choice by the program that always takes the right-hand branch), the meaning of this program given any initial state is $\bot$. (Less informally: the function that maps any state where $b$ is false to itself and any state where $b$ is true to $\bot$ is a fixed point of the $f$ used to define the loop.)</p>

<p>This means that the naive semantics I proposed doesn't correspond in the way I expect to be able to reason about programs. I blame my semantics, but don't how to fix them.</p>

CC BY-SA 3.0
2011-07-11T19:24:58.377Z
I think that by using $\{ \bot \} \cup \mathcal{P}(S)$ as the codomain of the meaning of a program, you have effectively given up reasoning anything about a program which can diverge.  A naive thought is to use $\mathcal{P}(S \cup \{ \bot \})$, but I do not know if that will introduce another problem.
Tsuyoshi Ito
CC BY-SA 3.0
2011-07-12T06:22:55.230Z
Yes, you're absolutely right that looking at the set $\{ \bot \} \cup \mathcal P(S)$ it is already apparent that hope is lost even before we get to the example. Your suggestion occured to me as well, but I think you end up with the same problem in this example is long as potential non-termination is modeled by $S \cup \{ \bot \}$ not $\{ \bot \}$, and if we chose the latter it would interfere with our ability to give meaning to a loop as a least fixed point in the usual way.
Rob Simmons
CC BY-SA 3.0
2011-07-14T07:13:37.650Z
Have you looked at Dynamic Logic? The semantics is given in terms of relations from states to states, and you can use the logic to reason about partial and total correctness, which is to say, the the properties of computations that terminate and that all computations terminate with a given property.
Dave Clarke
CC BY-SA 3.0
2011-07-14T08:33:50.787Z
I haven't thought about dynamic logic in this setting, but I see how it might be relevant - I'll see what Platzer and his students think when I'm back in Pittsburgh.
Rob Simmons
<reference-request><denotational-semantics>
Reasoning about non-deterministically terminating loops
Rob Simmons
# Reasoning about non-deterministically terminating loops

(Asked by: username_0 on 2011-07-11)

Here's a "track B" question if there ever was one. Summary: the first thing I think of when I try to give a semantics to non-deterministic programs results in a semantics where I can't prove things about loops that only terminate non-deterministicaly. Surely someone has worked out what to do in this situation, or at least pointed out that it's hard, but I don't know how to go about looking for it (hence the "reference request" tag).

## Background

I want to model an while-language with non-determinism. I think this is the obvious (or at least the naive) way to model such a language with a Smyth powerdomain, but correct me if I'm wrong. We will model the meaning of a command in this language is as a function whose domain is the set $S$ of states and whose codomain is the set ${\cal P}(S)\_\bot = \{ \bot \} \cup {\cal P}(S)$, where $\bot$ is a least element representing non-termination and ${\cal P}(S)$ is the powerset of states.

We interpret commands as maps from states $\sigma$ to either the non-termination event $\bot$ or to sets of states $\{ \sigma\_1, \sigma\_2, \ldots \}$ which represent possible outcomes. $P \circledast Q$ is non-deterministic choice.

* $⟦\mathbf{skip}⟧\sigma = \{ \sigma \}$
* $⟦x := E⟧\sigma = \{ \sigma[(⟦E⟧\sigma)/x] \}$
* $⟦\mathbf{abort}⟧\sigma = \bot$
* $⟦\mathbf{if}~E~\mathbf{then}~P~\mathbf{else}~Q⟧\sigma = ⟦P⟧\sigma$ if $⟦E⟧\sigma = \mathit{true}$, otherwise $⟦Q⟧\sigma$
* $⟦P \circledast Q⟧\sigma = \bot$ if $⟦P⟧\sigma = \bot$ or $⟦Q⟧\sigma = \bot$, otherwise $⟦P⟧\sigma \cup ⟦Q⟧\sigma$
* $⟦P; Q⟧\sigma = \bot$ if $⟦P⟧\sigma = \bot$ or $⟦Q⟧\tau = \bot$ for some $\tau \in ⟦P⟧\sigma$, otherwise $\bigcup\_{\tau \in ⟦P⟧\sigma} ⟦Q⟧\tau$

There's a directed complete partial order $\sqsubseteq$, where $\bot \sqsubseteq S'$ for any $S' \in {\cal P}(S)\_\bot$ and $S\_1 \sqsubseteq S\_2$ if both $S\_1$ and $S\_2$ are proper sets and $S\_1 \supseteq S\_2$, and we can extend this to functions $f$ from $S$ to ${\cal P}(S)\_\bot$ pointwise: $f\_1 \sqsubseteq f\_2$ if $f\_1(\sigma) \sqsubseteq f\_2(\sigma)$ for every $\sigma$, and $f\_\bot$ is the function that maps every state to $\bot$.

The meaning of a loop is $⟦\mathbf{while}~E~\mathbf{do}~P⟧\sigma$ is the least upper bound of the chain $f\_\bot \sqsubseteq f(f\_\bot) \sqsubseteq f(f(f\_\bot)) \sqsubseteq \ldots$, where $f(g)(\sigma) = \{\sigma\}$ if $⟦E⟧(\sigma) = \mathit{false}$, otherwise $\bot$ if $⟦P⟧\sigma = \bot$ or $g(\tau) = \bot$ for some $\tau \in ⟦P⟧\sigma$, otherwise $\bigcup\_{\tau \in ⟦P⟧\sigma}g(\tau)$. (This definition assumes that the $f$ I just defined is Scott continuous, but I think it's safe to leave that aside.)

## Question

Consider this program:

$x := 0;$  
$b := \mathsf{true};$  
$\mathbf{while}~b~\mathbf{do}$  
$\qquad x := x + 2;$  
$\qquad b := \mathsf{false} \circledast b := \mathsf{true}$

Intuitively, this is a loop that can return any positive even number or not terminate, and that corresponds to what we can prove about this loop using the weakest liberal precondition (it is possible to show that $\exists n. x = 2n$ is a loop invariant). However, because the loop has the ability not to terminate (we can refine the non-deterministic choice by the program that always takes the right-hand branch), the meaning of this program given any initial state is $\bot$. (Less informally: the function that maps any state where $b$ is false to itself and any state where $b$ is true to $\bot$ is a fixed point of the $f$ used to define the loop.)

This means that the naive semantics I proposed doesn't correspond in the way I expect to be able to reason about programs. I blame my semantics, but don't how to fix them.

**Tags:** reference-request, denotational-semantics
> **Comments:**
> **username_1**: I think that by using $\{ \bot \} \cup \mathcal{P}(S)$ as the codomain of the meaning of a program, you have effectively given up reasoning anything about a program which can diverge.  A naive thought is to use $\mathcal{P}(S \cup \{ \bot \})$, but I do not know if that will introduce another problem.  
> **username_0**: Yes, you're absolutely right that looking at the set $\{ \bot \} \cup \mathcal P(S)$ it is already apparent that hope is lost even before we get to the example. Your suggestion occured to me as well, but I think you end up with the same problem in this example is long as potential non-termination is modeled by $S \cup \{ \bot \}$ not $\{ \bot \}$, and if we chose the latter it would interfere with our ability to give meaning to a loop as a least fixed point in the usual way.  
> **username_2**: Have you looked at Dynamic Logic? The semantics is given in terms of relations from states to states, and you can use the logic to reason about partial and total correctness, which is to say, the the properties of computations that terminate and that all computations terminate with a given property.  
> **username_0**: I haven't thought about dynamic logic in this setting, but I see how it might be relevant - I'll see what Platzer and his students think when I'm back in Pittsburgh.  

---

## 1 answers

### Answer by username_3 on 2011-07-14. Score: 10 | Accepted answer

In [dB80] Hitchcock and Park's analysis of the termination properties
of recursion is proven to correspond to a semantic analysis based on
the so-called Egli-Milner interpretation of relations [Egl75, Plo76],
which expresses *erratic* nondeterminism. This notion captures
that a nondeterministic union of relations is correct if it generates
at least one computation leading to a desired result (even in the
presence of a nonterminating computation). This appears to correspond
to what you are trying to do.

Next characterize the meaning of a statement $S$ as a function $f\_S$
mapping each initial state $\sigma$ to some nonempty set of states,
possibly containing $\bot$, such that $f\_S$ is strict in the sense
that $f\_S(\bot) = \{\bot\}$. The nondeterministic choice between
statements $S\_1$ and $S\_2$ is described by the function mapping each
initial state $\sigma$ to the union of the individual results $f\_{S\_1}
(\sigma) \cup f\_{S\_2} (\sigma)$. Thus, whenever $S\_1$ or $S\_2$ has the
nondeterministic possibility of producing an undesirable result, then
so does their nondeterministic choice. As the resulting sets of final
states one obtains in this analysis the so-called Egli-Milner
powerset of states:

${\cal P}\_{\text{E--M}}(S) = \{ ~s\subseteq S\_\bot ~|~ s$ is finite and nonempty, or contains $\bot\}$

Why are infinite subsets of $S$ not considered possible sets of final
states in this model? Under the assumption that all basic building
blocks of relational terms produce only finite, nonempty sets of
possible final states, an infinite set of possible final states can
only be generated when an infinite computation is possible. This can
be seen as follows. Structure the set of all possible computations
starting in a given state $\sigma\_0$ as a tree with root $\sigma\_0$
and states as nodes. The set of leaves is then exactly the set of
possible final states reachable from $\sigma\_0$, except for $\bot$,
which might be missing among the leaves but is represented in the set
of final states by the fact that there is an infinite path in the
tree. By the assumption above, and since only finite nondeterministic
choice is available, this tree is finitely branching. Thus, there is
only a finite number of leaves at any given finite depth. Consequently
an infinite number of possible final states can only be generated in
the presence of an infinite computation (an application of König's
lemma [Kön32]).

$({\cal P}\_{\text{E--M}}(S),\sqsubseteq\_{\text{E--M}})$ is a poset for
$\sqsubseteq\_{\text{E--M}}$ defined by: for $s,t\in{\cal
P}\_{\text{E--M}}(S)$,

$
s\sqsubseteq\_{\text{E--M}} t\quad = \quad
(\bot\in s \land s\setminus\{\bot\}\subseteq t)
\lor (\bot\notin s \land s=t)~.
$

Here, $\bot$ can be seen as a placeholder through which
$\sqsubseteq\_{\text{E--M}}$-greater sets can be generated by inserting
more states in lieu of $\bot$. Therefore, $\{\bot\}$ is the least
element of $({\cal P}\_{\text{E--M}}(S),\sqsubseteq\_{\text{E--M}})$.
Furthermore, the poset $({\cal
P}\_{\text{E--M}}(S),\sqsubseteq\_{\text{E--M}})$ possesses lub's for
$\omega$-chains. Similarly, the strict functions from $S\cup\{\bot\}$
to ${\cal P}\_{\text{E--M}}(S)$ are partially ordered by the pointwise
extension of $\sqsubseteq\_{\text{E--M}}$. Moreover, the least such
function is $\lambda\sigma.\{\bot\}$ and lub's of $\omega$-chains of
such functions exist, too.

[dB80] JW de Bakker. *Mathematical Theory of Program Correctness*.
Prentice Hall, 1980.

[Egl75] H Egli. A mathematical model for nondeterministic
computations. Technical report, ETH Zürich, 1975.

[Kön32] D König. Theorie der endlichen und unendlichen Graphen.
Technical report, Leipzig, 1932.

[Plo76] GD Plotkin. A powerdomain construction. *SIAM Journal on
Computation*, 5(3):452-487, 1976.

Disclaimer: this is taken almost verbatim from a book I once co-authored:

WP de Roever and K Engelhardt. *Data Refinement: Model-Oriented
Proof Methods and their Comparison*. Cambridge University Press, 1998.

> **Comments:**
> **username_0**: The phrase "this is taken almost verbatium from a book I once co-authored" should probably be prefixed with "Extra Awesomeness:" not "Disclaimer:" :-D. Thanks, this is very helpful.  
> **username_0**: One way of looking at nondeterminism (and the way I want to look at it) is that it is a form of *underspecification* - a program with a nondeterministic choice is *refined* by the program that always takes the first choice, always takes the second choice, or (see McIver and Morgan's extensive work in this particular area) *the program that takes one choice or the other with probability .5*. So the loop that non-deterministically doesn't terminate is refined by the loop that *never* terminates, and also by your coin-flip loop that terminates (with probability 1)  

---

