Integration in real PCF

Abbas Edalat; Martin Hotzel Escardo

doi:10.1109/LICS.1996.561453

Integration in real PCF

Abbas Edalat^*, Martin Hotzel Escardo

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	https://doi.org/10.1109/LICS.1996.561453
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

Access to Document

10.1109/LICS.1996.561453

Cite this

@inproceedings{d964490152c04a559fb5779cbb98185a,

title = "Integration in real PCF",

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.",

keywords = "Differential equations, Integral equations, Algebra",

author = "Abbas Edalat and Escardo, {Martin Hotzel}",

note = "Funding Information: This work has been supported by EPSRC projects {\textquoteleft}{\textquoteleft}Constructive Approximation Using Domain Theory,{\textquoteright}{\textquoteright} {\textquoteleft}{\textquoteleft}Foundational Structures in Computer Science,{\textquoteright}{\textquoteright} and {\textquoteleft}{\textquoteleft}Programming Languages for Real Number Computation: Theory and Implementation,{\textquoteright}{\textquoteright} and by ARC Project {\textquoteleft}{\textquoteleft}A Computational Approach to Measure and Integration Theory.{\textquoteright}{\textquoteright} The second author has also been supported by the Brazilian agency CNPq.; Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96 ; Conference date: 27-07-1996 Through 30-07-1996",

year = "1996",

doi = "10.1109/LICS.1996.561453",

language = "English",

isbn = "0818674636",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "382--393",

booktitle = "Proceedings 11th Annual IEEE Symposium on Logic in Computer Science",

}

TY - GEN

T1 - Integration in real PCF

AU - Edalat, Abbas

AU - Escardo, Martin Hotzel

N1 - 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.

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

KW - Differential equations

KW - Integral equations

KW - Algebra

UR - http://www.scopus.com/inward/record.url?scp=0029714149&partnerID=8YFLogxK

U2 - 10.1109/LICS.1996.561453

DO - 10.1109/LICS.1996.561453

M3 - Conference contribution

AN - SCOPUS:0029714149

SN - 0818674636

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 382

EP - 393

BT - Proceedings 11th Annual IEEE Symposium on Logic in Computer Science

PB - IEEE

T2 - Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96

Y2 - 27 July 1996 through 30 July 1996

ER -

Integration in real PCF

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this