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).BackgroundI 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.)QuestionConsider 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.
Reasoning about non-deterministically terminating loops
reference request;denotational semantics
In [dB80] Hitchcock and Park's analysis of the termination propertiesof recursion is proven to correspond to a semantic analysis based onthe so-called Egli-Milner interpretation of relations [Egl75, Plo76],which expresses erratic nondeterminism. This notion capturesthat a nondeterministic union of relations is correct if it generatesat least one computation leading to a desired result (even in thepresence of a nonterminating computation). This appears to correspondto 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 sensethat $f_S(\bot) = \{\bot\}$. The nondeterministic choice betweenstatements $S_1$ and $S_2$ is described by the function mapping eachinitial 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 thenondeterministic possibility of producing an undesirable result, thenso does their nondeterministic choice. As the resulting sets of finalstates one obtains in this analysis the so-called Egli-Milnerpowerset 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 finalstates in this model? Under the assumption that all basic buildingblocks of relational terms produce only finite, nonempty sets ofpossible final states, an infinite set of possible final states canonly be generated when an infinite computation is possible. This canbe seen as follows. Structure the set of all possible computationsstarting 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 ofpossible final states reachable from $\sigma_0$, except for $\bot$,which might be missing among the leaves but is represented in the setof final states by the fact that there is an infinite path in thetree. By the assumption above, and since only finite nondeterministicchoice is available, this tree is finitely branching. Thus, there isonly a finite number of leaves at any given finite depth. Consequentlyan infinite number of possible final states can only be generated inthe presence of an infinite computation (an application of Knig'slemma [Kn32]).$({\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 insertingmore states in lieu of $\bot$. Therefore, $\{\bot\}$ is the leastelement 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 pointwiseextension of $\sqsubseteq_{\text{E--M}}$. Moreover, the least suchfunction is $\lambda\sigma.\{\bot\}$ and lub's of $\omega$-chains ofsuch functions exist, too.[dB80] JW de Bakker. Mathematical Theory of Program Correctness.Prentice Hall, 1980.[Egl75] H Egli. A mathematical model for nondeterministiccomputations. Technical report, ETH Zrich, 1975.[Kn32] D Knig. 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.