Turing-completeness totally free

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)
33 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationMathematics of Program Construction
Subtitle of host publication12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings
EditorsRalf Hinze, Janis Voigtländer
Place of PublicationCham, Switzerland
PublisherSpringer
Pages257-275
Number of pages19
Volume9129
ISBN (Print)9783319197968
DOIs
Publication statusPublished - 9 Jun 2015
Event12th International Conference on Mathematics of Program Construction (MPC 2015) - Königswinter, Germany
Duration: 29 Jun 20151 Jul 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9129
ISSN (Print)0302-9743

Conference

Conference12th International Conference on Mathematics of Program Construction (MPC 2015)
CountryGermany
CityKönigswinter
Period29/06/151/07/15

    Fingerprint

Keywords

  • monad morphisms
  • total functional programming
  • monads
  • general recursion

Cite this

McBride, C. (2015). Turing-completeness totally free. In R. Hinze, & J. Voigtländer (Eds.), Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings (Vol. 9129, pp. 257-275). (Lecture Notes in Computer Science; Vol. 9129). Cham, Switzerland: Springer. https://doi.org/10.1007/978-3-319-19797-5_13