The ambiguous choice operator amb was introduced by John McCarthy in [McCarthy 1963]. It is presented as a binary (or sometimes -ary) operator , which implements angelic nondeterministic choice.
Operationally, means "evaluate and 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
(where is a nonterminating program) must always resolve to . It is sometimes said that is bottom-avoiding.
As another example, the following program by McCarthy [1963] nondeterministically computes any natural number less than :
If we assume that is a nonterminating program , for this expands into . However, that is not a problem: the angelicity of means that it will preferentially return defined arguments, and will thus return either or .
amb is a particularly powerful programming construct.
[Lassen and Moran 1999] report that it can be used to implement any of
Moreover, when combined with general recursion, it can be used to implement countable nondeterminism.
Erratic choice can be implemented as
where as usual and .
This corresponds to erratic choice exactly because all terms of the form converge (to ), so the angelic choice is free to resolve it to either term, which is then 'unthunked.'
Countable nondeterminism, often denoted by , can be implemented recursively by
The value of will then be an arbitrary natural number.
This implements countable nondeterminism exactly because minimizes nontermination, it will not continue recursively unfolding forever.
There is a subtle question about amb: is the choice it makes the "best" locally or globally?
Suppose that we define
Then:
Thus, the "original" makes a "best" choice for the arguments it encloses.
There is an alternative description of , which is globally angelic. In that version, 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
is also satisfied.
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.
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 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.
[Carayol, Hirschkoff, and Sangiorgi 2005] show how to encode in the -calculus through a Milner encoding.
That paper also contains a wealth of interesting references.
McCarthy, John. 1963. ‘A Basis for a Mathematical Theory of Computation’. In Computer Proramming and Formal Systems, edited by P. Braffort and D. Hirschberg, 35:33–70. Studies in Logic and the Foundations of Mathematics. Elsevier. https://doi.org/10.1016/S0049-237X(08)72018-4. [pdf]
@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}
}
Clinger, William, and Charles Halpern. 1985. ‘Alternative Semantics for McCarthy’s Amb’. In Seminar on Concurrency, edited by Stephen D. Brookes, Andrew William Roscoe, and Glynn Winskel, 197:467–78. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-15670-4_22.
@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}
}
Broy, Manfred. 1986. ‘A Theory for Nondeterminism, Parallelism, Communication, and Concurrency’. Theoretical Computer Science 45: 1–61. https://doi.org/10.1016/0304-3975(86)90040-X.
@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}
}
Lassen, Søren B., and Andrew Moran. 1999. ‘Unique Fixed Point Induction for McCarthy’s Amb’. In Mathematical Foundations of Computer Science 1999, edited by Mirosław Kutyłowski, Leszek Pacholski, and Tomasz Wierzbicki, 1672:198–208. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48340-3_18.
@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}
}
Carayol, Arnaud, Daniel Hirschkoff, and Davide Sangiorgi. 2005. ‘On the Representation of McCarthy’s Amb in the π-Calculus’. Theoretical Computer Science 330 (3): 439–73. https://doi.org/10.1016/j.tcs.2004.10.005.
@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}
}
Levy, Paul Blain. 2007. ‘Amb Breaks Well-Pointedness, Ground Amb Doesn’t’. Electronic Notes in Theoretical Computer Science 173: 221–39. https://doi.org/10.1016/j.entcs.2007.02.036.
@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}
}
Lassen, Soren B, Paul Blain Levy, and Prakash Panangaden. 2005. ‘Divergence-Least Semantics Of Amb Is Hoare’. Short presentation at the 3rd APPSEM II workshop. https://www.cs.bham.ac.uk/~pbl/papers/ambdivleast.pdf.
@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}
}