Turing-completeness totally free

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

  • 2 Citations

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

Recursive functions
Semantics

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. DOI: 10.1007/978-3-319-19797-5_13
McBride, Conor. / Turing-completeness totally free. Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings. editor / Ralf Hinze ; Janis Voigtländer. Vol. 9129 Cham, Switzerland : Springer, 2015. pp. 257-275 (Lecture Notes in Computer Science).
@inproceedings{4581a267e5304ce1a651eb2e60ef57d3,
title = "Turing-completeness totally free",
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.",
keywords = "monad morphisms, total functional programming, monads, general recursion",
author = "Conor McBride",
year = "2015",
month = "6",
day = "9",
doi = "10.1007/978-3-319-19797-5_13",
language = "English",
isbn = "9783319197968",
volume = "9129",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "257--275",
editor = "Ralf Hinze and Janis Voigtl{\"a}nder",
booktitle = "Mathematics of Program Construction",

}

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, Lecture Notes in Computer Science, vol. 9129, Springer, Cham, Switzerland, pp. 257-275, 12th International Conference on Mathematics of Program Construction (MPC 2015) , Königswinter, Germany, 29/06/15. DOI: 10.1007/978-3-319-19797-5_13

Turing-completeness totally free. / McBride, Conor.

Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings. ed. / Ralf Hinze; Janis Voigtländer. Vol. 9129 Cham, Switzerland : Springer, 2015. p. 257-275 (Lecture Notes in Computer Science; Vol. 9129).

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

TY - GEN

T1 - Turing-completeness totally free

AU - McBride,Conor

PY - 2015/6/9

Y1 - 2015/6/9

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

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

KW - monad morphisms

KW - total functional programming

KW - monads

KW - general recursion

UR - http://www.cs.ox.ac.uk/conferences/MPC2015/

U2 - 10.1007/978-3-319-19797-5_13

DO - 10.1007/978-3-319-19797-5_13

M3 - Conference contribution

SN - 9783319197968

VL - 9129

T3 - Lecture Notes in Computer Science

SP - 257

EP - 275

BT - Mathematics of Program Construction

PB - Springer

CY - Cham, Switzerland

ER -

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