Optimized program extraction for induction and coinduction

Abstract

We prove 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. We show that wellfounded induction is an instance of strictly positive induction and derive from this a new computationally meaningful formulation of the Archimedean property for real numbers. We give an example of program extraction in computable analysis and show that Archimedean induction can be used to eliminate countable choice.