Skip to main content
SpringerLink
Log in

Turing-Completeness Totally Free

  • Conference paper
  • First Online:
Book cover Mathematics of Program Construction (MPC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9129))

Included in the following conference series:

Abstract

In this paper, I show that general recursive definitions can be represented in the free monad which supports the ‘effect’ of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.

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.

    http://github.com/pigworker/Totality.

  2. 2.

    I write brackets for case analysis over a sum.

  3. 3.

    Whenever I intend a monoidal accumulation, I say ‘crush’, not ‘fold’.

  4. 4.

    Agda, Coq, etc., stratify types by ‘size’ into sets-of-values, sets-of-sets-of-values, and so on, ensuring consistency by forbidding the quantification over ‘large’ types by ‘small’.

  5. 5.

    They observe also that and form a monad morphism.

References

  1. Abel, A.: Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Ph.D. thesis, Ludwig Maximilians University Munich (2007)

    Google Scholar 

  2. Abel, A., Chapman, J.: Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. In: Levy, P., Krishnaswami, N. (eds.) Workshop on Mathematically Structured Functional Programming 2014, vol. 153 of EPTCS, pp. 51–67 (2014)

    Google Scholar 

  3. Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: Giacobazzi, R., Cousot, R. (eds.) ACM Symposium on Principles of Programming Languages, POPL 2013, ACM, pp. 27–38 (2013)

    Google Scholar 

  4. Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 297–311. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108–123 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bove, A.: Simple general recursion in type theory. Nord. J. Comput. 8(1), 22–42 (2001)

    MathSciNet  MATH  Google Scholar 

  8. Bove, A., Capretta, V.: Nested general recursion and partiality in type theory. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 121–135. Springer, Heidelberg (2001)

    Chapter  MATH  Google Scholar 

  9. Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 115–129. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Capretta, V.: General recursion via coinductive types. Log. Meth. Comput. Sci. 1(2), 1–28 (2005)

    Article  MATH  Google Scholar 

  11. Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Dybjer, P., Setzer, A.: Indexed induction-recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, pp. 93–113. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Ghani, N., Hancock, P.: Containers, monads and induction recursion. Math. Struct. Comput. Sci. FirstView: 1–25, 2 (2015)

    Google Scholar 

  14. Ghani, N., Lüth, C., De Marchi, F., Power, J.: Algebras, coalgebras, monads and comonads. Electr. Notes Theor. Comput. Sci. 44(1), 128–145 (2001)

    Article  MATH  Google Scholar 

  15. Giménez, E.: Codifying guarded definitions with recursive schemes. In: Smith, J., Dybjer, Peter, Nordström, Bengt (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  16. Hancock, P., McBride, C., Ghani, N., Malatesta, L., Altenkirch, T.: Small Induction Recursion. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 156–172. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen, L.J., Los, J., Pfeiffer, H., Podewski, K.-P. (eds.) LMPS 6, pp. 153–175. North-Holland (1982)

    Google Scholar 

  18. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), pp. 14–23. IEEE Computer Society, Pacific Grove, California, USA, 5–8 June 1989

    Google Scholar 

  19. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  20. Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categorical Struct. 11(1), 69–94 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  21. Turner, D.A.: Total functional programming. J. Univ. Comput. Sci. 10(7), 751–768 (2004)

    MathSciNet  Google Scholar 

  22. Uustalu, T.: Partiality is an effect. Talk Given at Dagstuhl Seminar on Dependently Typed Programming. http://www.ioc.ee/~tarmo/tday-veskisilla/uustalu-slides.pdf (2004)

Download references

Author information

Authors and Affiliations

  1. University of Strathclyde, Glasgow, Scotland, UK

    Conor McBride

Authors
  1. Conor McBride
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Conor McBride .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, UK

    Ralf Hinze

  2. University of Bonn, Bonn, Germany

    Janis Voigtländer

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

McBride, C. (2015). Turing-Completeness Totally Free. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19797-5_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19796-8

  • Online ISBN: 978-3-319-19797-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation