Real PCF

PCF is a paradigmatic functional programming language used for theoretical investigations [51] in programming-language semantics. It has operational and denotational semantics connected by an adequacy property [44]. Several extensions of PCF with data types for real numbers have been discussed in the literature [19,25,47], and practical versions of these theoretical languages have been implemented by Edalat's group at Imperial College.

The idea is that one starts from a ground type R for real numbers, in addition to the usual ground types N and B for natural numbers and booleans, and that new types are obtained by iterating a function space construction. Thus, the types include

1.

functions of real numbers, 105#105,

2.

predicates defined on real numbers, 106#106,

3.

sequences of real numbers, 107#107,

4.

sequences of sequences of real numbers, 108#108,

5.

sequences of functions, 109#109,

6.

functionals mapping sequences to numbers (such as limit operators), 110#110,

7.

functionals mapping functions to numbers (such as definite integration and supremum operators and distributions), 111#111,

8.

functionals mapping predicates to truth-values (such as quantification operators), 112#112.

and so on. The syntactic framework is a simply typed lambda calculus with recursion [4]--in practice, this means that PCF is a functional programming language such as Haskell or ML [6,43], limited to the bare minimum level of sophistication, in order to simplify the theoretical investigations. The semantic framework is domain theory, already mentioned above, and one uses an interval domain proposed by Dana Scott as the interpretation of real numbers. The idea is that singletons give complete information or ``total real numbers'' and that other intervals give incomplete information or ``partial real numbers''. This is related to interval analysis, of course. But a term of the language denoting the number 113#113 doesn't produce a floating-point interval approximation of 113#113 under the operational semantics; rather, it produces better and better approximations of this value. In practice, this can be a signed-digit binary expansion of 113#113, for example, and, for theoretical purposes, this is taken as a shrinking sequence of rational intervals whose intersection is the singleton interval  114#114.