Abstract
We present a weak theory BasicReal 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. BasicReal captures for instance e and π, 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 BasicReal and specifications of the real numbers in higher order logic and various set theories.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible byWWW2 and FTP3. 146, http://www.brics.dk/Projects/CoFI
CoFI Language Design Task Group. Casl – The CoFI Algebraic Specification Language – Summary, version 1.0. Documents/CASLSummary, in [CoF] (July 1999)
Gödel, K.: The Consistency of the Continuum Hypothesis. Annals of Math. Studies, vol. 3. Princeton University Press, Princeton (1940)
Harrison, J.R.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)
Kulisch, U.W., Miranker, W.L.: Computer Arithmetic in Theory and Practice. Academic Press, London (1981)
Lang, S.: Algebra, 2nd edn. Addison-Wesley, Reading (1984)
Mossakowski, T., Haxthausen, A., Krieg-Brückner, B.: Subsorted partial higher-order logic as an extension of CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 126–145. Springer, Heidelberg (2000)
Mossakowski, T., Kolyang, Krieg-Brückner, B.: Static semantic analysis and theorem proving for CASL. In: Parisi Presicce, F. (ed.) Recent trends in algebraic development techniques. Proc. 12th International Workshop. LNCS, vol. 1376, pp. 333–348. Springer, Heidelberg (1998)
Moore, R.E. (ed.): Reliability in Computing, The Role of Interval Methods in Scientific Computations. Academic Press, London (1988)
Roggenbach, M., Schröder, L., Mossakowski, T.: The datatypes REAL and COMPLEX in Casl. Note M-7, version 0.3, in [CoF] (2000)
Roggenbach, M., Mossakowski, T., Schröder, L.: Basic Datatypes in Casl. Note L-12, version 0.4, in [CoF] (March 2000)
Roggenbach, M., Mossakowski, T.: Rules of Methodology. Note M-6, version 0.3, in [CoF] (2000)
Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 42, 230–265 (1936/1937)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roggenbach, M., Schröder, L., Mossakowski, T. (2000). Specifying Real Numbers in CASL . In: Bert, D., Choppy, C., Mosses, P.D. (eds) Recent Trends in Algebraic Development Techniques. WADT 1999. Lecture Notes in Computer Science, vol 1827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-44616-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-44616-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67898-4
Online ISBN: 978-3-540-44616-3
eBook Packages: Springer Book Archive