Skip to main content
SpringerLink
Log in

Optimized Program Extraction for Induction and Coinduction

  • Conference paper
  • First Online:
Book cover Sailing Routes in the World of Computation (CiE 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10936))

Included in the following conference series:

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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

  1. 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)

    Google Scholar 

  2. Berger, U.: Realisability for induction and coinduction with applications to constructive analysis. J. Univ. Comput. Sci. 16(18), 2535–2555 (2010)

    MathSciNet  MATH  Google Scholar 

  3. Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods Comput. Sci. 7(1), 1–24 (2011)

    Article  MathSciNet  Google Scholar 

  4. Berger, U., Hou, T.: A realizability interpretation of Church’s simple theory of types. Math. Struct. Comput. Sci. 27, 1–22 (2016)

    MathSciNet  Google Scholar 

  5. 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

    Chapter  MATH  Google Scholar 

  6. 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)

    Google Scholar 

  7. Berger, U., Seisenberger, M.: Proofs, programs, processes. Theory Comput. Syst. 51(3), 213–329 (2012)

    Article  MathSciNet  Google Scholar 

  8. Berger, U., Spreen, D.: A coinductive approach to computing with compact sets. J. Logic Anal. 8, 1–35 (2016)

    MathSciNet  MATH  Google Scholar 

  9. 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

    Book  MATH  Google Scholar 

  10. Bridges, D., Richman, F., Schuster, P.: Linear independence without choice. Ann. Pure Appl. Logic 101(1), 95–102 (1999)

    Article  MathSciNet  Google Scholar 

  11. Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, New Jersey (1986)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. Miranda-Perea, F.: Realizability for monotone clausular (co)inductive definitions. Electr. Notes Theoret. Comput. Sci. 123, 179–193 (2005)

    Article  MathSciNet  Google Scholar 

  14. Miyamoto, K.: Program extraction from coinductive proofs and its application to exact real arithmetic. Ph.D. thesis, Mathematisches Institut LMU, Munich (1993)

    Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. Parigot, M.: Recursive programming with proofs. Theor. Comput. Sci. 94(2), 335–356 (1992)

    Article  MathSciNet  Google Scholar 

  17. Richman, F.: The fundamental theorem of algebra: a constructive development without choice. Pacific J. Math. 196(1), 213–230 (2000)

    Article  MathSciNet  Google Scholar 

  18. 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

    Chapter  Google Scholar 

  19. Tupailo, S.: On the intuitionistic strength of monotone inductive definitions. J. Symb. Logic 69(3), 790–798 (2004)

    Article  MathSciNet  Google Scholar 

Download references

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

  1. Swansea University, Swansea, SA2 8PP, Wales, UK

    Ulrich Berger & Olga Petrovska

Authors
  1. Ulrich Berger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olga Petrovska
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ulrich Berger .

Editor information

Editors and Affiliations

  1. Kiel University, Kiel, Germany

    Florin Manea

  2. Queens College, CUNY, Queens, New York, USA

    Russell G. Miller

  3. Kiel University, Kiel, Germany

    Dirk Nowotka

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation