Turing-completeness totally free

McBride, Conor (2015) Turing-completeness totally free. In: Mathematics of Program Construction. Lecture Notes in Computer Science, 9129 . Springer, Cham, Switzerland, pp. 257-275. ISBN 9783319197968

[img]
Preview
 Text (McBride-LNCS2015-Turing-completeness-totally-free)
McBride_LNCS2015_Turing_completeness_totally_free.pdf
Accepted Author Manuscript
Download (287kB)| Preview

    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.

    Author(s):McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886
    Item type:Book Section
    ID code:60166
    Keywords:monad morphisms, total functional programming, monads, general recursion, Electronic computers. Computer science, Computer Science(all)
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:13 Mar 2017 16:26
    Last modified:11 Nov 2019 09:37
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/60166
    Export data:
    CORE (COnnecting REpositories)