A cook’s tour of countable nondeterminism

Abstract

We provide four semantics for a small programming language involving unbounded (but countable) nondeterminism. These comprise an operational one, two denotational ones based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. We also introduce a Hoare-like proof system for total correctness and show its soundness and completeness in an appropriate sense. Admission of countable nondeterminism results in a lack of continuity of various semantic functions; moreover some of the partial orders considered are in general not cpo's and in proofs of total correctness one has to resort to the use of (countable) ordinals. Proofs will appear in the full version of the paper.