Logic in Computer Science (LICS 1996)

Paper: Integration in Real PCF (at LICS 1996)

Authors: Abbas Edalat Martin Hötzel Escardo

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.

BibTeX

  @InProceedings{Escardo-IntegrationinRealPC,
    author = 	 {Abbas Edalat and Martin Hötzel Escardo},
    title = 	 {Integration in Real PCF},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {382-393},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }