Countable nondeterminism

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.

Syntax

Imperative programming

In an imperative language, this may syntactically appear as a command of the form

x := ?

whose effect is to set the variable x to any natural number - see e.g. Apt and Plotkin 1986.

Functional programming

In a functional language, this may appear as an expression of the form

\Gamma \vdash \mathbin{?} : \textsf{Nat}

which may nondeterministically reduce to any natural number. This makes the ? operation not referentially transparent, and hence effectful.

Relation to fairness

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 (\textsf{GC}):

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 \textsf{GC} has weakly fair iteration if each guard that is continuously enabled is not indefinitely postponed. For example, if \textsf{GC} 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.

References

• Wikipedia page

@book{dijkstra_1976,
	title = {A {Discipline} of {Programming}},
	isbn = {978-0-13-215871-8},
	publisher = {Prentice-Hall},
	author = {Dijkstra, Edsger W.},
	year = {1976}
}

@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}
}

@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},
}

@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}
}