Integration in real PCF

Real PCF is an extension of the programming language PCF with a data type f or real numbers. Although a Real PCF definable real number cannot be comput ed in finitely many steps, it is possible to compute an arbitrarily small r ational interval containing the real number in a sufficiently large number of steps. Based on a domain-theoretic approach to integration, we propose t wo approaches to integration in Real PCF. One consists in adding integratio n as primitive. The other consists in adding a primitive for function maxim ization and then recursively defining integration from maximization. In bot h cases we have a computational adequacy theorem for the corresponding exte nsion of Real PCF, Moreover, based an previous work on Real PCF definabilit y, we show that Real PCF extended with the maximization operator is univers al. (C) 2000 Academic Press.