Interpretations of recursion under unbounded nondeterminacy (Q1115173)

This well written article concerns the semantics of language that contains unbounded nondeterminacy. Although already many papers have been written on this issue, the author succeeds in treating the subject from an original and interesting perspective. He does so by giving a denotational semantics without the standard tools of cpos or limits, thus circumventing the usual problems in the denotational semantics of unbounded nondeterminism. Instead, he bases both his operational and denotational semantics on an axiomatically defined notion of interpretation, using elementary mathematical means. Next, the well known notions of weakest (liberal) preconditions are characterized as smallest (largest) preparator functions, which are a kind of objects dual to interpretations. Finally, a characterization is given of the spectrum of interpretations which cannot deliver unjustified meaningful values upon divergence. Again, corresponding preparator functions are determined.