Angelic nondeterminism

Angelic nondeterminism is a type of nondeterminism in which the "best possible" action will be chosen.

It usually refers to settings where nondeterminism and nontermination are both present. In that case, angelic nondeterminism will always resolve in a way that makes expressions more defined.

In a functional setting

In a functional programming language with nondeterminism, an angelic implementation will implement a nondeterministic choice by preferentially resolving to the branch that will avoid nontermination.

It is the earliest kind of nondeterminism expressed in a functional setting, through McCarthy's amb operator (1963).

Local vs. global

A distinction is often made between locally angelic vs. globally angelic nondeterminism.

In locally angelic nondeterminism, a choice e_1 \oplus e_2 between expressions e_1 and e_2 is resolved as to pick the locally more defined expression. For example, the expression \bot \oplus 1 should resolve to 1 (where \bot signifies a nonterminating program).

In globally angelic nondeterminism, on the other hand, choices are made as to obtain the best result from the overall computation. For example, suppose we have defined a function

f(x) = \begin{cases}
  0 & \text{ if $x = 1$} \\
  \bot & \text{ otherwise}
\end{cases}

Then, in the expression f(0 \oplus 1), the choice should always resolve to 1, as to lead to a well-defined output of f.

In domain theory

In Domain Theory, (locally) angelic nondeterminism is modelled using the Hoare powerdomain.

Søndergaard and Sestoft 1992 report that the domain-theoretic point of view may only model global angelic nondeterminism, as

a fixed-point theoretic characterization of these kinds of semantics is very difficult and still under investigation

In Hoare logic

When reasoning with Hoare logic and weakest preconditions, the operator \sqcap implements demonic nondeterministic choice when

\textsf{wp}\ (P \sqcup Q)\ \phi = \textsf{wp}\ P\ \phi \lor \textsf{wp}\ Q\ \phi

Thus, for the angelic nondeterministic choice P \sqcup Q to be "safe," at least one of the preconditions of P and Q must hold. The choice will automatically resolve to the program whose precondition holds.

See also

• Nondeterminism
• Demonic nondeterminism
• Erratic nondeterminism
• amb

References

• The classification demonic/angelic/erratic seems to originate in

@inproceedings{broy_1981,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {On the algebraic specification of nondeterministic programming languages},
	volume = {112},
	doi = {10.1007/3-540-10828-9_61},
	booktitle = {{CAAP} '81},
	publisher = {Springer Berlin Heidelberg},
	author = {Broy, M. and Wirsing, M.},
	editor = {Astesiano, Egidio and Böhm, Corrado},
	year = {1981},
	pages = {162--179}
}

• Angelic, demonic, and erratic nondeterminism are discussed in the survey article

@article{sondergaard_1992,
	title = {Non-determinism in {Functional} {Languages}},
	volume = {35},
	doi = {10.1093/comjnl/35.5.514},
	number = {5},
	journal = {The Computer Journal},
	author = {Søndergaard, H. and Sestoft, P.},
	year = {1992},
	pages = {514--523}
}