Book chapter 1056 views 218 downloads
Optimized Program Extraction for Induction and Coinduction
Ulrich Berger 
,
Olga Petrovska
,
Olga Petrovska
Sailing Routes in the World of Computation, Volume: 10936, Pages: 70 - 80
Swansea University Authors:
Ulrich Berger , Olga Petrovska
-
PDF | Accepted Manuscript
Download (327.7KB)
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...
| 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 |
| 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 |
|---|---|
| College: |
Faculty of Science and Engineering |
| Start Page: |
70 |
| End Page: |
80 |