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 show how to define integration in Real PCF. We propose two approaches to integration in Real PCF. One consists in adding integration as primitive. The other consists in adding a primitive for maximization of functions and then recursively defining integration from maximization. In both cases we have an 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, which implies that it is also fully abstract.
Original language | English |
---|---|
Title of host publication | Proceedings 11th Annual IEEE Symposium on Logic in Computer Science |
Publisher | IEEE |
Pages | 382-393 |
Number of pages | 12 |
ISBN (Print) | 0818674636 |
DOIs | |
Publication status | Published - 1996 |
Event | Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96 - New Brunswick, NJ, USA Duration: 27 Jul 1996 → 30 Jul 1996 |
Publication series
Name | Proceedings - Symposium on Logic in Computer Science |
---|---|
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
ISSN (Print) | 1043-6871 |
ISSN (Electronic) | 2575-5528 |
Conference
Conference | Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96 |
---|---|
City | New Brunswick, NJ, USA |
Period | 27/07/96 → 30/07/96 |
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.
Keywords
- Differential equations
- Integral equations
- Algebra
ASJC Scopus subject areas
- Software
- General Mathematics