No Cover Image

Book chapter 860 views 172 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

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
Tags: Add Tag
No Tags, Be the first to tag this record!
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