Coinductive Field of Exact Real Numbers and General Corecursion |
| |
Authors: | Milad Niqui |
| |
Affiliation: | aInstitute for Computing and Information Sciences, Faculty of Science, Radboud University Nijmegen, Toernooiveld 1, 6525 ED, Nijmegen, The Netherlands |
| |
Abstract: | In this article we present a method to define algebraic structure (field operations) on a representation of real numbers by coinductive streams. The field operations will be given in two algorithms (homographic and quadratic algorithm) that operate on streams of Möbius maps. The algorithms can be seen as coalgebra maps on the coalgebra of streams and hence they will be formalised as general corecursive functions. We use the machinery of Coq proof assistant for coinductive types to present the formalisation. |
| |
Keywords: | Coinductive types exact real arithmetic general corecursion |
本文献已被 ScienceDirect 等数据库收录! |
|