Jump to content

Angelic non-determinism

From Wikipedia, the free encyclopedia

This is the current revision of this page, as edited by 76.114.60.123 (talk) at 21:50, 11 April 2022 (Expand from just halting analysis to any nondet algorithm needed for a proof.). The present address (URL) is a permanent link to this version.

(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

In computer science, angelic non-determinism is the execution of a nondeterministic algorithm where particular choices are declared to always favor a desired result, if that result is possible.

For example, in halting analysis of a Nondeterministic Turing machine, the choices would always favor termination of the program.

The "angelic" terminology comes from the Christian religious conventions of angels being benevolent and acting on behalf of an omniscient God.

References

[edit]

Wirsing, M.; Broy, M. (5 March 1981). "On the algebraic specification of nondeterministic programming languages". Caap '81. Lecture Notes in Computer Science. 112. Springer, Berlin, Heidelberg: 162–179. doi:10.1007/3-540-10828-9_61. ISBN 978-3-540-10828-3.

Bodik, Rastislav; Chandra, Satish; Galenson, Joel; Kimelman, Doug; Tung, Nicholas; Barman, Shaon; Rodarmor, Casey (2010). "Programming with Angelic Nondeterminism". SIGPLAN Notices. 45 (1): 339–352. doi:10.1145/1707801.1706339. ISSN 0362-1340.