Abstract
The partial real line is an extension of the Euclidean real line with partial real numbers, which has been used to model exact real number computation in the programming language Real PCF. We introduce induction principles and recursion schemes for the partial unit interval, which allow us to verify that Real PCF programs meet their specification. They resemble the so-called Peano axioms for natural numbers. The theory is based on a domain-equation-like presentation of the partial unit interval. The principles are applied to show that Real PCF is universal in the sense that all computable elements of its universe of discourse are definable. These elements include higher-order functions such as integration operators.
| Original language | English |
|---|---|
| Pages (from-to) | 121-157 |
| Number of pages | 37 |
| Journal | Theoretical Computer Science |
| Volume | 210 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 6 Jan 1999 |
Bibliographical note
Funding Information:The first named author was supported by the Brazilian agency CNPq, an EPSRC project “Programming Languages for Real Number Computation: Theory and Implementation”, and an ARC project “A Computational Approach to Measure and Integration Theory”.
Keywords
- Coinduction
- Domain theory
- Exact real number computation
- Induction
- Real PCF
- Universality
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science