Abstract
In this work we focus on a formalisation of the algorithms of lazy exact arithmetic á la Potts and Edalat [1]. We choose the constructive type theory as our formal verification tool. We discuss an extension of the constructive type theory with coinductive types that enables one to formalise and reason about the infinite objects. We show examples of how infinite objects such as streams and expression trees can be formalised as coinductive types. We study the type theoretic notion of productivity which ensures the infiniteness of the outcome of the algorithms on infinite objects. Syntactical methods are not always strong enough to ensure the productivity. However, if some information about the complexity of a function is provided, one may be able to show the productivity of that function. In the case of the normalisation algorithm we show that such information can be obtained from the choice of real number representation that is used to represent the input and the output.
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
Potts, P.J., Edalat, A.: Exact real computer arithmetic. Technical Report DOC 97/9, Department of Computing, Imperial College (1997)
Edalat, A., Potts, P.J., Sünderhauf, P.: Lazy computation with exact real numbers. In: Berman, M., Berman, S. (eds.) Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), Baltimore, Maryland, USA, September 27-29, 1998. ACM SIGPLAN Notices, vol. 34(1), pp. 185–194. ACM Press, New York (1999)
Niqui, M.: Formalising Exact Arithmetic: Representations, Algorithms and Proofs. PhD thesis, Radboud Universiteit Nijmegen (2004)
Giménez, E.: Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communicants. PhD thesis PhD 96-11, Laboratoire de l’Informatique du Parallélisme, Ecole Normale Supérieure de Lyon (1996)
The Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.0. INRIA (2004), http://coq.inria.fr/doc/main.html , (cited 31st January 2005)
Hagino, T.: A Categorical Programming Language. PhD thesis CST-47-87, Laboratory for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh (1987)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier Science Publishers, Amsterdam (1998)
Martin-Löf, P.: Intuitionistic Type Theory, Biblioplois, Napoli. Notes of Giovanni Sambin on a series of lectures given in Padova (1984)
Coquand, T., Paulin, C.: Inductively defined types (preliminary version). In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)
Potts, P.J.: Exact Real Arithmetic using Möbius Transformations. PhD thesis, University of London, Imperial College (1998)
Saïbi, A.: Typing algorithm in type theory with inheritance. In: POPL 1997: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM SIGACT and SIGPLAN, pp. 292–301. ACM Press, New York (1997)
Sijtsma, B.A.: On the productivity of recursive list definitions. ACM Trans. Program. Lang. Syst (TOPLAS) 11, 633–649 (1989)
Weihrauch, K.: Computable Analysis. An introduction, p. 285. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niqui, M. (2005). Formalising Exact Arithmetic in Type Theory. In: Cooper, S.B., Löwe, B., Torenvliet, L. (eds) New Computational Paradigms. CiE 2005. Lecture Notes in Computer Science, vol 3526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11494645_46
Download citation
DOI: https://doi.org/10.1007/11494645_46
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26179-7
Online ISBN: 978-3-540-32266-5
eBook Packages: Computer ScienceComputer Science (R0)