Amb

The ambiguous choice operator amb was introduced by John McCarthy in McCarthy 1963. It is presented as a binary (or sometimes n-ary) operator \textsf{amb}(M, N), which implements angelic nondeterministic choice.

Operationally, \textsf{amb}(M, N) means "evaluate M and N on an arbitrary fair scheduler, and return whatever answer you get first" Lassen et al. 2005.

Thus, the angelicity of the nondeterministic choice essentially helps avoid nontermination. For example, the expression

\textsf{amb}(\lambda x. x, \Omega)

(where \Omega is a nonterminating program) must always resolve to \lambda x. x. It is sometimes said that \textbf{amb} is bottom-avoiding.

As another example, the following program by McCarthy 1963 nondeterministically computes any natural number less than n:

\textsf{less}(n) = \textsf{amb}(n - 1, \textsf{less}(n- 1))

If we assume that 0 - 1 is a nonterminating program \bot, for n = 2 this expands into \textsf{amb}(1, \textsf{amb}(0, \bot)). However, that is not a problem: the angelicity of \textsf{amb} means that it will preferentially return defined arguments, and will thus return either 0 or 1.

Expressivity of amb

amb is a particularly powerful programming construct.

Lassen and Moran 1999 report that it can be used to implement any of

• Erratic choice
• Parallel or

Moreover, when combined with general recursion, it can be used to implement countable nondeterminism.

Erratic choice

Erratic choice \oplus can be implemented as

M \oplus N = \textsf{amb}(\textsf{K} M, \textsf{K} N) \textsf{I}

where as usual \textbf{K} = \lambda x. \lambda y. x and \textbf{I} = \lambda x. x.

This corresponds to erratic choice exactly because all terms of the form \textbf{K} X converge (to \lambda y. X), so the angelic choice is free to resolve it to either term, which is then 'unthunked.'

Countable nondeterminism

Countable nondeterminism, often denoted by ?, can be implemented recursively by

? = \textsf{amb}(0, ? + 1)

The value of ? will then be an arbitrary natural number.

This implements countable nondeterminism exactly because \textsf{amb} minimizes nontermination, it will not continue recursively unfolding forever.

Local or global?

There is a subtle question about amb: is the choice it makes the "best" locally or globally?

Suppose that we define

f(x) = \begin{cases}
  0     & \text{if $x = 0$} \\
  \bot  & \text{otherwise}
\end{cases}

Then:

• \textsf{amb}(f(0), f(1)) always terminates, returning 0.
• f(\textsf{amb}(0, 1)) may either return 0, or it may diverge.

Thus, the "original" \textsf{amb} makes a "best" choice for the arguments it encloses.

There is an alternative description of \textsf{amb}, which is globally angelic. In that version, \textsf{amb} makes the best possible choice for the convergence of the entire program that is being run. This is presented by Clinger and Halpern 1985, who also show that in that case the equation

\textsf{amb}(f(x), f(y)) = f(\textsf{amb}(x, y))

is also satisfied.

Denotational semantics

It is difficult to formulate a domain-theoretic semantics that can capture the nondeterminism of amb.

The natural place to look would be in powerdomains.

• Lassen and Moran 1999 report that amb is not monotonic with respect to the Egli-Milner order, so it cannot be directly modelled in the Plotkin powerdomain or its variants.
• Lassen et al. 2005 argue that \textsf{amb} is strongly connected to the Hoare powerdomain, which is the only one that can model it.

There is a domain-theoretic semantics for amb in a first-order language, due to Broy 1986.

Paul Levy MFPS 2007 showed that there cannot be a denotational semantics of amb that is well-pointed. The argument works only for typed calculi, and if we are able to apply amb at higher types.

In dataflow networks

In Kahn process networks, the amb operator has a slightly different meaning. It a process with two input channels and one output channel. The output sequence is one of the two input sequences, whichever
is non-empty - if any.

See the main article on fair merge for more information.

In the \pi-calculus

Carayol, Hirschkoff, and Sangiorgi 2005 show how to encode \textbf{amb} in the \pi-calculus through a Milner encoding.

That paper also contains a wealth of interesting references.

See also

• Nondeterminism
• Angelic nondeterminism
• Demonic nondeterminism
• Fair merge

References

@incollection{mccarthy_basis_1963,
	series = {Studies in {Logic} and the {Foundations} of {Mathematics}},
	title = {A {Basis} for a {Mathematical} {Theory} of {Computation}},
	volume = {35},
	booktitle = {Computer {Proramming} and {Formal} {Systems}},
	publisher = {Elsevier},
	author = {McCarthy, John},
	editor = {Braffort, P. and Hirschberg, D.},
	year = {1963},
	doi = {10.1016/S0049-237X(08)72018-4},
	pages = {33--70}
}

@inproceedings{brookes_alternative_1985,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Alternative semantics for {McCarthy}'s amb},
	volume = {197},
	doi = {10.1007/3-540-15670-4_22},
	booktitle = {Seminar on {Concurrency}},
	publisher = {Springer Berlin Heidelberg},
	author = {Clinger, William and Halpern, Charles},
	editor = {Brookes, Stephen D. and Roscoe, Andrew William and Winskel, Glynn},
	year = {1985},
	pages = {467--478}
}

@article{broy_1986,
	title = {A theory for nondeterminism, parallelism, communication, and concurrency},
	volume = {45},
	doi = {10.1016/0304-3975(86)90040-X},
	journal = {Theoretical Computer Science},
	author = {Broy, Manfred},
	year = {1986},
	pages = {1--61}
}

@inproceedings{lassen_1999,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Unique {Fixed} {Point} {Induction} for {McCarthy}’s {Amb}},
	volume = {1672},
	doi = {10.1007/3-540-48340-3_18},
	booktitle = {Mathematical {Foundations} of {Computer} {Science} 1999},
	publisher = {Springer Berlin Heidelberg},
	author = {Lassen, S{\o}ren B. and Moran, Andrew},
	editor = {Kuty{\l}owski, Miros{\l}aw and Pacholski, Leszek and Wierzbicki, Tomasz},
	year = {1999},
	pages = {198--208}
}

@article{carayol_2005,
	title = {On the representation of {McCarthy}'s amb in the π-calculus},
	volume = {330},
	doi = {10.1016/j.tcs.2004.10.005},
	number = {3},
	journal = {Theoretical Computer Science},
	author = {Carayol, Arnaud and Hirschkoff, Daniel and Sangiorgi, Davide},
	year = {2005},
	pages = {439--473}
}

@article{levy_amb_2007,
	title = {Amb {Breaks} {Well}-{Pointedness}, {Ground} {Amb} {Doesn}'t},
	volume = {173},
	url = {https://www.cs.bham.ac.uk/~pbl/papers/ambhowenew.pdf},
	doi = {10.1016/j.entcs.2007.02.036},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {Levy, Paul Blain},
	year = {2007},
	pages = {221--239}
}

• For an argument that the only divergence-least semantics of \textsf{amb} is related to the Hoare powerdomain see

@misc{lassen_2005,
	type = {Short presentation at the 3rd {APPSEM} {II} workshop},
	title = {Divergence-{Least} {Semantics} {Of} amb {Is} {Hoare}},
	url = {https://www.cs.bham.ac.uk/~pbl/papers/ambdivleast.pdf},
	author = {Lassen, Søren B and Levy, Paul Blain and Panangaden, Prakash},
	year = {2005}
}