Milad Niqui - Coinductive Formal Reasoning in Exact Real Arithmetic

lmcs:953 - Logical Methods in Computer Science, September 10, 2008, Volume 4, Issue 3 -
Coinductive Formal Reasoning in Exact Real Arithmetic

Authors: Milad Niqui

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ö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.

Volume: Volume 4, Issue 3
Published on: September 10, 2008
Accepted on: June 25, 2015
Submitted on: June 11, 2007
Keywords: Computer Science - Logic in Computer Science,F.3.1,D.2.4


Consultation statistics

This page has been seen 233 times.
This article's PDF has been downloaded 272 times.