Call-time and run-time choice choice

In the semantics of nondeterminism, call-time choice and run-time choice refer to two different conventions about where nondeterministic choice is resolved in a function call.

The notion is somewhat deprecated, given the advent of calculi like call-by-push value, which finely control the evaluation order of effects by distinguishing values from computations.

In their early survey of the semantics of nondeterminism, Søndergaard and Sestoft 1992 introduce the synonymous terms singular vs. plural semantics, which do not seem to have been widely adopted.

Example

A classic example, essentially due to both Hennessy and Ashcroft 1977 and Hussmann 1992 is the double coin example. Letting \oplus signify choice, define

\begin{aligned}
  &&\textsf{double}(x) &\rightarrow x + x \\
  &&\textsf{coin} &\rightarrow 0 \oplus 1
\end{aligned}

If we have call-time choice, then we might observe the following reduction sequences:

\begin{aligned}
  &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{double}(0)
  \rightarrow 0 + 0
  \rightarrow 0 \\
  &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{double}(1)
  \rightarrow 1 + 1
  \rightarrow 2
\end{aligned}

However, if we have run-time choice then we might observe any of the following reduction sequences:

\begin{aligned}
  &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{coin} + \textsf{coin}
  \rightarrow 0 + 0
  \rightarrow 0 \\
  &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{coin} + \textsf{coin}
  \rightarrow 0 + 1
  \rightarrow 1 \\
    &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{coin} + \textsf{coin}
  \rightarrow 1 + 0
  \rightarrow 1 \\
    &\textsf{double}(\textsf{coin})
  \rightarrow \textsf{coin} + \textsf{coin}
  \rightarrow 1 + 1
  \rightarrow 2
\end{aligned}

References

The terminology of call-time-choice was introduced by Hennessy and Ashcroft in a STOC 1977 paper:

Hennessy, M. C.B., and E. A. Ashcroft. 1977. ‘Parameter-Passing Mechanisms and Nondeterminism’. In STOC ’77: Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, 306–11. ACM. https://doi.org/10.1145/800105.803420.

@inproceedings{hennessy_1977,
	title = {Parameter-passing mechanisms and nondeterminism},
	doi = {10.1145/800105.803420},
	booktitle = {{STOC} '77: {Proceedings} of the ninth annual {ACM} {Symposium} on {Theory} of {Computing}},
	publisher = {ACM},
	author = {Hennessy, M. C.B. and Ashcroft, E. A.},
	year = {1977},
	pages = {306--311},
}

The "double coin" example above seems to have first appeared in

Hussmann, Heinrich. 1992. ‘Nondeterministic Algebraic Specifications and Nonconfluent Term Rewriting’. The Journal of Logic Programming 12 (3): 237–55. https://doi.org/10.1016/0743-1066(92)90026-Y.

@article{hussmann_1992,
	title = {Nondeterministic algebraic specifications and nonconfluent term rewriting},
	volume = {12},
	issn = {07431066},
	doi = {10.1016/0743-1066(92)90026-Y},
	number = {3},
	journal = {The Journal of Logic Programming},
	author = {Hussmann, Heinrich},
	year = {1992},
	pages = {237--255},
}

See also

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