Turing-completeness totally free

Conor McBride

doi:10.1007/978-3-319-19797-5_13

Turing-completeness totally free

Conor McBride

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

14 Citations (Scopus)

40 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 language	English
Title of host publication	Mathematics of Program Construction
Subtitle of host publication	12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings
Editors	Ralf Hinze, Janis Voigtländer
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	257-275
Number of pages	19
Volume	9129
ISBN (Print)	9783319197968
DOIs	https://doi.org/10.1007/978-3-319-19797-5_13
Publication status	Published - 9 Jun 2015
Event	12th International Conference on Mathematics of Program Construction (MPC 2015) - Königswinter, Germany Duration: 29 Jun 2015 → 1 Jul 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9129
ISSN (Print)	0302-9743

Conference

Conference	12th International Conference on Mathematics of Program Construction (MPC 2015)
Country	Germany
City	Königswinter
Period	29/06/15 → 1/07/15

Keywords

monad morphisms
total functional programming
monads
general recursion

Access to Document

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

McBride-LNCS2015-Turing-completeness-totally-freeAccepted author manuscript, 280 KB

Link to conference web site

Fingerprint Dive into the research topics of 'Turing-completeness totally free'. Together they form a unique fingerprint.

Conor McBride
- conor.mcbride@strath.ac.uk
- Computer And Information Sciences - Reader
- SICSA
Person: Academic

Cite this

@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 {\textquoteleft}effect{\textquoteright} 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 = jun,

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",

note = "12th International Conference on Mathematics of Program Construction (MPC 2015) ; Conference date: 29-06-2015 Through 01-07-2015",

}

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. https://doi.org/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 proceeding › Conference contribution book

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 book

SN - 9783319197968

VL - 9129

T3 - Lecture Notes in Computer Science

SP - 257

EP - 275

BT - Mathematics of Program Construction

A2 - Hinze, Ralf

A2 - Voigtländer, Janis

PB - Springer

CY - Cham, Switzerland

T2 - 12th International Conference on Mathematics of Program Construction (MPC 2015)

Y2 - 29 June 2015 through 1 July 2015

ER -