University of Birmingham
4pm Tuesday 26th June 2007
Room 2511, JCMB, King's Buildings
J.R. Marcial-Romero and M. Escardó considered an extension of PCF for real number computation, in which a construct rtest : real ---> bool is used to overcome the undecidability of the relation "r different from 0" [1]. The advantage over previous methods is that the underlying operational semantics is sequential; the drawback is that it is undeterministic: one program may output different results upon different runs. The denotation of a program is hence taken to be a set of values, in a suitable structure. The authors used Hoare powerdomains. While this allows a match between the operational meaning [P] and the denotational meaning [[P]] of a program, i.e. one has [P]=[[P]], such a model doesn't distinguish between total programs that diverge and those that don't, so the denotation is not quite satisfactory to prove total programs correct. It is also shown in [1] that achieving [P]=[[P]] using Smyth powerdomains is impossible. However, we argue that the use of Smyth powerdomains nevertheless allows to define good enough approximations of the operational meaning of programs to prove total ones correct.