Countable nondeterminism and random assignment

Abstract

Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.