Turing-completeness totally free

McBride, Conor; Hinze, Ralf and Voigtländer, Janis, eds. (2015) Turing-completeness totally free. In: Mathematics of Program Construction. Lecture Notes in Computer Science, 9129 . Springer, DEU, pp. 257-275. ISBN 9783319197968

[thumbnail of McBride-LNCS2015-Turing-completeness-totally-free]
Text (McBride-LNCS2015-Turing-completeness-totally-free)
Accepted Author Manuscript

Download (287kB)| Preview


    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.

    ORCID iDs

    McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886; Hinze, Ralf and Voigtländer, Janis