PLS Lab

Demonic nondeterminism

Demonic nondeterminism is a type of nondeterminism in which the "worst" possible action will be chosen.

The definition of "worst" depends on the setting.

In a functional setting

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

For example, when faced with the nondeterministic choice

(\lambda x. x) \oplus \bot

it will always pick \bot.

In domain theory

In domain theory, (locally) demonic nondeterminism is modelled using the Smyth powerdomain.

Søndergaard and Sestoft 1992 report that the domain-theoretic point of view may only model global demonic 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 \sqcap Q)\ \phi = \textsf{wp}\ P\ \phi \land \textsf{wp}\ Q\ \phi

Thus, for the nondeterministic choice P \sqcap Q to be "safe," both the preconditions of P and Q must hold.

See also

References

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}
}
  • The classification demonic/angelic/erratic seems to originate in
 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}
}