by Markus Roggenbach, Lutz Schröder and Till Mossakowski
Abstract:
We present a weak theory of the real numbers in the first order specification language CASL. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. Our theory captures for instance e and pi, as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype and specifications of the real numbers in higher order logic and various set theories.
Reference:
Markus Roggenbach, Lutz Schröder and Till Mossakowski: Specifying real numbers in CASL, In Christine Choppy, Didier Bert, eds.: Recent Developments in Algebraic Development Techniques, 14th International Workshop, WADT'99, Lecture Notes in Computer Science, vol. 1827, pp. 146–161, Springer; Berlin; http://www.springer.de, 2000.
Bibtex Entry:
@InProceedings{RoggenbachEA00,
author = {Markus Roggenbach and Lutz Schr{\"o}der and Till Mossakowski},
title = {Specifying real numbers in {CASL}},
year = {2000},
editor = {Christine Choppy and Didier Bert},
booktitle = {Recent Developments in Algebraic Development Techniques, 14th International Workshop, WADT'99},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {1827},
pages = {146--161},
keywords = {real numbers CASL},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1827&spage=146},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/reals.ps.gz},
abstract = { We present a weak theory of the real numbers in the first order specification language CASL. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. Our theory captures for instance e and pi, as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype and specifications of the real numbers in higher order logic and various set theories.
},
isbn = {3-540-67898-0},
}