Semantics of Unbounded Nondeterminism

摘要

A program construct is proposed, for which the assumption of bounded nondeterminism is not natural. It is shown that the simple approach of taking the power domain of the flat cpo does not produce a correct semantics for programs in which nondeterminism is unbounded. The power domain approach is then extended to computation paths, resulting in an essentially operational semantics for programs of unbounded nondeterminism.