Extraction of Programs for Exact Real Number Computation Using Agda
Chi Ming Chuang · 2011
This thesis contains the to our knowledge first research project to extract in the theorem prover Agda programs from proofs involving postulated axioms. Our method doesn’t require to write a Meta program for extracting programs from proofs. It shows as well the correctness of the machinery. This method has been applied to the extraction of programs about real number computation. The method has been used for showing that the signed digit approximable real numbers are closed under addition, multiplication, and contain the rational numbers. Therefore we obtain in Agda a provably correct program which executes the corresponding operations on signed digit streams. The first part of the thesis introduces axioms about real numbers using postulated data types and functions in Agda without giving any computational rules. Then we investigate some properties of real numbers constructed by Cauchy sequences: we introduce the set of