Denotational semantics for unguarded recursion: the demonic case
Arie de Bruin, E.P. de Vink · 1990
We show that the technique to prove equivalence of operational and denotational cpo based semantics using retractions, as introduced in [BV] for a sequential backtracking language, can be applied to parallel languages as well. We prove equivalence for a uniform language in which procedure calls need not be guarded. The unguardedness is taken care of by giving a semantics in which the nondeterminism is demonic. Section 1 Introduction In [BV]a we have introduced a new idea of proving equivalence of an operational semantics, say O, and a denotational semantics, say D, where both semantics are based on cpo's. The idea is to introduce less abstract variants O and D of the semantical definitions for which the equivalence O = D is easier to establish. The latter proof will be less complicated if O and D can be defined in such a way that for each statement they deliver maximal elements in the cpo of meanings of statements. The equivalence O = D can then be established by sho...