Countable nondeterminism (or unbounded nondeterminism) is a computational effect which nondeterministically chooses a natural number.
Countable nondetermnism presents many semantic difficulties. There's a host of literature, a lot of it from the 1980s and 1990s, that concerns the various models that one can use.
This famously led Edsger Dijkstra to argue that countable nondeterminism cannot be implemented [Dijkstra 1976].
Need more detail on this argument - it has to do with fairness. Don't have the book close. Also look at Hoare comments in CACM article on CSP.
In an imperative language, this may syntactically appear as a command of the form
whose effect is to set the variable x to any natural number - see e.g. [Apt and Plotkin 1986].
In a functional language, this may appear as an expression of the form
which may nondeterministically reduce to any natural number. This makes the operation not referentially transparent, and hence effectful.
Countable nondeterminism is related to the notion of fairness (and hence to concurrency).
In [Dijkstra 1976, p. 76] a program which sets a variable x to an arbitrary natural number is given, in the language of Dijkstra's guarded commands ():
b := true; x := 0;
do
b -> x := x+1
[]
b -> b := false
od
At each iteration of the loop, this program nondeterministically chooses to either increment x, or to set b to false and thus stop looping.
We say that has weakly fair iteration if each guard that is continuously enabled is not indefinitely postponed. For example, if has weakly fair iteration then the above program will not be able to loop forever. It will thus act as an implementation of the countable choice construct x := ?. This observation is mentioned in [Apt and Plotkin 1986].
Conversely, if we have a countable choice construct x := ?, then we can implement weakly fair iteration! For example, the weakly fair iteration command
do B_1 -> C_1 [] ... [] B_n -> Cn od
can be simulated by
do (B_1 v ... v B_n) ->
x1 := ?; ...; xn := ?;
do
x1 >= 0 ->
x1 := x1 - 1; if B1 -> C1 fi
[]
...
[]
xn >= 0 ->
xn := xn - 1; if Bn -> Cn fi
od
This example comes from [Giantonio et al. 1995].
Dijkstra, Edsger W. 1976. A Discipline of Programming. Prentice-Hall. [archive.org]
@book{dijkstra_1976,
title = {A {Discipline} of {Programming}},
isbn = {978-0-13-215871-8},
publisher = {Prentice-Hall},
author = {Dijkstra, Edsger W.},
year = {1976}
}
Apt, K. R., and G. D. Plotkin. 1986. ‘Countable Nondeterminism and Random Assignment’. Journal of the ACM 33 (4): 724–67. https://doi.org/10.1145/6490.6494.
@article{apt_1986,
title = {Countable nondeterminism and random assignment},
volume = {33},
doi = {10.1145/6490.6494},
number = {4},
journal = {Journal of the ACM},
author = {Apt, K. R. and Plotkin, G. D.},
year = {1986},
pages = {724--767}
}
Gianantonio, Pietro Di, Furio Honsell, and G. D. Plotkin. 1995. ‘Uncountable Limits and the Lambda Calculus’. Nordic Journal of Computing 2 (2): 126–45. [pdf]
@article{gianantonio_1995,
title = {Uncountable {Limits} and the {Lambda} {Calculus}},
volume = {2},
number = {2},
journal = {Nordic Journal of Computing},
author = {Gianantonio, Pietro Di and Honsell, Furio and Plotkin, G. D.},
year = {1995},
pages = {126--145},
}
Birkedal, Lars, Ale Bizjak, and Jan Schwinghammer. 2013. ‘Step-Indexed Relational Reasoning for Countable Nondeterminism’. Logical Methods in Computer Science 9 (4). https://doi.org/10.2168/LMCS-9(4:4)2013.
@article{birkedal_2013,
title = {Step-{Indexed} {Relational} {Reasoning} for {Countable} {Nondeterminism}},
volume = {9},
doi = {10.2168/LMCS-9(4:4)2013},
number = {4},
journal = {Logical Methods in Computer Science},
author = {Birkedal, Lars and Bizjak, Ale and Schwinghammer, Jan},
year = {2013}
}