Operational semantics of Real PCF

The paper [25] contains a development of an operational semantics for PCF extended with real numbers (referred to as Real PCF) and a proof of its computational adequacy, which states that the operational semantics produces a convergent sequence of better and better approximations to the mathematical value of a program. The main idea for developing an operational semantics is the observation that the prefix order of the monoid of increasing affine endomaps of the unit interval is isomorphic to the information (=reverse inclusion) order of the interval domain. Moreover, under the isomorphism, infinitely iterated concatenations in this monoid correspond to joins in the domain. Thus, computations are operationally implemented as infinitely iterated compositions of rational affine maps. These infinitely iterated compositions can be regarded as multi-base expansions allowing not only negative but also rational digits.

In the paper [47] it is proposed to work with the larger monoid of Möbius transformations. This is possible because the information refinement property still holds. Again, a computationally adequate operational semantics is obtained. Advantages of generalizing affine maps to Möbius transformations include the fact that the basic transcendental functions can be elegantly implemented in this framework via the theory of continued fractions, as Edalat and Potts have shown [24].