Contribution: CoinductiveReals

Real numbers as coinductive ternary streams

Authors

Description

See the README file

Keywords

real numbers, co inductive types, co recursion, exact arithmetic

README

DESCRIPTION

This contribution contains a formalisation of algebraic operations on
coinductive streams representing real numbers in the interval [-1,1].
This includes:

 * A ternary representation for real numbers in [-1,1] using the type
   [Reals] (see digits.v).
 * Proof that this is a representation for real numbers using the real
   numbers of the standard library (see Cauchy_stream.v).
 * Implementation of the homographic algorithm using a general
   corecursion technique explained in [1] (see homographic.v).
 * Implementation of the quadratic algorithm using a general
   corecursion technique explained in [1] (see quadratic.v).
 * A coinductive proof of correctness of the algorithms as explained
   in [2] (see hcorrectness.v and qcorrectness.v).
 * A metric proof of the correctness of the algorithms (see
   productivity_M.v and productivity_T.v). These are the formalisation
   of the proofs in Chapter 5 of [3].

USAGE

 The files should be compiled using Coq version 8.1 or higher. They
 also need the rational numbers of QArithSternBrocot package which
 could be downloaded from:

  http://coq.inria.fr/contribs/QArithSternBrocot.tar.gz
 
 or from svn archive in the subdirectory Nijmegen/QArithSternBrocot.

 First compile the QArithSternBrocot package and make sure it is in
 the load path for your coqc command.

 Then you can compile this contribution using the provided
 Makefile. In order to compile the files do the following:

$ touch .depend
$ make depend
$ make

REFERENCES 

[1] Milad Niqui; `Coinductive Field of Exact Real Numbers and General
    Corecursion', In N. Ghani and J. Power (Eds.), Proceedings of 8th
    Workshop on Coalgebraic Methods in Computer Science (CMCS 2006),
    Vienna, Austria 25-27 March 2006, ENTCS 164.1.
    http://www.cs.ru.nl/~milad/publications/CMCS06.html

[2] Milad Niqui; `Coinductive Correctness of Homographic and Quadratic
    Algorithms for Exact Real Numbers', To appear in the LNCS
    Proceedings of TYPES 2006 Workshop.
    http://www.cs.ru.nl/~milad/publications/TYPES06.html

[3] Milad Niqui; PhD Thesis; Formalising Exact Arithmetic:
    Representations, Algorithms and Proofs, Radboud University
    Nijmegen, September 2004, ISBN 90-9018333-7.
    http://www.cs.ru.nl/~milad/proefschrift/

AUTHOR

 Milad Niqui (Radboud University Nijmegen) <milad@cs.ru.nl>

LICENSE

 LGPL (GNU Lesser General Public License Version 2.1)
 A copy of this license is distributed in this package in the file
 LICENSE.

DATE

 24-04-2007

Available files