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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The binary representation of natural numbers is obtained by defining the (same) set of natural numbers as \(\mathbf {N}(x) {\mathop {=}\limits ^{\mu }}\exists y\,((y=0 \vee y>0 \wedge \mathbf {N}(y)) \wedge \exists i\in \{0,1\}(x = 2y+i))\).
References
Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp. 27–38 (2013)
Berger, U.: Realisability for induction and coinduction with applications to constructive analysis. J. Univ. Comput. Sci. 16(18), 2535–2555 (2010)
Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods Comput. Sci. 7(1), 1–24 (2011)
Berger, U., Hou, T.: A realizability interpretation of Church’s simple theory of types. Math. Struct. Comput. Sci. 27, 1–22 (2016)
Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog - a tool for program extraction supporting algebras and coalgebras. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 393–399. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_29
Berger, U., Miyamoto, K., Schwichtenberg, H., Tsuiki, H.: Logic for Gray-code computation. In: Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter (2016)
Berger, U., Seisenberger, M.: Proofs, programs, processes. Theory Comput. Syst. 51(3), 213–329 (2012)
Berger, U., Spreen, D.: A coinductive approach to computing with compact sets. J. Logic Anal. 8, 1–35 (2016)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5
Bridges, D., Richman, F., Schuster, P.: Linear independence without choice. Ann. Pure Appl. Logic 101(1), 95–102 (1999)
Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, New Jersey (1986)
Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol. 93. CUP (2003)
Miranda-Perea, F.: Realizability for monotone clausular (co)inductive definitions. Electr. Notes Theoret. Comput. Sci. 123, 179–193 (2005)
Miyamoto, K.: Program extraction from coinductive proofs and its application to exact real arithmetic. Ph.D. thesis, Mathematisches Institut LMU, Munich (1993)
Miyamoto, K., Nordvall Forsberg, F., Schwichtenberg, H.: Program extraction from nested definitions. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 370–385. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_27
Parigot, M.: Recursive programming with proofs. Theor. Comput. Sci. 94(2), 335–356 (1992)
Richman, F.: The fundamental theorem of algebra: a constructive development without choice. Pacific J. Math. 196(1), 213–230 (2000)
Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 338–364. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054298
Tupailo, S.: On the intuitionistic strength of monotone inductive definitions. J. Symb. Logic 69(3), 790–798 (2004)
Acknowledgments
This work was supported by the Marie Curie International Research Staff Exchange Schemes Computable Analysis (PIRSES-GA-2011-294962) and Correctness by Construction (FP7-PEOPLE-2013-IRSES-612638) as well as the Marie Curie RISE project Computing with Infinite Data (H2020-MSCA-RISE-2016-731143) and the EPSRC Doctoral Training Grant No. 1818640.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Berger, U., Petrovska, O. (2018). Optimized Program Extraction for Induction and Coinduction. In: Manea, F., Miller, R., Nowotka, D. (eds) Sailing Routes in the World of Computation. CiE 2018. Lecture Notes in Computer Science(), vol 10936. Springer, Cham. https://doi.org/10.1007/978-3-319-94418-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-94418-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94417-3
Online ISBN: 978-3-319-94418-0
eBook Packages: Computer ScienceComputer Science (R0)