Abstract
Real PCF is an extension of the programming language PCF with a data type for real numbers. Although a Real PCF definable real number cannot be computed in finitely many steps, it is possible to compute an arbitrarily small rational interval containing the real number in a sufficiently large number of steps. Based on a domain-theoretic approach to integration, we propose two approaches to integration in Real PCF. One consists in adding integration as primitive. The other consists in adding a primitive for function maximization and then recursively defining integration from maximization. In both cases we have a computational adequacy theorem for the corresponding extension of Real PCF. Moreover, based on previous work on Real PCF definability, we show that Real PCF extended with the maximization operator is universal.
| Original language | English |
|---|---|
| Pages (from-to) | 128-166 |
| Number of pages | 39 |
| Journal | Information and Computation |
| Volume | 160 |
| Issue number | 1-2 |
| DOIs | |
| Publication status | Published - 10 Jul 2000 |
Bibliographical note
Funding Information:This work has been supported by EPSRC projects ‘‘Constructive Approximation Using Domain Theory,’’ ‘‘Foundational Structures in Computer Science,’’ and ‘‘Programming Languages for Real Number Computation: Theory and Implementation,’’ and by ARC Project ‘‘A Computational Approach to Measure and Integration Theory.’’ The second author has also been supported by the Brazilian agency CNPq.
ASJC Scopus subject areas
- Theoretical Computer Science
- Information Systems
- Computer Science Applications
- Computational Theory and Mathematics