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