Computer Science – Logic in Computer Science
Scientific paper
2008-07-10
LMCS 4 (3:6) 2008
Computer Science
Logic in Computer Science
40 pages
Scientific paper
10.2168/LMCS-4(3:6)2008
In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by coinductive streams. The algorithms work on coinductive stream of M\"{o}bius maps and form the basis of the Edalat--Potts exact real arithmetic. We use the machinery of the Coq proof assistant for the coinductive types to present the formalisation. The formalised algorithms are only partially productive, i.e., they do not output provably infinite streams for all possible inputs. We show how to deal with this partiality in the presence of syntactic restrictions posed by the constructive type theory of Coq. Furthermore we show that the type theoretic techniques that we develop are compatible with the semantics of the algorithms as continuous maps on real numbers. The resulting Coq formalisation is available for public download.
No associations
LandOfFree
Coinductive Formal Reasoning in Exact Real Arithmetic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Coinductive Formal Reasoning in Exact Real Arithmetic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Coinductive Formal Reasoning in Exact Real Arithmetic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-459818