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 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).
A distinction is often made between locally angelic vs. globally angelic nondeterminism.
In locally angelic nondeterminism, a choice between expressions and is resolved as to pick the locally more defined expression. For example, the expression should resolve to (where 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
Then, in the expression , the choice should always resolve to , as to lead to a well-defined output of .
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
When reasoning with Hoare logic and weakest preconditions, the operator implements demonic nondeterministic choice when
Thus, for the angelic nondeterministic choice to be "safe," at least one of the preconditions of and must hold. The choice will automatically resolve to the program whose precondition holds.
Broy, M., and M. Wirsing. 1981. ‘On the Algebraic Specification of Nondeterministic Programming Languages’. In CAAP ’81, edited by Egidio Astesiano and Corrado Böhm, 112:162–79. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-10828-9_61.
@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}
}
Søndergaard, H., and P. Sestoft. 1992. ‘Non-Determinism in Functional Languages’. The Computer Journal 35 (5): 514–23. https://doi.org/10.1093/comjnl/35.5.514.
@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}
}