No Cover Image

Book chapter 1056 views 218 downloads

Optimized Program Extraction for Induction and Coinduction

Ulrich Berger Orcid Logo, Olga Petrovska Orcid Logo

Sailing Routes in the World of Computation, Volume: 10936, Pages: 70 - 80

Swansea University Authors: Ulrich Berger Orcid Logo, Olga Petrovska Orcid Logo

Check full text

DOI (Published version): 10.1007/978-3-319-94418-0_7

Abstract

The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instanc...

Full description

Published in: Sailing Routes in the World of Computation
ISBN: 9783319944173 9783319944180
ISSN: 0302-9743 1611-3349
Published: Cham Springer International Publishing 2018
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa39885
first_indexed 2018-07-30T13:32:07Z
last_indexed 2024-11-14T11:48:38Z
id cronfa39885
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2023-05-22T15:01:12.7002403</datestamp><bib-version>v2</bib-version><id>39885</id><entry>2018-05-02</entry><title>Optimized Program Extraction for Induction and Coinduction</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>3f0bf84d3c8d15113f3f0da0aab6b783</sid><ORCID>0000-0003-1170-8816</ORCID><firstname>Olga</firstname><surname>Petrovska</surname><name>Olga Petrovska</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2018-05-02</date><deptcode>MACS</deptcode><abstract>The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice</abstract><type>Book chapter</type><journal>Sailing Routes in the World of Computation</journal><volume>10936</volume><journalNumber/><paginationStart>70</paginationStart><paginationEnd>80</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783319944173</isbnPrint><isbnElectronic>9783319944180</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-01-01</publishedDate><doi>10.1007/978-3-319-94418-0_7</doi><url>http://dx.doi.org/10.1007/978-3-319-94418-0_7</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-05-22T15:01:12.7002403</lastEdited><Created>2018-05-02T22:51:06.7841193</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>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Olga</firstname><surname>Petrovska</surname><orcid>0000-0003-1170-8816</orcid><order>2</order></author></authors><documents><document><filename>0039885-02052018230228.pdf</filename><originalFilename>mainv3.pdf</originalFilename><uploaded>2018-05-02T23:02:28.4730000</uploaded><type>Output</type><contentLength>286337</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-07-03T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2023-05-22T15:01:12.7002403 v2 39885 2018-05-02 Optimized Program Extraction for Induction and Coinduction 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 3f0bf84d3c8d15113f3f0da0aab6b783 0000-0003-1170-8816 Olga Petrovska Olga Petrovska true false 2018-05-02 MACS The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice Book chapter Sailing Routes in the World of Computation 10936 70 80 Springer International Publishing Cham 9783319944173 9783319944180 0302-9743 1611-3349 1 1 2018 2018-01-01 10.1007/978-3-319-94418-0_7 http://dx.doi.org/10.1007/978-3-319-94418-0_7 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2023-05-22T15:01:12.7002403 2018-05-02T22:51:06.7841193 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Olga Petrovska 0000-0003-1170-8816 2 0039885-02052018230228.pdf mainv3.pdf 2018-05-02T23:02:28.4730000 Output 286337 application/pdf Accepted Manuscript true 2019-07-03T00:00:00.0000000 true eng
title Optimized Program Extraction for Induction and Coinduction
spellingShingle Optimized Program Extraction for Induction and Coinduction
Ulrich Berger
Olga Petrovska
title_short Optimized Program Extraction for Induction and Coinduction
title_full Optimized Program Extraction for Induction and Coinduction
title_fullStr Optimized Program Extraction for Induction and Coinduction
title_full_unstemmed Optimized Program Extraction for Induction and Coinduction
title_sort Optimized Program Extraction for Induction and Coinduction
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
3f0bf84d3c8d15113f3f0da0aab6b783
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
3f0bf84d3c8d15113f3f0da0aab6b783_***_Olga Petrovska
author Ulrich Berger
Olga Petrovska
author2 Ulrich Berger
Olga Petrovska
format Book chapter
container_title Sailing Routes in the World of Computation
container_volume 10936
container_start_page 70
publishDate 2018
institution Swansea University
isbn 9783319944173
9783319944180
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-319-94418-0_7
publisher Springer International Publishing
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
url http://dx.doi.org/10.1007/978-3-319-94418-0_7
document_store_str 1
active_str 0
description The paper proves soundness of an optimized realizability interpretation for a logic supporting strictly positive induction and coinduction. The optimization concerns the special treatment of Harrop formulas which yields simpler extracted programs. It is shown that wellfounded induction is an instance of strictly positive induction and from this a new computationally meaningful formulation of the Archimedean property for real numbers is derived. An example of program extraction in computableanalysis shows that Archimedean induction can be used to eliminate countable choice
published_date 2018-01-01T19:24:12Z
_version_ 1821344060851355648
score 11.04748

Similar Items