Angels and demons

A subject the papers are about. The loosest grouping, and the one to reach for last.

Two nondeterminisms in one program: the demon resolves a choice against you and the angel in your favour, so a specification's freedom and an adversary's turn out to be one construct with opposite polarity.

Floyd is the ancestor and the set was starting mid-argument without him. *Nondeterministic Algorithms*, 1967, proposes choice as a programming construct with the successful path selected -- which is the angelic reading, before it had a name or a dual. Everything after formalises the polarity and asks what it costs.

Back and von Wright combine the two in a refinement calculus; McIver and Morgan work out demonic choice against probability, where the demon is an adversary and the distinction stops being a matter of taste; Martin, Barman and Mamouras take it to modelling, programming and synthesis. Demri is the odd member and the one that shows the construct is not confined to program semantics.

The set's claim is worth stating carefully because it is easy to hear as wordplay. Angelic and demonic nondeterminism are the same syntactic construct read under opposite quantifiers -- there exists a resolution, for all resolutions. That is why a specification's underdetermination and an adversary's freedom are formally the same thing, and why a calculus that handles one gets the other by duality rather than by a separate theory.

Floyd 1967 is linked `distinct-from` floyd1967assigning, the other Floyd paper of that year, which the corpus holds in `relatively-complete`.