No Cover Image

E-Thesis 20584 views 171 downloads

Extraction of programs for exact number computation using Agda. / Chi Ming Chuang

Swansea University Author: Chi Ming Chuang

Abstract

This thesis contains the to our knowledge first research project to ex-tract in the theorem prover Agda programs from proofs involving pos-tulated 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. T...

Full description

Published: 2011
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
URI: https://cronfa.swan.ac.uk/Record/cronfa42274
first_indexed 2018-08-02T18:54:18Z
last_indexed 2018-08-03T10:09:43Z
id cronfa42274
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-08-02T16:24:28.6513889</datestamp><bib-version>v2</bib-version><id>42274</id><entry>2018-08-02</entry><title>Extraction of programs for exact number computation using Agda.</title><swanseaauthors><author><sid>f2d226665fc9a278c0f31a914e196a7e</sid><ORCID>NULL</ORCID><firstname>Chi Ming</firstname><surname>Chuang</surname><name>Chi Ming Chuang</name><active>true</active><ethesisStudent>true</ethesisStudent></author></swanseaauthors><date>2018-08-02</date><abstract>This thesis contains the to our knowledge first research project to ex-tract in the theorem prover Agda programs from proofs involving pos-tulated 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 real numbers which are limits of Cauchy sequences of rational numbers (Cauchy Reals) and show that they are closed under addition and multiplication. We also prove that Cauchy Reals are Cauchy complete. Furthermore, we introduce the real numbers in the interval [-1,1], which have a binary signed digit representation, i.e. r = 0.d0d1d2..., where di &amp;isin; {lcub}-1, 0, 1{rcub}. This set of real numbers is given as a codata type (SDR). We determine for rational numbers in the interval [-1, 1] their SDR and show that SDRs are closed under the average function and the multiplication function. Besides, a finding digit function is defined which determines the first n digits of a stream of signed digits. In the second part of the thesis, a theorem is given which shows the correctness of our method. It shows that under certain conditions our method always normalises and doesn't make use of the axioms. The conditions mainly guarantee that a postulated function or axiom has as result type only a postulated type, so the reduction of elements of algebraic data types to head normal form will not refer to these postulates. Because of our theorem the finding digit function applied to a real number r s.t. SDR r holds normalises to [do, d1,..., dn-1] for the first n digit d0d1...dn-1 of r. Therefore, we can compute the SDR of rational numbers and from SDRs of real numbers the SDR of their average and product.</abstract><type>E-Thesis</type><journal/><journalNumber></journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><issnPrint/><issnElectronic/><keywords>Computer science.</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2011</publishedYear><publishedDate>2011-12-31</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2018-08-02T16:24:28.6513889</lastEdited><Created>2018-08-02T16:24:28.6513889</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Chi Ming</firstname><surname>Chuang</surname><orcid>NULL</orcid><order>1</order></author></authors><documents><document><filename>0042274-02082018162441.pdf</filename><originalFilename>10797982.pdf</originalFilename><uploaded>2018-08-02T16:24:41.5670000</uploaded><type>Output</type><contentLength>5693808</contentLength><contentType>application/pdf</contentType><version>E-Thesis</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-02T16:24:41.5670000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2018-08-02T16:24:28.6513889 v2 42274 2018-08-02 Extraction of programs for exact number computation using Agda. f2d226665fc9a278c0f31a914e196a7e NULL Chi Ming Chuang Chi Ming Chuang true true 2018-08-02 This thesis contains the to our knowledge first research project to ex-tract in the theorem prover Agda programs from proofs involving pos-tulated 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 real numbers which are limits of Cauchy sequences of rational numbers (Cauchy Reals) and show that they are closed under addition and multiplication. We also prove that Cauchy Reals are Cauchy complete. Furthermore, we introduce the real numbers in the interval [-1,1], which have a binary signed digit representation, i.e. r = 0.d0d1d2..., where di &isin; {lcub}-1, 0, 1{rcub}. This set of real numbers is given as a codata type (SDR). We determine for rational numbers in the interval [-1, 1] their SDR and show that SDRs are closed under the average function and the multiplication function. Besides, a finding digit function is defined which determines the first n digits of a stream of signed digits. In the second part of the thesis, a theorem is given which shows the correctness of our method. It shows that under certain conditions our method always normalises and doesn't make use of the axioms. The conditions mainly guarantee that a postulated function or axiom has as result type only a postulated type, so the reduction of elements of algebraic data types to head normal form will not refer to these postulates. Because of our theorem the finding digit function applied to a real number r s.t. SDR r holds normalises to [do, d1,..., dn-1] for the first n digit d0d1...dn-1 of r. Therefore, we can compute the SDR of rational numbers and from SDRs of real numbers the SDR of their average and product. E-Thesis Computer science. 31 12 2011 2011-12-31 COLLEGE NANME Computer Science COLLEGE CODE Swansea University Doctoral Ph.D 2018-08-02T16:24:28.6513889 2018-08-02T16:24:28.6513889 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Chi Ming Chuang NULL 1 0042274-02082018162441.pdf 10797982.pdf 2018-08-02T16:24:41.5670000 Output 5693808 application/pdf E-Thesis true 2018-08-02T16:24:41.5670000 false
title Extraction of programs for exact number computation using Agda.
spellingShingle Extraction of programs for exact number computation using Agda.
Chi Ming Chuang
title_short Extraction of programs for exact number computation using Agda.
title_full Extraction of programs for exact number computation using Agda.
title_fullStr Extraction of programs for exact number computation using Agda.
title_full_unstemmed Extraction of programs for exact number computation using Agda.
title_sort Extraction of programs for exact number computation using Agda.
author_id_str_mv f2d226665fc9a278c0f31a914e196a7e
author_id_fullname_str_mv f2d226665fc9a278c0f31a914e196a7e_***_Chi Ming Chuang
author Chi Ming Chuang
author2 Chi Ming Chuang
format E-Thesis
publishDate 2011
institution Swansea University
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description This thesis contains the to our knowledge first research project to ex-tract in the theorem prover Agda programs from proofs involving pos-tulated 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 real numbers which are limits of Cauchy sequences of rational numbers (Cauchy Reals) and show that they are closed under addition and multiplication. We also prove that Cauchy Reals are Cauchy complete. Furthermore, we introduce the real numbers in the interval [-1,1], which have a binary signed digit representation, i.e. r = 0.d0d1d2..., where di &isin; {lcub}-1, 0, 1{rcub}. This set of real numbers is given as a codata type (SDR). We determine for rational numbers in the interval [-1, 1] their SDR and show that SDRs are closed under the average function and the multiplication function. Besides, a finding digit function is defined which determines the first n digits of a stream of signed digits. In the second part of the thesis, a theorem is given which shows the correctness of our method. It shows that under certain conditions our method always normalises and doesn't make use of the axioms. The conditions mainly guarantee that a postulated function or axiom has as result type only a postulated type, so the reduction of elements of algebraic data types to head normal form will not refer to these postulates. Because of our theorem the finding digit function applied to a real number r s.t. SDR r holds normalises to [do, d1,..., dn-1] for the first n digit d0d1...dn-1 of r. Therefore, we can compute the SDR of rational numbers and from SDRs of real numbers the SDR of their average and product.
published_date 2011-12-31T05:20:10Z
_version_ 1866948055783178240
score 11.107121

Similar Items