Corrigendum: 'On infinite computations in denotational semantics'
J.W. deBakker, João Frederico da Costa Azevedo Meyer, Jeffery I. Zucker · Theoretical Computer Science · 1984
We are indebted to colleagues and students of the University of Utrecht for pointing out to us the following two errors in our paper. (1) The formalism to determine the finite and infinite parts as it is presented fails to work properly with respect to the abort statement A, due to the strictness c;f the semantic functions regarding the s-tate S. Technically this problem can be resolved by deleting this strictness and defining the following: (a) S{CX/K} = 8, i.e., modifications of the S-state yield S itself, (b) ?V( b)(S) =fl, which implies that for instance 9(false)(S) = 0 by Definition 2.4(c). However, we appreciate that one may object that the operational intuition behind this resolution is less clear; one would perhaps expect that a boolean statement (e.g. false) to be performed in S should leave a trace of 6 in the resulting set of states. (2) Lemma 2.3 as it stands is incorrect. In fact, for a chain (7i)i with Ti E 0 we do not necessarily have that its lub exists (take, e.g., Ti E 0 such that _L & ?i and such that UiTi is infinite). What we need as ordering on 0 is the (usual) Egli-Milner ordering E EM defined by r1 +M 72 iff either _L e q and q\(1) c 72 or 1 g 71 and 71 = 72. It is well known (see, e.g., [4]) that 0 is a cpo with respect to !&MM, and